:: AFINSQ_1 semantic presentation

theorem E1: :: AFINSQ_1:1
for b1 being Nat holds b1 in b1 + 1
proof
let c1 be Nat;
c1 < c1 + 1 by NAT_1:38;
then c1 in { b1 where B is Nat : b1 < c1 + 1 } ;
hence c1 in c1 + 1 by AXIOMS:30;
end;

theorem E2: :: AFINSQ_1:2
for b1, b2 being Nat holds
( b1 <= b2 implies b1 = b1 /\ b2 )
proof
let c1, c2 be Nat;
assume c1 <= c2 ;
then c1 c= c2 by CARD_1:56;
hence c1 = c1 /\ c2 by XBOOLE_1:28;
end;

theorem :: AFINSQ_1:3
for b1, b2 being Nat holds
( b1 = b1 /\ b2 implies b1 <= b2 ) by E2;

theorem E3: :: AFINSQ_1:4
for b1 being Nat holds b1 \/ {b1} = b1 + 1
proof
let c1 be Nat;
c1 + 1 = succ c1 by CARD_1:52;
hence c1 \/ {c1} = c1 + 1 by ORDINAL1:def 1;
end;

theorem E4: :: AFINSQ_1:5
for b1 being Nat holds Seg b1 c= b1 + 1
proof
let c1 be Nat;
let c2 be set ; :: according to TARSKI:def 3
assume E5: c2 in Seg c1 ;
then reconsider c3 = c2 as Nat ;
( 1 <= c3 & c3 <= c1 ) by E5, FINSEQ_1:3;
then c3 < c1 + 1 by NAT_1:38;
hence c2 in c1 + 1 by EULER_1:1;
end;

theorem :: AFINSQ_1:6
for b1 being Nat holds b1 + 1 = {0} \/ (Seg b1)
proof
let c1 be Nat;
thus c1 + 1 c= {0} \/ (Seg c1) :: according to XBOOLE_0:def 10
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in c1 + 1 ;
then c2 in { b1 where B is Nat : b1 < c1 + 1 } by AXIOMS:30;
then consider c3 being Nat such that
E5: ( c3 = c2 & c3 < c1 + 1 ) ;
( c3 = 0 or ( 0 < c3 & c3 <= c1 ) ) by E5, NAT_1:38;
then ( c3 = 0 or ( 1 < c3 + 1 & c3 <= c1 ) ) by XREAL_1:31;
then ( c3 = 0 or ( 1 <= c3 & c3 <= c1 ) ) by NAT_1:38;
then ( c2 in {0} or c2 in Seg c1 ) by E5, FINSEQ_1:3, TARSKI:def 1;
hence c2 in {0} \/ (Seg c1) by XBOOLE_0:def 2;
end;
1 <= c1 + 1 by NAT_1:29;
then E5: {0} c= c1 + 1 by CARD_1:56, CARD_5:1;
Seg c1 c= c1 + 1 by E4;
hence {0} \/ (Seg c1) c= c1 + 1 by E5, XBOOLE_1:8;
end;

theorem E5: :: AFINSQ_1:7
for b1 being Function holds
( ( b1 is finite & b1 is T-Sequence-like ) iff ex b2 being Nat st dom b1 = b2 )
proof
let c1 be Function;
hereby
assume ( c1 is finite & c1 is T-Sequence-like ) ;
then ( dom c1 is finite & dom c1 is Ordinal ) by FINSET_1:29, ORDINAL1:def 7;
then dom c1 in omega by CARD_4:7;
hence ex b1 being Nat st dom c1 = b1 ;
end;
assume ex b1 being Nat st dom c1 = b1 ;
hence ( c1 is finite & c1 is T-Sequence-like ) by FINSET_1:29, ORDINAL1:def 7;
end;

registration
cluster T-Sequence-like finite set ;
existence
ex b1 being Function st
( b1 is finite & b1 is T-Sequence-like )
proof
take c1 = {} ;
E6: for b1 being set holds
( b1 in {} implies c1 . b1 = 0 ) ;
dom c1 = {} ;
hence ( c1 is finite & c1 is T-Sequence-like ) by E6, E5;
end;
end;

definition
mode XFinSequence is finite T-Sequence;
end;

