set D = F₂() ^omega ;
reconsider s0 = F₃() as Element of F₂() by A0;
reconsider f0 = <%s0%> as Element of F₂() ^omega by AFINSQ_1:42;
defpred S₉[ set , Element of F₂() ^omega , Element of F₂() ^omega ] means ( ( ( $2 = {} or F₁((last $2)) = {} ) implies $2 = $3 ) & ( $2 <> {} & F₁((last $2)) <> {} implies ex y being Element of F₂() st
( P₁[ last $2,y] & F₁(y) c< F₁((last $2)) & $2 ^ <%y%> = $3 ) ) );
A3: for a being Element of NAT
for x being Element of F₂() ^omega ex y being Element of F₂() ^omega st S₉[a,x,y]

proof

let a be Element of NAT ; :: thesis: for x being Element of F₂() ^omega ex y being Element of F₂() ^omega st S₉[a,x,y]
let x be Element of F₂() ^omega ; :: thesis: ex y being Element of F₂() ^omega st S₉[a,x,y]

per cases ( x = {} or F₁((last x)) = {} or ( x <> {} & F₁((last x)) <> {} ) ) ;

suppose C1: ( x = {} or F₁((last x)) = {} ) ; :: thesis: ex y being Element of F₂() ^omega st S₉[a,x,y]

take y = x; :: thesis: S₉[a,x,y]
thus S₉[a,x,y] by C1; :: thesis: verum

end;

suppose C2: ( x <> {} & F₁((last x)) <> {} ) ; :: thesis: ex y being Element of F₂() ^omega st S₉[a,x,y]

then last x in F₂() by Lem3;
then consider y being Element of F₂() such that
C3: ( P₁[ last x,y] & F₁(y) c< F₁((last x)) ) by A2, C2;
reconsider z = x ^ <%y%> as Element of F₂() ^omega by AFINSQ_1:42;
take z ; :: thesis: S₉[a,x,z]
thus S₉[a,x,z] by C2, C3; :: thesis: verum

end;

end;

end;

consider F being Function of NAT,(F₂() ^omega) such that
B1: ( F . 0 = f0 & ( for a being Element of NAT holds S₉[a,F . a,F . (a + 1)] ) ) from RECDEF_1:sch 2(A3);
defpred S₁₀[ Nat] means F . $1 <> {} ;
B8: S₁₀[ 0 ] by B1;
B9: for m being natural number st S₁₀[m] holds
S₁₀[m + 1]

proof

let m be natural number ; :: thesis: ( S₁₀[m] implies S₁₀[m + 1] )
assume S₁₀[m] ; :: thesis: S₁₀[m + 1]
then reconsider f = F . m as non empty T-Sequence ;
m in NAT by ORDINAL1:def 12;
then S₉[m,F . m,F . (m + 1)] by B1;
then ( F . (m + 1) = f or ex x being set st F . (m + 1) = f ^ <%x%> ) ;
hence S₁₀[m + 1] ; :: thesis: verum

end;

N0: for m being natural number holds S₁₀[m] from NAT_1:sch 2(B8, B9);
defpred S₁₁[ Function] means ( $1 . 0 = F₃() & ( for a being ordinal number st succ a in dom $1 holds
ex x, y being Element of F₂() st
( x = $1 . a & y = $1 . (succ a) & P₁[x,y] ) ) );
defpred S₁₂[ Nat] means S₁₁[F . $1];
D1: S₁₂[ 0 ]

proof

thus (F . 0) . 0 = F₃() by B1, AFINSQ_1:def 4; :: thesis: for a being ordinal number st succ a in dom (F . 0) holds
ex x, y being Element of F₂() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P₁[x,y] )
let a be ordinal number ; :: thesis: ( succ a in dom (F . 0) implies ex x, y being Element of F₂() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P₁[x,y] ) )
assume succ a in dom (F . 0) ; :: thesis: ex x, y being Element of F₂() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P₁[x,y] )
then succ a in 1 by B1, AFINSQ_1:def 4;
hence ex x, y being Element of F₂() st
( x = (F . 0) . a & y = (F . 0) . (succ a) & P₁[x,y] ) by CARD_1:49, TARSKI:def 1; :: thesis: verum

end;

D2: for m being natural number st S₁₂[m] holds
S₁₂[m + 1]

proof

let m be natural number ; :: thesis: ( S₁₂[m] implies S₁₂[m + 1] )
assume F1: S₁₂[m] ; :: thesis: S₁₂[m + 1]
F0: m in NAT by ORDINAL1:def 12;
then F2: S₉[m,F . m,F . (m + 1)] by B1;

per cases ( F . m = {} or F₁((last (F . m))) = {} or ( F . m <> {} & F₁((last (F . m))) <> {} ) ) ;

suppose ( F . m = {} or F₁((last (F . m))) = {} ) ; :: thesis: S₁₂[m + 1]

hence S₁₂[m + 1] by F1, F2; :: thesis: verum

end;

suppose F3: ( F . m <> {} & F₁((last (F . m))) <> {} ) ; :: thesis: S₁₂[m + 1]

