set D = F₂() ^omega ;
reconsider s0 = F₃() as Element of F₂() by A1;
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 ) ) );
A4: for a being Nat
for x being Element of F₂() ^omega ex y being Element of F₂() ^omega st S₉[a,x,y]

proof

let a be 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 A5: ( 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 A5; :: thesis: verum

end;

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

then last x in F₂() by Th79;
then consider y being Element of F₂() such that
A7: ( P₁[ last x,y] & F₁(y) c< F₁((last x)) ) by A3, A6;
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 A6, A7; :: thesis: verum

end;

end;

end;

consider F being sequence of (F₂() ^omega) such that
A8: ( F . 0 = f0 & ( for a being Nat holds S₉[a,F . a,F . (a + 1)] ) ) from RECDEF_1:sch 2(A4);
defpred S₁₀[ Nat] means F . $1 <> {} ;
A9: S₁₀[ 0 ] by A8;
A10: for m being Nat st S₁₀[m] holds
S₁₀[m + 1]

proof

let m be Nat; :: thesis: ( S₁₀[m] implies S₁₀[m + 1] )
assume S₁₀[m] ; :: thesis: S₁₀[m + 1]
then reconsider f = F . m as non empty Sequence ;
S₉[m,F . m,F . (m + 1)] by A8;
then ( F . (m + 1) = f or ex x being set st F . (m + 1) = f ^ <%x%> ) ;
hence S₁₀[m + 1] ; :: thesis: verum

end;

A11: for m being Nat holds S₁₀[m] from NAT_1:sch 2(A9, A10);
defpred S₁₁[ Function] means ( $1 . 0 = F₃() & ( for a being Ordinal 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];
A12: S₁₂[ 0 ]

proof

thus (F . 0) . 0 = F₃() by A8; :: thesis: for a being Ordinal 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; :: 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 A8, 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;

A13: for m being Nat st S₁₂[m] holds
S₁₂[m + 1]

proof

let m be Nat; :: thesis: ( S₁₂[m] implies S₁₂[m + 1] )
assume A14: S₁₂[m] ; :: thesis: S₁₂[m + 1]
A15: S₉[m,F . m,F . (m + 1)] by A8;

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 A14, A15; :: thesis: verum

end;

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

reconsider fm = F . m as non empty finite Sequence of F₂() by A16;
reconsider fm1 = F . (m + 1) as finite Sequence of F₂() ;
consider y being Element of F₂() such that
A17: ( P₁[ last fm,y] & F₁(y) c< F₁((last fm)) & fm ^ <%y%> = F . (m + 1) ) by A8, A16;
0 in dom fm by ORDINAL3:8;
hence (F . (m + 1)) . 0 = F₃() by A14, A17, ORDINAL4:def 1; :: thesis: for a being Ordinal 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; :: 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 A18: 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] )
A19: a in succ a by ORDINAL1:6;
then A20: a in dom fm1 by A18, ORDINAL1:10;
then reconsider n = a as Nat ;
reconsider x = fm1 . a, z = fm1 . (succ a) as Element of F₂() by A18, A20, FUNCT_1:102;
A21: dom <%y%> = 1 by AFINSQ_1:def 4;
then dom fm1 = (dom fm) +^ 1 by A17, ORDINAL4:def 1
.= succ (dom fm) by ORDINAL2:31 ;
then A22: a in dom fm by A18, 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 A23: succ a in dom fm ; :: thesis: P₁[x,z]

then a in dom fm by A19, ORDINAL1:10;
then A24: ( x = fm . a & z = fm . (succ a) ) by A17, A23, ORDINAL4:def 1;
ex x, y being Element of F₂() st
( x = fm . a & y = fm . (succ a) & P₁[x,y] ) by A14, A23;
hence P₁[x,z] by A24; :: thesis: verum

end;

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

succ a c= dom fm by A22, ORDINAL1:21;
then A26: dom fm = succ a by A25;
then union (dom fm) = a by ORDINAL2:2;
then A27: last fm = fm1 . a by A17, A22, ORDINAL4:def 1;
( 0 in Segm 1 & (succ a) +^ 0 = succ a ) by NAT_1:44, ORDINAL2:27;
then z = <%y%> . 0 by A21, A17, A26, ORDINAL4:def 1;
hence P₁[x,z] by A17, A27; :: thesis: verum

end;

end;

end;

end;

end;

A28: for m being Nat holds S₁₂[m] from NAT_1:sch 2(A12, A13);
defpred S₁₃[ Nat] means ex n being Nat st card F₁((last (F . n))) = $1;
A29: ex n being Nat st S₁₃[n]

proof

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

end;

A30: for n being Nat st n <> 0 & S₁₃[n] holds
ex m being Nat st
( m < n & S₁₃[m] )

proof

let n be Nat; :: thesis: ( n <> 0 & S₁₃[n] implies ex m being Nat st
( m < n & S₁₃[m] ) )
assume A31: n <> 0 ; :: thesis: ( not S₁₃[n] or ex m being Nat st
( m < n & S₁₃[m] ) )
given k being Nat such that A32: card F₁((last (F . k))) = n ; :: thesis: ex m being Nat st
( m < n & S₁₃[m] )
reconsider fk = F . k, fk1 = F . (k + 1) as Element of F₂() ^omega ;
( S₉[k,fk,fk1] & fk <> {} ) by A11, A8;
then consider y being Element of F₂() such that
A33: ( P₁[ last fk,y] & F₁(y) c< F₁((last fk)) & fk ^ <%y%> = fk1 ) by A31, A32;
A34: ( F₁((last fk)) is finite & F₁(y) c= F₁((last fk)) ) by A32, A33;
A35: last fk1 = y by A33, Th81;
then reconsider m = card F₁((last fk1)) as Nat by A34;
take m ; :: thesis: ( m < n & S₁₃[m] )
thus m < n by A32, A33, A34, A35, TREES_1:6; :: thesis: S₁₃[m]
thus S₁₃[m] ; :: thesis: verum

end;

S₁₃[ 0 ] from NAT_1:sch 7(A29, A30);
then consider n being Nat such that
A36: card F₁((last (F . n))) = 0 ;
reconsider f = F . n as non empty XFinSequence of F₂() by A11;
take f ; :: thesis: ex k being Element of F₂() st
( k = last f & F₁(k) = {} & f . 0 = F₃() & ( for a being Ordinal 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 Th79;
take k ; :: thesis: ( k = last f & F₁(k) = {} & f . 0 = F₃() & ( for a being Ordinal 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 A36; :: thesis: ( f . 0 = F₃() & ( for a being Ordinal 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 A28; :: thesis: verum