registration
cluster natural -> finite set ;
coherence
for b1 being set holds
( b1 is natural implies b1 is finite )
proof
let c1 be set ;
assume c1 in omega ; :: according to ORDINAL2:def 21
then c1 is Nat ;
hence c1 is finite ;
end;
let c1 be XFinSequence;
cluster dom a1 -> natural ;
coherence
dom c1 is natural
proof
ex b1 being Nat st dom c1 = b1 by E5;
hence dom c1 is natural ;
end;
end;

notation
let c1 be XFinSequence;
synonym len c1 for Card c1;
end;

definition
let c1 be XFinSequence;
redefine func len as len c1 -> Nat means :E6: :: AFINSQ_1:def 1
a2 = dom a1;
coherence
len c1 is Nat
proof
Card c1 = card c1 ;
hence len c1 is Nat ;
end;
compatibility
for b1 being Nat holds
( b1 = len c1 iff b1 = dom c1 )
proof
let c2 be Nat;
consider c3 being Nat such that
E6: dom c1 = c3 by E5;
dom c1,c1 are_equipotent
proof
deffunc H1( set ) -> set = [a1,(c1 . a1)];
consider c4 being Function such that
E7: dom c4 = dom c1 and
E8: for b1 being set holds
( b1 in dom c1 implies c4 . b1 = H1(b1) ) from FUNCT_1:sch 3();
 take c4 ; :: according to WELLORD2:def 4
thus c4 is one-to-one
proof
let c5 be set ; :: according to FUNCT_1:def 8
let c6 be set ;
assume E9: ( c5 in dom c4 & c6 in dom c4 ) ;
assume c4 . c5 = c4 . c6 ;
then [c5,(c1 . c5)] = c4 . c6 by E7, E8, E9
.= [c6,(c1 . c6)] by E7, E8, E9 ;
hence c5 = c6 by ZFMISC_1:33;
end;
thus dom c4 = dom c1 by E7;
thus rng c4 c= c1 :: according to XBOOLE_0:def 10
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in rng c4 ;
then consider c6 being set such that
E9: c6 in dom c4 and
E10: c4 . c6 = c5 by FUNCT_1:def 5;
c4 . c6 = [c6,(c1 . c6)] by E7, E8, E9;
hence c5 in c1 by E7, E9, E10, FUNCT_1:8;
end;
let c5 be set ; :: according to TARSKI:def 3
assume E9: c5 in c1 ;
then consider c6, c7 being set such that
E10: c5 = [c6,c7] by RELAT_1:def 1;
E11: ( c6 in dom c1 & c7 = c1 . c6 ) by E9, E10, FUNCT_1:8;
then c4 . c6 = c5 by E8, E10;
hence c5 in rng c4 by E7, E11, FUNCT_1:def 5;
end;
then E7: Card c1 = Card (dom c1) by CARD_1:21;
hence ( c2 = Card c1 implies c2 = dom c1 ) by E6, CARD_1:66;
thus ( c2 = dom c1 implies c2 = len c1 ) by E7, CARD_1:66;
end;
end;

:: deftheorem E6 defines len AFINSQ_1:def 1 :
for b1 being XFinSequence
for b2 being Nat holds
( b2 = len b1 iff b2 = dom b1 );

definition
let c1 be XFinSequence;
redefine func dom as dom c1 -> Subset of NAT ;
coherence
dom c1 is Subset of NAT
proof
E7: dom c1 = len c1 by E6
.= { b1 where B is Nat : b1 < len c1 } by AXIOMS:30 ;
{ b1 where B is Nat : b1 < len c1 } c= NAT
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in { b1 where B is Nat : b1 < len c1 } ;
then consider c3 being Nat such that
E8: ( c3 = c2 & c3 < len c1 ) ;
thus c2 in NAT by E8;
end;
hence dom c1 is Subset of NAT by E7;
end;
end;

theorem :: AFINSQ_1:8
for b1 being Function holds
not ( ex b2 being Nat st dom b1 c= b2 & ( for b2 being XFinSequence holds
not b1 c= b2 ) )
proof
let c1 be Function;
given c2 being Nat such that E7: dom c1 c= c2 ;
deffunc H1( set ) -> set = c1 . a1;
consider c3 being Function such that
E8: ( dom c3 = c2 & ( for b1 being set holds
( b1 in c2 implies c3 . b1 = H1(b1) ) ) ) from FUNCT_1:sch 3();
 reconsider c4 = c3 as XFinSequence by E8, E5;