reconsider fm = F . m as non empty finite T-Sequence of by F3;
reconsider fm1 = F . (m + 1) as finite T-Sequence of ;
consider y being Element of F₂() such that
F4: ( P₁[ last fm,y] & F₁(y) c< F₁((last fm)) & fm ^ <%y%> = F . (m + 1) ) by B1, F0, F3;
0 in dom fm by ORDINAL3:8;
hence (F . (m + 1)) . 0 = F₃() by F1, F4, ORDINAL4:def 1; :: thesis: for a being ordinal number st succ a in dom (F . (m + 1)) holds
ex x, y being Element of F₂() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P₁[x,y] )
let a be ordinal number ; :: thesis: ( succ a in dom (F . (m + 1)) implies ex x, y being Element of F₂() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P₁[x,y] ) )
assume F5: succ a in dom (F . (m + 1)) ; :: thesis: ex x, y being Element of F₂() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P₁[x,y] )
F7: a in succ a by ORDINAL1:6;
then F6: a in dom fm1 by F5, ORDINAL1:10;
reconsider n = a as Nat by F5, F7;
reconsider x = fm1 . a, z = fm1 . (succ a) as Element of F₂() by F5, F6, FUNCT_1:102;
F8: dom <%y%> = 1 by AFINSQ_1:def 4;
then dom fm1 = (dom fm) +^ 1 by F4, ORDINAL4:def 1
.= succ (dom fm) by ORDINAL2:31 ;
then F9: a in dom fm by F5, ORDINAL3:3;
take x ; :: thesis: ex y being Element of F₂() st
( x = (F . (m + 1)) . a & y = (F . (m + 1)) . (succ a) & P₁[x,y] )
take z ; :: thesis: ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) & P₁[x,z] )
thus ( x = (F . (m + 1)) . a & z = (F . (m + 1)) . (succ a) ) ; :: thesis: P₁[x,z]

per cases ( succ a in dom fm or dom fm c= succ a ) by ORDINAL6:4;

suppose G1: succ a in dom fm ; :: thesis: P₁[x,z]

then a in dom fm by F7, ORDINAL1:10;
then G2: ( x = fm . a & z = fm . (succ a) ) by F4, G1, ORDINAL4:def 1;
ex x, y being Element of F₂() st
( x = fm . a & y = fm . (succ a) & P₁[x,y] ) by F1, G1;
hence P₁[x,z] by G2; :: thesis: verum

end;

suppose G3: dom fm c= succ a ; :: thesis: P₁[x,z]

succ a c= dom fm by F9, ORDINAL1:21;
then G4: dom fm = succ a by G3, XBOOLE_0:def 10;
then union (dom fm) = a by ORDINAL2:2;
then G5: last fm = fm1 . a by F4, F9, ORDINAL4:def 1;
( 0 in 1 & (succ a) +^ 0 = succ a ) by NAT_1:44, ORDINAL2:27;
then z = <%y%> . 0 by F8, F4, G4, ORDINAL4:def 1;
hence P₁[x,z] by F4, G5, AFINSQ_1:def 4; :: thesis: verum

end;

end;

end;

end;

end;

D3: for m being natural number holds S₁₂[m] from NAT_1:sch 2(D1, D2);
defpred S₁₃[ Nat] means ex n being natural number st card F₁((last (F . n))) = $1;
B3: ex n being natural number st S₁₃[n]

proof

last f0 = s0 by Lem4;
then reconsider n = card F₁((last (F . 0))) as Nat by A1, B1;
take n ; :: thesis: S₁₃[n]
thus S₁₃[n] ; :: thesis: verum

end;

B4: for n being natural number st n <> 0 & S₁₃[n] holds
ex m being natural number st
( m < n & S₁₃[m] )

proof

let n be natural number ; :: thesis: ( n <> 0 & S₁₃[n] implies ex m being natural number st
( m < n & S₁₃[m] ) )
assume Z0: n <> 0 ; :: thesis: ( not S₁₃[n] or ex m being natural number st
( m < n & S₁₃[m] ) )
given k being Nat such that Z1: card F₁((last (F . k))) = n ; :: thesis: ex m being natural number st
( m < n & S₁₃[m] )
reconsider fk = F . k, fk1 = F . (k + 1) as Element of F₂() ^omega ;
k in NAT by ORDINAL1:def 12;
then ( S₉[k,fk,fk1] & fk <> {} ) by N0, B1;
then consider y being Element of F₂() such that
H1: ( P₁[ last fk,y] & F₁(y) c< F₁((last fk)) & fk ^ <%y%> = fk1 ) by Z0, Z1;
H4: ( F₁((last fk)) is finite & F₁(y) c= F₁((last fk)) ) by Z1, H1, XBOOLE_0:def 8;
H3: last fk1 = y by H1, Lem5;
then reconsider m = card F₁((last fk1)) as Nat by H4;
take m ; :: thesis: ( m < n & S₁₃[m] )
thus m < n by Z1, H1, H4, H3, TREES_1:6; :: thesis: S₁₃[m]
thus S₁₃[m] ; :: thesis: verum

end;

S₁₃[ 0 ] from NAT_1:sch 7(B3, B4);
then consider n being natural number such that
B6: card F₁((last (F . n))) = 0 ;
reconsider f = F . n as non empty XFinSequence of by N0;
take f ; :: thesis: ex k being Element of F₂() st
( k = last f & F₁(k) = {} & f . 0 = F₃() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F₂() st
( x = f . a & y = f . (succ a) & P₁[x,y] ) ) )
reconsider k = last f as Element of F₂() by Lem3;
take k ; :: thesis: ( k = last f & F₁(k) = {} & f . 0 = F₃() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F₂() st
( x = f . a & y = f . (succ a) & P₁[x,y] ) ) )
thus ( k = last f & F₁(k) = {} ) by B6; :: thesis: ( f . 0 = F₃() & ( for a being ordinal number st succ a in dom f holds
ex x, y being Element of F₂() st
( x = f . a & y = f . (succ a) & P₁[x,y] ) ) )
thus S₁₁[f] by D3; :: thesis: verum