:: AFINSQ_1 semantic presentation

theorem E1: :: AFINSQ_1:1

for b₁ being Nat holds b₁ in b₁ + 1

let c₁ be Nat;
c₁ < c₁ + 1 by NAT_1:38;
then c₁ in { b₁ where B is Nat : b₁ < c₁ + 1 } ;
hence c₁ in c₁ + 1 by AXIOMS:30;

end;

theorem E2: :: AFINSQ_1:2

for b₁, b₂ being Nat holds
( b₁ <= b₂ implies b₁ = b₁ /\ b₂ )

proof

let c₁, c₂ be Nat;
assume c₁ <= c₂ ;
then c₁ c= c₂ by CARD_1:56;
hence c₁ = c₁ /\ c₂ by XBOOLE_1:28;

end;

theorem :: AFINSQ_1:3

for b₁, b₂ being Nat holds
( b₁ = b₁ /\ b₂ implies b₁ <= b₂ ) by E2;

theorem E3: :: AFINSQ_1:4

for b₁ being Nat holds b₁ \/ {b₁} = b₁ + 1

proof

let c₁ be Nat;
c₁ + 1 = succ c₁ by CARD_1:52;
hence c₁ \/ {c₁} = c₁ + 1 by ORDINAL1:def 1;

end;

theorem E4: :: AFINSQ_1:5

for b₁ being Nat holds Seg b₁ c= b₁ + 1

proof

let c₁ be Nat;
let c₂ be set ; :: uses TARSKI:def 3
assume E5: c₂ in Seg c₁ ;
then reconsider c₃ = c₂ as Nat ;
( 1 <= c₃ & c₃ <= c₁ ) by E5, FINSEQ_1:3;
then c₃ < c₁ + 1 by NAT_1:38;
hence c₂ in c₁ + 1 by EULER_1:1;

end;

theorem :: AFINSQ_1:6

for b₁ being Nat holds b₁ + 1 = {0} \/ (Seg b₁)

proof

let c₁ be Nat;
thus c₁ + 1 c= {0} \/ (Seg c₁) :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ + 1 ;
then c₂ in { b₁ where B is Nat : b₁ < c₁ + 1 } by AXIOMS:30;
then consider c₃ being Nat such that
E5: ( c₃ = c₂ & c₃ < c₁ + 1 ) ;
( c₃ = 0 or ( 0 < c₃ & c₃ <= c₁ ) ) by E5, NAT_1:38;
then ( c₃ = 0 or ( 1 < c₃ + 1 & c₃ <= c₁ ) ) by XREAL_1:31;
then ( c₃ = 0 or ( 1 <= c₃ & c₃ <= c₁ ) ) by NAT_1:38;
then ( c₂ in {0} or c₂ in Seg c₁ ) by E5, FINSEQ_1:3, TARSKI:def 1;
hence c₂ in {0} \/ (Seg c₁) by XBOOLE_0:def 2;

end;

1 <= c₁ + 1 by NAT_1:29;
then E5: {0} c= c₁ + 1 by CARD_1:56, CARD_5:1;
Seg c₁ c= c₁ + 1 by E4;
hence {0} \/ (Seg c₁) c= c₁ + 1 by E5, XBOOLE_1:8;

end;

theorem E5: :: AFINSQ_1:7

for b₁ being Function holds
( ( b₁ is finite & b₁ is T-Sequence-like ) iff ex b₂ being Nat st dom b₁ = b₂ )

proof

let c₁ be Function;

hereby

assume ( c₁ is finite & c₁ is T-Sequence-like ) ;
then ( dom c₁ is finite & dom c₁ is Ordinal ) by FINSET_1:29, ORDINAL1:def 7;
then dom c₁ in NAT by CARD_4:7;
hence ex b₁ being Nat st dom c₁ = b₁ ;

end; assume ex b₁ being Nat st dom c₁ = b₁ ;
hence ( c₁ is finite & c₁ is T-Sequence-like ) by FINSET_1:29, ORDINAL1:def 7;

end;

registration

cluster T-Sequence-like finite set ;
existence

proof

take c₁ = {} ;
E6: for b₁ being set holds
( b₁ in {} implies c₁ . b₁ = 0 ) ;
dom c₁ = {} ;
hence ( c₁ is finite & c₁ is T-Sequence-like ) by E6, E5;

end;

definition

mode XFinSequence is finite T-Sequence;

end;

registration

cluster natural -> finite set ;
coherence

proof