take c4 ;
let c5 be set ; :: according to TARSKI:def 3
assume E9: c5 in c1 ;
then consider c6, c7 being set such that
E10: [c6,c7] = c5 by RELAT_1:def 1;
c6 in dom c1 by E9, E10, RELAT_1:def 4;
then ( c6 in dom c4 & c1 . c6 = c7 ) by E7, E8, E9, E10, FUNCT_1:def 4;
then ( [c6,(c4 . c6)] in c4 & c4 . c6 = c7 ) by E8, FUNCT_1:8;
hence c5 in c4 by E10;
end;

scheme :: AFINSQ_1:sch 1
s1{ F1() -> Nat, P1[ set , set ] } :
ex b1 being XFinSequence st
( dom b1 = F1() & ( for b2 being Nat holds
( b2 in F1() implies P1[b2,b1 . b2] ) ) )
provided
E7: for b1 being Nat
for b2, b3 being set holds
( ( b1 in F1() & P1[b1,b2] & P1[b1,b3] ) implies ( b2 = b3 ) ) and E8: for b1 being Nat holds
not ( b1 in F1() & ( for b2 being set holds
not P1[b1,b2] ) )
proof
E9: for b1, b2, b3 being set holds
( ( b1 in F1() & P1[b1,b2] & P1[b1,b3] ) implies ( b2 = b3 ) )
proof
let c1, c2, c3 be set ;
assume E10: ( c1 in F1() & P1[c1,c2] & P1[c1,c3] ) ;
F1() = { b1 where B is Nat : b1 < F1() } by AXIOMS:30;
then consider c4 being Nat such that
E11: ( c4 = c1 & c4 < F1() ) by E10;
thus c2 = c3 by E7, E10, E11;
end;
E10: for b1 being set holds
not ( b1 in F1() & ( for b2 being set holds
not P1[b1,b2] ) )
proof
let c1 be set ;
assume E11: c1 in F1() ;
F1() = { b1 where B is Nat : b1 < F1() } by AXIOMS:30;
then consider c2 being Nat such that
E12: ( c2 = c1 & c2 < F1() ) by E11;
thus ex b1 being set st P1[c1,b1] by E8, E11, E12;
end;
consider c1 being Function such that
E11: ( dom c1 = F1() & ( for b1 being set holds
( b1 in F1() implies P1[b1,c1 . b1] ) ) ) from FUNCT_1:sch 2(E9, E10);
 reconsider c2 = c1 as XFinSequence by E11, E5;
take c2 ;
thus ( dom c2 = F1() & ( for b1 being Nat holds
( b1 in F1() implies P1[b1,c2 . b1] ) ) ) by E11;
end;

scheme :: AFINSQ_1:sch 2
s2{ F1() -> Nat, F2( set ) -> set } :
ex b1 being XFinSequence st
( len b1 = F1() & ( for b2 being Nat holds
( b2 in F1() implies b1 . b2 = F2(b2) ) ) )
provided
proof
consider c1 being Function such that
E7: ( dom c1 = F1() & ( for b1 being set holds
( b1 in F1() implies c1 . b1 = F2(b1) ) ) ) from FUNCT_1:sch 3();
 reconsider c2 = c1 as XFinSequence by E7, E5;
take c2 ;
thus ( len c2 = F1() & ( for b1 being Nat holds
( b1 in F1() implies c2 . b1 = F2(b1) ) ) ) by E7, E6;
end;

theorem :: AFINSQ_1:9
for b1 being set
for b2 being XFinSequence holds
not ( b1 in b2 & ( for b3 being Nat holds
not ( b3 in dom b2 & b1 = [b3,(b2 . b3)] ) ) )
proof
let c1 be set ;
let c2 be XFinSequence;
assume E7: c1 in c2 ;
then consider c3, c4 being set such that
E8: c1 = [c3,c4] by RELAT_1:def 1;
c3 in dom c2 by E7, E8, FUNCT_1:8;
then reconsider c5 = c3 as Nat ;
take c5 ;
thus ( c5 in dom c2 & c1 = [c5,(c2 . c5)] ) by E7, E8, FUNCT_1:8;
end;

theorem E7: :: AFINSQ_1:10
for b1, b2 being XFinSequence holds
( ( dom b1 = dom b2 & ( for b3 being Nat holds
( b3 in dom b1 implies b1 . b3 = b2 . b3 ) ) ) implies ( b1 = b2 ) )
proof
let c1, c2 be XFinSequence;
assume E8: ( dom c1 = dom c2 & ( for b1 being Nat holds
( b1 in dom c1 implies c1 . b1 = c2 . b1 ) ) ) ;
then for b1 being set holds
( b1 in dom c1 implies c1 . b1 = c2 . b1 ) ;
hence c1 = c2 by E8, FUNCT_1:9;
end;

theorem :: AFINSQ_1:11
for b1, b2 being XFinSequence holds
( ( len b1 = len b2 & ( for b3 being Nat holds
( b3 < len b1 implies b1 . b3 = b2 . b3 ) ) ) implies ( b1 = b2 ) )
proof
let c1, c2 be XFinSequence;
assume E8: ( len c1 = len c2 & ( for b1 being Nat holds
( b1 < len c1 implies c1 . b1 = c2 . b1 ) ) ) ;
E9: ( dom c1 = len c1 & dom c2 = len c2 ) by E6;
now
let c3 be set ;
assume E10: c3 in dom c1 ;
then reconsider c4 = c3 as Nat ;
c4 < len c1 by E9, E10, EULER_1:1;
hence c1 . c3 = c2 . c3 by E8;
end;
hence c1 = c2 by E8, E9, FUNCT_1:9;
end;

theorem E8: :: AFINSQ_1:12
for b1 being Nat
for b2 being XFinSequence holds
b2 | b1 is XFinSequence
proof
let c1 be Nat;
let c2 be XFinSequence;
E9: dom (c2 | c1) = (dom c2) /\ c1 by RELAT_1:90
.= (len c2) /\ c1 by E6 ;
( len c2 <= c1 or c1 <= len c2 ) ;
then ( dom (c2 | c1) = len c2 or dom (c2 | c1) = c1 ) by E9, E2;
hence c2 | c1 is XFinSequence by E5;
end;

theorem :: AFINSQ_1:13
for b1 being Function
for b2 being XFinSequence holds
( rng b2 c= dom b1 implies b1 * b2 is XFinSequence )
proof
let c1 be Function;
let c2 be XFinSequence;
assume rng c2 c= dom c1 ;
then dom (c1 * c2) = dom c2 by RELAT_1:46
.= len c2 by E6 ;
hence c1 * c2 is XFinSequence by E5;
end;

theorem :: AFINSQ_1:14
for b1 being Nat
for b2, b3 being XFinSequence holds
( ( b3 = b2 | b1 ) implies ( not b1 < len b2 or ( len b3 = b1 & dom b3 = b1 ) ) )
proof
let c1 be Nat;
let c2, c3 be XFinSequence;
assume E9: ( c1 < len c2 & c3 = c2 | c1 ) ;
then c1 c= len c2 by CARD_1:56;
then c1 c= dom c2 by E6;
then dom c3 = c1 by E9, RELAT_1:91;
hence ( len c3 = c1 & dom c3 = c1 ) by E6;
end;

registration
let c1 be set ;
cluster finite T-Sequence of a1;
existence
ex b1 being T-Sequence of c1 st b1 is finite
proof
{} is T-Sequence of c1 by ORDINAL1:45;
hence ex b1 being T-Sequence of c1 st b1 is finite ;
end;
end;

definition
let c1 be set ;
mode XFinSequence is finite T-Sequence of a1;
end;

theorem E9: :: AFINSQ_1:15
for b1 being set
for b2 being XFinSequence of b1 holds
b2 is PartFunc of NAT ,b1
proof
let c1 be set ;
let c2 be XFinSequence of c1;
E10: dom c2 c= NAT ;
rng c2 c= c1 by ORDINAL1:def 8;
hence c2 is PartFunc of NAT ,c1 by E10, RELSET_1:11;
end;

registration
cluster {} -> T-Sequence-like ;
coherence
{} is T-Sequence-like by ORDINAL1:45;
end;

registration
let c1 be set ;
cluster T-Sequence-like finite M5( NAT ,a1);
existence
ex b1 being PartFunc of NAT ,c1 st
( b1 is finite & b1 is T-Sequence-like )
proof
{} is PartFunc of NAT ,c1 by PARTFUN1:56;
hence ex b1 being PartFunc of NAT ,c1 st
( b1 is finite & b1 is T-Sequence-like ) ;
end;
end;