let c₁ be set ;
assume c₁ in NAT ; :: uses ORDINAL2:def 21
then c₁ is Nat ;
hence c₁ is finite ;

end;

let c₁ be XFinSequence;
cluster dom a₁ -> natural ;
coherence

proof

ex b₁ being Nat st dom c₁ = b₁ by E5;
hence dom c₁ is natural ;

end;

notation

let c₁ be XFinSequence;

end;

definition

let c₁ be XFinSequence;
redefine func len as len a₁ -> Nat means :E6: :: AFINSQ_1:def 1
a₂ = dom a₁;
coherence

proof

len c₁ = card c₁ ;
hence len c₁ is Nat ;

end;

compatibility

proof

let c₂ be Nat;
consider c₃ being Nat such that
E6: dom c₁ = c₃ by E5;
dom c₁,c₁ are_equipotent

proof

deffunc H₁( set ) -> set = [a₁,(c₁ . a₁)];
consider c₄ being Function such that
E7: dom c₄ = dom c₁
and E8: for b₁ being set holds
( b₁ in dom c₁ implies c₄ . b₁ = H₁(b₁) ) from FUNCT_1:sch 3();
take c₄ ; :: uses WELLORD2:def 4
thus c₄ is one-to-one

proof

let c₅ be set ; :: uses FUNCT_1:def 8
let c₆ be set ;
assume E9: ( c₅ in dom c₄ & c₆ in dom c₄ ) ;
assume c₄ . c₅ = c₄ . c₆ ;
then [c₅,(c₁ . c₅)] = c₄ . c₆ by E7, E8, E9
.= [c₆,(c₁ . c₆)] by E7, E8, E9 ;
hence c₅ = c₆ by ZFMISC_1:33;

end;

thus dom c₄ = dom c₁ by E7;
thus rng c₄ c= c₁ :: uses XBOOLE_0:def 10

proof

let c₅ be set ; :: uses TARSKI:def 3
assume c₅ in rng c₄ ;
then consider c₆ being set such that
E9: c₆ in dom c₄
and E10: c₄ . c₆ = c₅ by FUNCT_1:def 5;
c₄ . c₆ = [c₆,(c₁ . c₆)] by E7, E8, E9;
hence c₅ in c₁ by E7, E9, E10, FUNCT_1:8;

end;

let c₅ be set ; :: uses TARSKI:def 3
assume E9: c₅ in c₁ ;
then consider c₆, c₇ being set such that
E10: c₅ = [c₆,c₇] by RELAT_1:def 1;
E11: ( c₆ in dom c₁ & c₇ = c₁ . c₆ ) by E9, E10, FUNCT_1:8;
then c₄ . c₆ = c₅ by E8, E10;
hence c₅ in rng c₄ by E7, E11, FUNCT_1:def 5;

end;

then E7: len c₁ = len (dom c₁) by CARD_1:21;
hence ( c₂ = len c₁ implies c₂ = dom c₁ ) by E6, CARD_1:66;
thus ( c₂ = dom c₁ implies c₂ = len c₁ ) by E7, CARD_1:66;

end;

:: deftheorem E6 defines len AFINSQ_1:def 1 :

definition

let c₁ be XFinSequence;
redefine func dom as dom a₁ -> Subset of NAT ;
coherence

proof

E7: dom c₁ = len c₁ by E6
.= { b₁ where B is Nat : b₁ < len c₁ } by AXIOMS:30 ;
{ b₁ where B is Nat : b₁ < len c₁ } c= NAT

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in { b₁ where B is Nat : b₁ < len c₁ } ;
then consider c₃ being Nat such that
E8: ( c₃ = c₂ & c₃ < len c₁ ) ;
thus c₂ in NAT by E8;

end;

hence dom c₁ is Subset of NAT by E7;

end;

theorem :: AFINSQ_1:8

for b₁ being Function holds
not ( ex b₂ being Nat st dom b₁ c= b₂ & for b₂ being XFinSequence holds
not b₁ c= b₂ )

proof