theorem :: AFINSQ_1:16
for b1 being Nat
for b2 being set
for b3 being XFinSequence of b2 holds
b3 | b1 is XFinSequence of b2
proof
let c1 be Nat;
let c2 be set ;
let c3 be XFinSequence of c2;
( rng (c3 | c1) c= rng c3 & rng c3 c= c2 ) by ORDINAL1:def 8;
then rng (c3 | c1) c= c2 by XBOOLE_1:1;
hence c3 | c1 is XFinSequence of c2 by E8, ORDINAL1:def 8;
end;

theorem :: AFINSQ_1:17
for b1 being Nat
for b2 being non empty set holds
ex b3 being XFinSequence of b2 st len b3 = b1
proof
let c1 be Nat;
let c2 be non empty set ;
consider c3 being Element of c2;
set c4 = c1 --> c3;
E10: ( dom (c1 --> c3) = c1 & ( for b1 being Nat holds
( b1 in c1 implies (c1 --> c3) . b1 = c3 ) ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider c5 = c1 --> c3 as XFinSequence by E5;
E11: rng c5 c= {c3} by FUNCOP_1:19;
{c3} c= c2 by ZFMISC_1:37;
then rng c5 c= c2 by E11, XBOOLE_1:1;
then reconsider c6 = c5 as XFinSequence of c2 by ORDINAL1:def 8;
take c6 ;
thus len c6 = c1 by E10, E6;
end;

registration
cluster empty set ;
existence
ex b1 being XFinSequence st b1 is empty by ORDINAL1:45;
end;

theorem E10: :: AFINSQ_1:18
for b1 being XFinSequence holds
( len b1 = 0 iff b1 = {} )
proof
let c1 be XFinSequence;
( len c1 = 0 iff c1, {} are_equipotent ) by CARD_1:def 5;
hence ( len c1 = 0 iff c1 = {} ) by CARD_1:46;
end;

theorem E11: :: AFINSQ_1:19
for b1 being set holds
{} is XFinSequence of b1
proof
let c1 be set ;
rng {} c= c1 by XBOOLE_1:2;
hence {} is XFinSequence of c1 by ORDINAL1:def 8;
end;

registration
let c1 be set ;
cluster empty T-Sequence of a1;
existence
ex b1 being XFinSequence of c1 st b1 is empty
proof
{} is XFinSequence of c1 by E11;
hence ex b1 being XFinSequence of c1 st b1 is empty ;
end;
end;

definition
let c1 be set ;
func <%c1%> -> set equals :: AFINSQ_1:def 2
{[0,a1]};
coherence
{[0,c1]} is set ;
end;

:: deftheorem defines <% AFINSQ_1:def 2 :
for b1 being set holds <%b1%> = {[0,b1]};

definition
let c1 be set ;
func <%> c1 -> empty XFinSequence of a1 equals :: AFINSQ_1:def 3
 {} ;
coherence
{} is empty XFinSequence of c1 by E11;
end;

:: deftheorem defines <%> AFINSQ_1:def 3 :
for b1 being set holds <%> b1 = {} ;

definition
let c1, c2 be XFinSequence;
redefine func c1 ^ c2 -> set means :E12: :: AFINSQ_1:def 4
( dom a3 = (len a1) + (len a2) & ( for b1 being Nat holds
( b1 in dom a1 implies a3 . b1 = a1 . b1 ) ) & ( for b1 being Nat holds
( b1 in dom a2 implies a3 . ((len a1) + b1) = a2 . b1 ) ) );
compatibility
for b1 being set holds
( b1 = c1 ^ c2 iff ( dom b1 = (len c1) + (len c2) & ( for b2 being Nat holds
( b2 in dom c1 implies b1 . b2 = c1 . b2 ) ) & ( for b2 being Nat holds
( b2 in dom c2 implies b1 . ((len c1) + b2) = c2 . b2 ) ) ) )
proof
let c3 be T-Sequence;
E12: ( len c1 = dom c1 & len c2 = dom c2 ) by E6;
E13: (len c1) +^ (len c2) = (len c1) + (len c2) by CARD_2:49;
hereby
assume E14: c3 = c1 ^ c2 ;
hence dom c3 = (len c1) + (len c2) by E12, E13, ORDINAL4:def 1;
thus for b1 being Nat holds
( b1 in dom c1 implies c3 . b1 = c1 . b1 ) by E14, ORDINAL4:def 1;
let c4 be Nat;
assume c4 in dom c2 ;
then c3 . ((len c1) +^ c4) = c2 . c4 by E12, E14, ORDINAL4:def 1;
hence c3 . ((len c1) + c4) = c2 . c4 by CARD_2:49;
end;
assume that
E14: dom c3 = (len c1) + (len c2) and
E15: for b1 being Nat holds
( b1 in dom c1 implies c3 . b1 = c1 . b1 ) and
E16: for b1 being Nat holds
( b1 in dom c2 implies c3 . ((len c1) + b1) = c2 . b1 ) ;
E17: for b1 being Ordinal holds
( b1 in dom c1 implies c3 . b1 = c1 . b1 ) by E15;
now
let c4 be Ordinal;
assume E18: c4 in dom c2 ;
then reconsider c5 = c4 as Nat ;
thus c3 . ((dom c1) +^ c4) = c3 . ((len c1) + c5) by E12, CARD_2:49
.= c2 . c4 by E16, E18 ;
end;
hence c3 = c1 ^ c2 by E12, E13, E14, E17, ORDINAL4:def 1;
end;
end;

:: deftheorem E12 defines ^ AFINSQ_1:def 4 :
for b1, b2 being XFinSequence
for b3 being set holds
( b3 = b1 ^ b2 iff ( dom b3 = (len b1) + (len b2) & ( for b4 being Nat holds
( b4 in dom b1 implies b3 . b4 = b1 . b4 ) ) & ( for b4 being Nat holds
( b4 in dom b2 implies b3 . ((len b1) + b4) = b2 . b4 ) ) ) );

registration
let c1, c2 be XFinSequence;
cluster a1 ^ a2 -> finite ;
coherence
c1 ^ c2 is finite
proof
dom (c1 ^ c2) = (dom c1) +^ (dom c2) by ORDINAL4:def 1;
then dom (c1 ^ c2) is Nat by ORDINAL2:def 21;
hence c1 ^ c2 is finite by E5;
end;
end;

theorem E13: :: AFINSQ_1:20
for b1, b2 being XFinSequence holds len (b1 ^ b2) = (len b1) + (len b2)
proof
let c1, c2 be XFinSequence;
dom (c1 ^ c2) = (len c1) + (len c2) by E12;
hence len (c1 ^ c2) = (len c1) + (len c2) by E6;
end;

theorem E14: :: AFINSQ_1:21
for b1 being Nat
for b2, b3 being XFinSequence holds
( ( len b2 <= b1 ) implies ( not b1 < (len b2) + (len b3) or (b2 ^ b3) . b1 = b3 . (b1 - (len b2)) ) )
proof
let c1 be Nat;
let c2, c3 be XFinSequence;
assume E15: ( len c2 <= c1 & c1 < (len c2) + (len c3) ) ;
then consider c4 being Nat such that
E16: (len c2) + c4 = c1 by NAT_1:28;
c1 - (len c2) < ((len c2) + (len c3)) - (len c2) by E15, REAL_1:92;
then c4 in len c3 by E16, EULER_1:1;
then c4 in dom c3 by E6;
hence (c2 ^ c3) . c1 = c3 . (c1 - (len c2)) by E16, E12;
end;

theorem :: AFINSQ_1:22
for b1 being Nat
for b2, b3 being XFinSequence holds
( ( len b2 <= b1 ) implies ( not b1 < len (b2 ^ b3) or (b2 ^ b3) . b1 = b3 . (b1 - (len b2)) ) )
proof
let c1 be Nat;
let c2, c3 be XFinSequence;
assume E15: ( len c2 <= c1 & c1 < len (c2 ^ c3) ) ;
then c1 < (len c2) + (len c3) by E13;
hence (c2 ^ c3) . c1 = c3 . (c1 - (len c2)) by E15, E14;
end;

theorem E15: :: AFINSQ_1:23
for b1 being Nat
for b2, b3 being XFinSequence holds
not ( b1 in dom (b2 ^ b3) & not b1 in dom b2 & ( for b4 being Nat holds
not ( b4 in dom b3 & b1 = (len b2) + b4 ) ) )
proof
let c1 be Nat;
let c2, c3 be XFinSequence;
assume c1 in dom (c2 ^ c3) ;
then c1 in len (c2 ^ c3) by E6;
then c1 in (len c2) + (len c3) by E13;
then E16: c1 < (len c2) + (len c3) by EULER_1:1;
E17: now
assume not len c2 <= c1 ;
then c1 in len c2 by EULER_1:1;
hence not ( not c1 in dom c2 & ( for b1 being Nat holds
not ( b1 in dom c3 & c1 = (len c2) + b1 ) ) ) by E6;
end;
now
assume len c2 <= c1 ;
then consider c4 being Nat such that
E18: c1 = (len c2) + c4 by NAT_1:28;
(c4 + (len c2)) - (len c2) < ((len c3) + (len c2)) - (len c2) by E16, E18, REAL_1:92;
then c4 in len c3 by EULER_1:1;
then c4 in dom c3 by E6;
hence not ( not c1 in dom c2 & ( for b1 being Nat holds
not ( b1 in dom c3 & c1 = (len c2) + b1 ) ) ) by E18;
end;
hence not ( not c1 in dom c2 & ( for b1 being Nat holds
not ( b1 in dom c3 & c1 = (len c2) + b1 ) ) ) by E17;
end;

theorem E16: :: AFINSQ_1:24
for b1, b2 being T-Sequence holds dom b1 c= dom (b1 ^ b2)
proof
let c1, c2 be T-Sequence;
dom (c1 ^ c2) = (dom c1) +^ (dom c2) by ORDINAL4:def 1;
hence dom c1 c= dom (c1 ^ c2) by ORDINAL3:27;
end;

theorem E17: :: AFINSQ_1:25
for b1 being set
for b2, b3 being XFinSequence holds
not ( b1 in dom b2 & ( for b4 being Nat holds
not ( b4 = b1 & (len b3) + b4 in dom (b3 ^ b2) ) ) )
proof
let c1 be set ;
let c2, c3 be XFinSequence;
assume E18: c1 in dom c2 ;
then E19: c1 in len c2 by E6;
reconsider c4 = c1 as Nat by E18;
take c4 ;
c4 < len c2 by E19, EULER_1:1;
then (len c3) + c4 < (len c3) + (len c2) by XREAL_1:10;
then (len c3) + c4 in (len c3) + (len c2) by EULER_1:1;
hence ( c4 = c1 & (len c3) + c4 in dom (c3 ^ c2) ) by E12;
end;

theorem E18: :: AFINSQ_1:26
for b1 being Nat
for b2, b3 being XFinSequence holds
( b1 in dom b2 implies (len b3) + b1 in dom (b3 ^ b2) )
proof
let c1 be Nat;
let c2, c3 be XFinSequence;
assume c1 in dom c2 ;
then ex b1 being Nat st
( b1 = c1 & (len c3) + b1 in dom (c3 ^ c2) ) by E17;
hence (len c3) + c1 in dom (c3 ^ c2) ;
end;

theorem E19: :: AFINSQ_1:27
for b1, b2 being XFinSequence holds rng b1 c= rng (b1 ^ b2)
proof
let c1, c2 be XFinSequence;
now
let c3 be set ;
assume c3 in rng c1 ;
then consider c4 being set such that
E20: ( c4 in dom c1 & c3 = c1 . c4 ) by FUNCT_1:def 5;
reconsider c5 = c4 as Nat by E20;
E21: ( c5 in dom c1 & dom c1 c= dom (c1 ^ c2) ) by E20, E16;
(c1 ^ c2) . c5 = c1 . c5 by E20, E12;
hence c3 in rng (c1 ^ c2) by E20, E21, FUNCT_1:12;
end;
hence rng c1 c= rng (c1 ^ c2) by TARSKI:def 3;
end;

theorem E20: :: AFINSQ_1:28
for b1, b2 being XFinSequence holds rng b1 c= rng (b2 ^ b1)
proof
let c1, c2 be XFinSequence;
now
let c3 be set ;
assume c3 in rng c1 ;
then consider c4 being set such that
E21: ( c4 in dom c1 & c3 = c1 . c4 ) by FUNCT_1:def 5;
reconsider c5 = c4 as Nat by E21;
E22: (len c2) + c5 in dom (c2 ^ c1) by E21, E18;
(c2 ^ c1) . ((len c2) + c5) = c1 . c5 by E21, E12;
hence c3 in rng (c2 ^ c1) by E21, E22, FUNCT_1:12;
end;
hence rng c1 c= rng (c2 ^ c1) by TARSKI:def 3;
end;

theorem E21: :: AFINSQ_1:29
for b1, b2 being XFinSequence holds rng (b1 ^ b2) = (rng b1) \/ (rng b2)
proof
let c1, c2 be XFinSequence;
now
let c3 be set ;
assume c3 in rng (c1 ^ c2) ;
then consider c4 being set such that
E22: ( c4 in dom (c1 ^ c2) & c3 = (c1 ^ c2) . c4 ) by FUNCT_1:def 5;
E23: c4 in (len c1) + (len c2) by E22, E12;
reconsider c5 = c4 as Nat by E22;
E24: c5 < (len c1) + (len c2) by E23, EULER_1:1;
E25: now
assume E26: len c1 <= c5 ;
then E27: c2 . (c5 - (len c1)) = c3 by E22, E24, E14;
consider c6 being Nat such that
E28: (len c1) + c6 = c5 by E26, NAT_1:28;
(c6 + (len c1)) - (len c1) < ((len c1) + (len c2)) - (len c1) by E24, E28, REAL_1:92;
then c6 in len c2 by EULER_1:1;
then c5 - (len c1) in dom c2 by E28, E6;
hence c3 in rng c2 by E27, FUNCT_1:12;
end;
now
assume not len c1 <= c5 ;
then c5 in len c1 by EULER_1:1;
then E26: c5 in dom c1 by E6;
then c1 . c5 = c3 by E22, E12;
hence c3 in rng c1 by E26, FUNCT_1:12;
end;
hence c3 in (rng c1) \/ (rng c2) by E25, XBOOLE_0:def 2;
end;
then E22: rng (c1 ^ c2) c= (rng c1) \/ (rng c2) by TARSKI:def 3;
( rng c1 c= rng (c1 ^ c2) & rng c2 c= rng (c1 ^ c2) ) by E19, E20;
then (rng c1) \/ (rng c2) c= rng (c1 ^ c2) by XBOOLE_1:8;
hence rng (c1 ^ c2) = (rng c1) \/ (rng c2) by E22, XBOOLE_0:def 10;
end;

theorem E22: :: AFINSQ_1:30
for b1, b2, b3 being XFinSequence holds (b1 ^ b2) ^ b3 = b1 ^ (b2 ^ b3)
proof
let c1, c2, c3 be XFinSequence;
E23: dom ((c1 ^ c2) ^ c3) = (len (c1 ^ c2)) + (len c3) by E12
.= ((len c1) + (len c2)) + (len c3) by E13
.= (len c1) + ((len c2) + (len c3))
.= (len c1) + (len (c2 ^ c3)) by E13 ;
E24: for b1 being Nat holds
( b1 in dom c1 implies ((c1 ^ c2) ^ c3) . b1 = c1 . b1 )
proof
let c4 be Nat;
assume E25: c4 in dom c1 ;
dom c1 c= dom (c1 ^ c2) by E16;
hence ((c1 ^ c2) ^ c3) . c4 = (c1 ^ c2) . c4 by E25, E12
.= c1 . c4 by E25, E12 ;

end;
for b1 being Nat holds
( b1 in dom (c2 ^ c3) implies ((c1 ^ c2) ^ c3) . ((len c1) + b1) = (c2 ^ c3) . b1 )
proof
let c4 be Nat;
assume E25: c4 in dom (c2 ^ c3) ;
E26: now
assume E27: c4 in dom c2 ;
then (len c1) + c4 in dom (c1 ^ c2) by E18;
hence ((c1 ^ c2) ^ c3) . ((len c1) + c4) = (c1 ^ c2) . ((len c1) + c4) by E12
.= c2 . c4 by E27, E12
.= (c2 ^ c3) . c4 by E27, E12 ;

end;
now
assume not c4 in dom c2 ;
then consider c5 being Nat such that
E27: ( c5 in dom c3 & c4 = (len c2) + c5 ) by E25, E15;
thus ((c1 ^ c2) ^ c3) . ((len c1) + c4) = ((c1 ^ c2) ^ c3) . (((len c1) + (len c2)) + c5) by E27
.= ((c1 ^ c2) ^ c3) . (