let c₁ be Function;
given c₂ being Nat such that E7: dom c₁ c= c₂ ;
deffunc H₁( set ) -> set = c₁ . a₁;
consider c₃ being Function such that
E8: ( dom c₃ = c₂ & for b₁ being set holds
( b₁ in c₂ implies c₃ . b₁ = H₁(b₁) ) ) from FUNCT_1:sch 3();
reconsider c₄ = c₃ as XFinSequence by E8, E5;
take c₄ ;
let c₅ be set ; :: uses TARSKI:def 3
assume E9: c₅ in c₁ ;
then consider c₆, c₇ being set such that
E10: [c₆,c₇] = c₅ by RELAT_1:def 1;
c₆ in dom c₁ by E9, E10, RELAT_1:def 4;
then ( c₆ in dom c₄ & c₁ . c₆ = c₇ ) by E7, E8, E9, E10, FUNCT_1:def 4;
then ( [c₆,(c₄ . c₆)] in c₄ & c₄ . c₆ = c₇ ) by E8, FUNCT_1:8;
hence c₅ in c₄ by E10;

end;

scheme :: AFINSQ_1:sch 1
s1{ F₁() -> Nat, P₁[ set , set ] } :

ex b₁ being XFinSequence st
( dom b₁ = F₁() & for b₂ being Nat holds
( b₂ in F₁() implies P₁[b₂,b₁ . b₂] ) )

provided

E7: for b₁ being Nat
for b₂, b₃ being set holds
( ( b₁ in F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] ) implies ( b₂ = b₃ ) ) and E8: for b₁ being Nat holds
not ( b₁ in F₁() & for b₂ being set holds
not P₁[b₁,b₂] )

proof

E9: for b₁, b₂, b₃ being set holds
( ( b₁ in F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] ) implies ( b₂ = b₃ ) )

proof

let c₁, c₂, c₃ be set ;
assume E10: ( c₁ in F₁() & P₁[c₁,c₂] & P₁[c₁,c₃] ) ;
F₁() = { b₁ where B is Nat : b₁ < F₁() } by AXIOMS:30;
then consider c₄ being Nat such that
E11: ( c₄ = c₁ & c₄ < F₁() ) by E10;
thus c₂ = c₃ by E7, E10, E11;

end;

E10: for b₁ being set holds
not ( b₁ in F₁() & for b₂ being set holds
not P₁[b₁,b₂] )

proof

let c₁ be set ;
assume E11: c₁ in F₁() ;
F₁() = { b₁ where B is Nat : b₁ < F₁() } by AXIOMS:30;
then consider c₂ being Nat such that
E12: ( c₂ = c₁ & c₂ < F₁() ) by E11;
thus ex b₁ being set st P₁[c₁,b₁] by E8, E11, E12;

end;

consider c₁ being Function such that
E11: ( dom c₁ = F₁() & for b₁ being set holds
( b₁ in F₁() implies P₁[b₁,c₁ . b₁] ) ) from FUNCT_1:sch 2(E9, E10);
reconsider c₂ = c₁ as XFinSequence by E11, E5;
take c₂ ;
thus ( dom c₂ = F₁() & for b₁ being Nat holds
( b₁ in F₁() implies P₁[b₁,c₂ . b₁] ) ) by E11;

end;

scheme :: AFINSQ_1:sch 2
s2{ F₁() -> Nat, F₂( set ) -> set } :

ex b₁ being XFinSequence st
( len b₁ = F₁() & for b₂ being Nat holds
( b₂ in F₁() implies b₁ . b₂ = F₂(b₂) ) )

provided

proof

consider c₁ being Function such that
E7: ( dom c₁ = F₁() & for b₁ being set holds
( b₁ in F₁() implies c₁ . b₁ = F₂(b₁) ) ) from FUNCT_1:sch 3();
reconsider c₂ = c₁ as XFinSequence by E7, E5;
take c₂ ;
thus ( len c₂ = F₁() & for b₁ being Nat holds
( b₁ in F₁() implies c₂ . b₁ = F₂(b₁) ) ) by E7, E6;

end;

theorem :: AFINSQ_1:9

for b₁ being set
for b₂ being XFinSequence holds
not ( b₁ in b₂ & for b₃ being Nat holds
not ( b₃ in dom b₂ & b₁ = [b₃,(b₂ . b₃)] ) )

proof

let c₁ be set ;
let c₂ be XFinSequence;
assume E7: c₁ in c₂ ;
then consider c₃, c₄ being set such that
E8: c₁ = [c₃,c₄] by RELAT_1:def 1;
c₃ in dom c₂ by E7, E8, FUNCT_1:8;
then reconsider c₅ = c₃ as Nat ;
take c₅ ;
thus ( c₅ in dom c₂ & c₁ = [c₅,(c₂ . c₅)] ) by E7, E8, FUNCT_1:8;

end;

theorem E7: :: AFINSQ_1:10

for b₁, b₂ being XFinSequence holds
( ( dom b₁ = dom b₂ & for b₃ being Nat holds
( b₃ in dom b₁ implies b₁ . b₃ = b₂ . b₃ ) ) implies ( b₁ = b₂ ) )

proof

let c₁, c₂ be XFinSequence;
assume E8: ( dom c₁ = dom c₂ & for b₁ being Nat holds
( b₁ in dom c₁ implies c₁ . b₁ = c₂ . b₁ ) ) ;
then for b₁ being set holds
( b₁ in dom c₁ implies c₁ . b₁ = c₂ . b₁ ) ;
hence c₁ = c₂ by E8, FUNCT_1:9;

end;

theorem :: AFINSQ_1:11

for b₁, b₂ being XFinSequence holds
( ( len b₁ = len b₂ & for b₃ being Nat holds
( b₃ < len b₁ implies b₁ . b₃ = b₂ . b₃ ) ) implies ( b₁ = b₂ ) )

proof

let c₁, c₂ be XFinSequence;
assume E8: ( len c₁ = len c₂ & for b₁ being Nat holds
( b₁ < len c₁ implies c₁ . b₁ = c₂ . b₁ ) ) ;
E9: ( dom c₁ = len c₁ & dom c₂ = len c₂ ) by E6;

now

let c₃ be set ;
assume E10: c₃ in dom c₁ ;
then reconsider c₄ = c₃ as Nat ;
c₄ < len c₁ by E9, E10, EULER_1:1;
hence c₁ . c₃ = c₂ . c₃ by E8;

end;

hence c₁ = c₂ by E8, E9, FUNCT_1:9;

end;

theorem E8: :: AFINSQ_1:12

for b₁ being Nat
for b₂ being XFinSequence holds
b₂ | b₁ is XFinSequence

proof

let c₁ be Nat;
let c₂ be XFinSequence;
E9: dom (c₂ | c₁) = (dom c₂) /\ c₁ by RELAT_1:90
.= (len c₂) /\ c₁ by E6 ;
( len c₂ <= c₁ or c₁ <= len c₂ ) ;
then ( dom (c₂ | c₁) = len c₂ or dom (c₂ | c₁) = c₁ ) by E9, E2;
hence c₂ | c₁ is XFinSequence by E5;

end;

theorem :: AFINSQ_1:13

for b₁ being Function
for b₂ being XFinSequence holds
( rng b₂ c= dom b₁ implies b₂ * b₁ is XFinSequence )

proof

let c₁ be Function;
let c₂ be XFinSequence;
assume rng c₂ c= dom c₁ ;
then dom (c₂ * c₁) = dom c₂ by RELAT_1:46
.= len c₂ by E6 ;
hence c₂ * c₁ is XFinSequence by E5;

end;

theorem :: AFINSQ_1:14

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
( ( b₃ = b₂ | b₁ ) implies ( not b₁ < len b₂ or ( len b₃ = b₁ & dom b₃ = b₁ ) ) )

proof

let c₁ be Nat;
let c₂, c₃ be XFinSequence;
assume E9: ( c₁ < len c₂ & c₃ = c₂ | c₁ ) ;
then c₁ c= len c₂ by CARD_1:56;
then c₁ c= dom c₂ by E6;
then dom c₃ = c₁ by E9, RELAT_1:91;
hence ( len c₃ = c₁ & dom c₃ = c₁ ) by E6;

end;

registration

let c₁ be set ;
cluster finite T-Sequence of a₁;
existence

proof

{} is T-Sequence of c₁ by ORDINAL1:45;
hence ex b₁ being T-Sequence of c₁ st b₁ is finite ;

end;

definition

let c₁ be set ;
mode XFinSequence is finite T-Sequence of a₁;

end;

theorem E9: :: AFINSQ_1:15

for b₁ being set
for b₂ being XFinSequence of b₁ holds
b₂ is PartFunc of NAT ,b₁

proof

let c₁ be set ;
let c₂ be XFinSequence of c₁;
E10: dom c₂ c= NAT ;
rng c₂ c= c₁ by ORDINAL1:def 8;
hence c₂ is PartFunc of NAT ,c₁ by E10, RELSET_1:11;

end;

registration

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

end;

registration

let c₁ be set ;
cluster T-Sequence-like finite M5( NAT ,a₁);
existence

proof

{} is PartFunc of NAT ,c₁ by PARTFUN1:56;
hence ex b₁ being PartFunc of NAT ,c₁ st
( b₁ is finite & b₁ is T-Sequence-like ) ;

end;

theorem :: AFINSQ_1:16

for b₁ being Nat
for b₂ being set
for b₃ being XFinSequence of b₂ holds
b₃ | b₁ is XFinSequence of b₂

proof

let c₁ be Nat;
let c₂ be set ;
let c₃ be XFinSequence of c₂;
( rng (c₃ | c₁) c= rng c₃ & rng c₃ c= c₂ ) by ORDINAL1:def 8;
then rng (c₃ | c₁) c= c₂ by XBOOLE_1:1;
hence c₃ | c₁ is XFinSequence of c₂ by E8, ORDINAL1:def 8;

end;

theorem :: AFINSQ_1:17

for b₁ being Nat
for b₂ being non empty set holds
ex b₃ being XFinSequence of b₂ st len b₃ = b₁

proof

let c₁ be Nat;
let c₂ be non empty set ;
consider c₃ being Element of c₂;
set c₄ = c₁ --> c₃;
E10: ( dom (c₁ --> c₃) = c₁ & for b₁ being Nat holds
( b₁ in c₁ implies (c₁ --> c₃) . b₁ = c₃ ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider c₅ = c₁ --> c₃ as XFinSequence by E5;
E11: rng c₅ c= {c₃} by FUNCOP_1:19;
{c₃} c= c₂ by ZFMISC_1:37;
then rng c₅ c= c₂ by E11, XBOOLE_1:1;
then reconsider c₆ = c₅ as XFinSequence of c₂ by ORDINAL1:def 8;
take c₆ ;
thus len c₆ = c₁ by E10, E6;

end;

registration

cluster empty set ;
existence by ORDINAL1:45;

end;

theorem E10: :: AFINSQ_1:18

for b₁ being XFinSequence holds
( len b₁ = 0 iff b₁ = {} )

proof

let c₁ be XFinSequence;
( len c₁ = 0 iff c₁, {} are_equipotent ) by CARD_1:def 5;
hence ( len c₁ = 0 iff c₁ = {} ) by CARD_1:46;

end;

theorem E11: :: AFINSQ_1:19

for b₁ being set holds
{} is XFinSequence of b₁

proof

let c₁ be set ;
rng {} c= c₁ by XBOOLE_1:2;
hence {} is XFinSequence of c₁ by ORDINAL1:def 8;

end;

registration

let c₁ be set ;
cluster empty T-Sequence of a₁;
existence

proof

{} is XFinSequence of c₁ by E11;
hence ex b₁ being XFinSequence of c₁ st b₁ is empty ;

end;

definition

let c₁ be set ;
func <%a₁%> -> set equals :: AFINSQ_1:def 2
{[0,a₁]};
coherence ;

end;

:: deftheorem defines <% AFINSQ_1:def 2 :

definition

let c₁ be set ;
func <%> a₁ -> empty XFinSequence of a₁ equals :: AFINSQ_1:def 3
{} ;
coherence by E11;

end;

:: deftheorem defines <%> AFINSQ_1:def 3 :

definition

let c₁, c₂ be XFinSequence;
means :E12: :: AFINSQ_1:def 4
( dom a₃ = (len a₁) + (len a₂) & for b₁ being Nat holds
( b₁ in dom a₁ implies a₃ . b₁ = a₁ . b₁ ) & for b₁ being Nat holds
( b₁ in dom a₂ implies a₃ . ((len a₁) + b₁) = a₂ . b₁ ) );
compatibility

proof

let c₃ be T-Sequence;
E12: ( len c₁ = dom c₁ & len c₂ = dom c₂ ) by E6;
E13: (len c₁) +^ (len c₂) = (len c₁) + (len c₂) by CARD_2:49;

hereby

assume E14: c₃ = c₁ ^ c₂ ;
hence dom c₃ = (len c₁) + (len c₂) by E12, E13, ORDINAL4:def 1;
thus for b₁ being Nat holds
( b₁ in dom c₁ implies c₃ . b₁ = c₁ . b₁ ) by E14, ORDINAL4:def 1;
let c₄ be Nat;
assume c₄ in dom c₂ ;
then c₃ . ((len c₁) +^ c₄) = c₂ . c₄ by E12, E14, ORDINAL4:def 1;
hence c₃ . ((len c₁) + c₄) = c₂ . c₄ by CARD_2:49;

end; assume that E14: dom c₃ = (len c₁) + (len c₂)
and E15: for b₁ being Nat holds
( b₁ in dom c₁ implies c₃ . b₁ = c₁ . b₁ )
and E16: for b₁ being Nat holds
( b₁ in dom c₂ implies c₃ . ((len c₁) + b₁) = c₂ . b₁ ) ;
E17: for b₁ being Ordinal holds
( b₁ in dom c₁ implies c₃ . b₁ = c₁ . b₁ ) by E15;

now

let c₄ be Ordinal;
assume E18: c₄ in dom c₂ ;
then reconsider c₅ = c₄ as Nat ;
thus c₃ . ((dom c₁) +^ c₄) = c₃ . ((len c₁) + c₅) by E12, CARD_2:49
.= c₂ . c₄ by E16, E18 ;

end;

hence c₃ = c₁ ^ c₂ by E12, E13, E14, E17, ORDINAL4:def 1;

end;

:: deftheorem E12 defines ^ AFINSQ_1:def 4 :

registration

let c₁, c₂ be XFinSequence;
cluster a₁ ^ a₂ -> finite ;
coherence

proof

dom (c₁ ^ c₂) = (dom c₁) +^ (dom c₂) by ORDINAL4:def 1;
then dom (c₁ ^ c₂) is Nat by ORDINAL2:def 21;
hence c₁ ^ c₂ is finite by E5;

end;

theorem E13: :: AFINSQ_1:20

for b₁, b₂ being XFinSequence holds len (b₁ ^ b₂) = (len b₁) + (len b₂)

proof

let c₁, c₂ be XFinSequence;
dom (c₁ ^ c₂) = (len c₁) + (len c₂) by E12;
hence len (c₁ ^ c₂) = (len c₁) + (len c₂) by E6;

end;

theorem E14: :: AFINSQ_1:21

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
( ( len b₂ <= b₁ ) implies ( not b₁ < (len b₂) + (len b₃) or (b₂ ^ b₃) . b₁ = b₃ . (b₁ - (len b₂)) ) )

proof

let c₁ be Nat;
let c₂, c₃ be XFinSequence;
assume E15: ( len c₂ <= c₁ & c₁ < (len c₂) + (len c₃) ) ;
then consider c₄ being Nat such that
E16: (len c₂) + c₄ = c₁ by NAT_1:28;
c₁ - (len c₂) < ((len c₂) + (len c₃)) - (len c₂) by E15, REAL_1:92;
then c₄ in len c₃ by E16, EULER_1:1;
then c₄ in dom c₃ by E6;
hence (c₂ ^ c₃) . c₁ = c₃ . (c₁ - (len c₂)) by E16, E12;

end;

theorem :: AFINSQ_1:22

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
( ( len b₂ <= b₁ ) implies ( not b₁ < len (b₂ ^ b₃) or (b₂ ^ b₃) . b₁ = b₃ . (b₁ - (len b₂)) ) )

proof

let c₁ be Nat;
let c₂, c₃ be XFinSequence;
assume E15: ( len c₂ <= c₁ & c₁ < len (c₂ ^ c₃) ) ;
then c₁ < (len c₂) + (len c₃) by E13;
hence (c₂ ^ c₃) . c₁ = c₃ . (c₁ - (len c₂)) by E15, E14;

end;

theorem E15: :: AFINSQ_1:23

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
not ( b₁ in dom (b₂ ^ b₃) & not b₁ in dom b₂ & for b₄ being Nat holds
not ( b₄ in dom b₃ & b₁ = (len b₂) + b₄ ) )

proof

let c₁ be Nat;
let c₂, c₃ be XFinSequence;
assume c₁ in dom (c₂ ^ c₃) ;
then c₁ in len (c₂ ^ c₃) by E6;
then c₁ in (len c₂) + (len c₃) by E13;
then E16: c₁ < (len c₂) + (len c₃) by EULER_1:1;

E17: now

assume not len c₂ <= c₁ ;
then c₁ in len c₂ by EULER_1:1;
hence not ( not c₁ in dom c₂ & for b₁ being Nat holds
not ( b₁ in dom c₃ & c₁ = (len c₂) + b₁ ) ) by E6;

end;

now

assume len c₂ <= c₁ ;
then consider c₄ being Nat such that
E18: c₁ = (len c₂) + c₄ by NAT_1:28;
(c₄ + (len c₂)) - (len c₂) < ((len c₃) + (len c₂)) - (len c₂) by E16, E18, REAL_1:92;
then c₄ in len c₃ by EULER_1:1;
then c₄ in dom c₃ by E6;
hence not ( not c₁ in dom c₂ & for b₁ being Nat holds
not ( b₁ in dom c₃ & c₁ = (len c₂) + b₁ ) ) by E18;

end;

hence not ( not c₁ in dom c₂ & for b₁ being Nat holds
not ( b₁ in dom c₃ & c₁ = (len c₂) + b₁ ) ) by E17;

end;

theorem E16: :: AFINSQ_1:24

for b₁, b₂ being T-Sequence holds dom b₁ c= dom (b₁ ^ b₂)

proof

let c₁, c₂ be T-Sequence;
dom (c₁ ^ c₂) = (dom c₁) +^ (dom c₂) by ORDINAL4:def 1;
hence dom c₁ c= dom (c₁ ^ c₂) by ORDINAL3:27;

end;

theorem E17: :: AFINSQ_1:25

for b₁ being set
for b₂, b₃ being XFinSequence holds
not ( b₁ in dom b₂ & for b₄ being Nat holds
not ( b₄ = b₁ & (len b₃) + b₄ in dom (b₃ ^ b₂) ) )

proof

let c₁ be set ;
let c₂, c₃ be XFinSequence;
assume E18: c₁ in dom c₂ ;
then E19: c₁ in len c₂ by E6;
reconsider c₄ = c₁ as Nat by E18;
take c₄ ;
c₄ < len c₂ by E19, EULER_1:1;
then (len c₃) + c₄ < (len c₃) + (len c₂) by XREAL_1:10;
then (len c₃) + c₄ in (len c₃) + (len c₂) by EULER_1:1;
hence ( c₄ = c₁ & (len c₃) + c₄ in dom (c₃ ^ c₂) ) by E12;

end;

theorem E18: :: AFINSQ_1:26

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
( b₁ in dom b₂ implies (len b₃) + b₁ in dom (b₃ ^ b₂) )

proof

let c₁ be Nat;
let c₂, c₃ be XFinSequence;
assume c₁ in dom c₂ ;
then ex b₁ being Nat st
( b₁ = c₁ & (len c₃) + b₁ in dom (c₃ ^ c₂) ) by E17;
hence (len c₃) + c₁ in dom (c₃ ^ c₂) ;

end;

theorem E19: :: AFINSQ_1:27

for b₁, b₂ being XFinSequence holds rng b₁ c= rng (b₁ ^ b₂)

proof

let c₁, c₂ be XFinSequence;

now

let c₃ be set ;
assume c₃ in rng c₁ ;
then consider c₄ being set such that
E20: ( c₄ in dom c₁ & c₃ = c₁ . c₄ ) by FUNCT_1:def 5;
reconsider c₅ = c₄ as Nat by E20;
E21: ( c₅ in dom c₁ & dom c₁ c= dom (c₁ ^ c₂) ) by E20, E16;
(c₁ ^ c₂) . c₅ = c₁ . c₅ by E20, E12;
hence c₃ in rng (c₁ ^ c₂) by E20, E21, FUNCT_1:12;

end;

hence rng c₁ c= rng (c₁ ^ c₂) by TARSKI:def 3;

end;

theorem E20: :: AFINSQ_1:28

for b₁, b₂ being XFinSequence holds rng b₁ c= rng (b₂ ^ b₁)

proof

let c₁, c₂ be XFinSequence;

now

let c₃ be set ;
assume c₃ in rng c₁ ;
then consider c₄ being set such that
E21: ( c₄ in dom c₁ & c₃ = c₁ . c₄ ) by FUNCT_1:def 5;
reconsider c₅ = c₄ as Nat by E21;
E22: (len c₂) + c₅ in dom (c₂ ^ c₁) by E21, E18;
(c₂ ^ c₁) . ((len c₂) + c₅) = c₁ . c₅ by E21, E12;
hence c₃ in rng (c₂ ^ c₁) by E21, E22, FUNCT_1:12;

end;

hence rng c₁ c= rng (c₂ ^ c₁) by TARSKI:def 3;

end;

theorem E21: :: AFINSQ_1:29

for b₁, b₂ being XFinSequence holds rng (b₁ ^ b₂) = (rng b₁) \/ (rng b₂)

proof

let c₁, c₂ be XFinSequence;

now

let c₃ be set ;
assume c₃ in rng (c₁ ^ c₂) ;
then consider c₄ being set such that
E22: ( c₄ in dom (c₁ ^ c₂) & c₃ = (c₁ ^ c₂) . c₄ ) by FUNCT_1:def 5;
E23: c₄ in (len c₁) + (len c₂) by E22, E12;
reconsider c₅ = c₄ as Nat by E22;
E24: c₅ < (len c₁) + (len c₂) by E23, EULER_1:1;

E25: now

assume E26: len c₁ <= c₅ ;
then E27: c₂ . (c₅ - (len c₁)) = c₃ by E22, E24, E14;
consider c₆ being Nat such that
E28: (len c₁) + c₆ = c₅ by E26, NAT_1:28;
(c₆ + (len c₁)) - (len c₁) < ((len c₁) + (len c₂)) - (len c₁) by E24, E28, REAL_1:92;
then c₆ in len c₂ by EULER_1:1;
then c₅ - (len c₁) in dom c₂ by E28, E6;
hence c₃ in rng c₂ by E27, FUNCT_1:12;

end;

now

assume not len c₁ <= c₅ ;
then c₅ in len c₁ by EULER_1:1;
then E26: c₅ in dom c₁ by E6;
then c₁ . c₅ = c₃ by E22, E12;
hence c₃ in rng c₁ by E26, FUNCT_1:12;

end;

hence c₃ in (rng c₁) \/ (rng c₂) by E25, XBOOLE_0:def 2;

end;

then E22: rng (c₁ ^ c₂) c= (rng c₁) \/ (rng c₂) by TARSKI:def 3;
( rng c₁ c= rng (c₁ ^ c₂) & rng c₂ c= rng (c₁ ^ c₂) ) by E19, E20;
then (rng c₁) \/ (rng c₂) c= rng (c₁ ^ c₂) by XBOOLE_1:8;
hence rng (c₁ ^ c₂) = (rng c₁) \/ (rng c₂) by E22, XBOOLE_0:def 10;

end;

theorem E22: :: AFINSQ_1:30

for b₁, b₂, b₃ being XFinSequence holds (b₁ ^ b₂) ^ b₃ = b₁ ^ (b₂ ^ b₃)

proof

let c₁, c₂, c₃ be XFinSequence;
E23: dom ((c₁ ^ c₂) ^ c₃) = (len (c₁ ^ c₂)) + (len c₃) by E12
.= ((len c₁) + (len c₂)) + (len c₃) by E13
.= (len c₁) + ((len c₂) + (len c₃))
.= (len c₁) + (len (c₂ ^ c₃)) by E13 ;
E24: for b₁ being Nat holds
( b₁ in dom c₁ implies ((c₁ ^ c₂) ^ c₃) . b₁ = c₁ . b₁ )

proof

let c₄ be Nat;
assume E25: c₄ in dom c₁ ;
dom c₁ c= dom (c₁ ^ c₂) by E16;
hence ((c₁ ^ c₂) ^ c₃) . c₄ = (c₁ ^ c₂) . c₄ by E25, E12
.= c₁ . c₄ by E25, E12 ;

end;

for b₁ being Nat holds
( b₁ in dom (c₂ ^ c₃) implies ((c₁ ^ c₂) ^ c₃) . ((len c₁) + b₁) = (c₂ ^ c₃) . b₁ )

proof

let c₄ be Nat;
assume E25: c₄ in dom (c₂ ^ c₃) ;

E26: now

assume E27: c₄ in dom c₂ ;
then (len c₁) + c₄ in dom (c₁ ^ c₂) by E18;
hence ((c₁ ^ c₂) ^ c₃) . ((len c₁) + c₄) = (c₁ ^ c₂) . ((len c₁) + c₄) by E12
.= c₂ . c₄ by E27, E12
.= (c₂ ^ c₃) . c₄ by E27, E12 ;

end;

now

assume not c₄ in dom c₂ ;
then consider c₅ being Nat such that
E27: ( c₅ in dom c₃ & c₄ = (len c₂) + c₅ ) by E25, E15;
thus ((c₁ ^ c₂) ^ c₃) . ((len c₁) + c₄) = ((c₁ ^ c₂) ^ c₃) . (((len c₁) + (len c₂)) + c₅) by E27
.= ((c₁ ^ c₂) ^ c₃) . ((len (c₁ ^ c₂)) + c₅) by E13
.= c₃ . c₅ by E27, E12
.= (c₂ ^ c₃) . c₄ by E27, E12 ;

end;

hence ((c₁ ^ c₂) ^ c₃) . ((len c₁) + c₄) = (c₂ ^ c₃) . c₄ by E26;

end;

hence (c₁ ^ c₂)