now

assume not F₂() is finite ; :: thesis: contradiction
then not dom F₂() is finite by FINSET_1:29;
then consider B being Branch of dom F₂() such that
A2: not B is finite by Th22;
defpred S₁[ set ] means ex t being Element of dom F₂() st
( t in B & $1 = F₂() . t );
defpred S₂[ set , set ] means ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & $1 = F₂() . t & $2 = F₂() . t' );
A3: ( F₂() . {} in F₁() & S₁[F₂() . {} ] )

proof

{} in B by TREES_2:28;
then S₁[F₂() . {} ] ;
hence ( F₂() . {} in F₁() & S₁[F₂() . {} ] ) ; :: thesis: verum

end;

A4: for x being set st x in F₁() & S₁[x] holds
ex y being set st
( y in F₁() & S₂[x,y] & S₁[y] )

proof

let x be set ; :: thesis: ( x in F₁() & S₁[x] implies ex y being set st
( y in F₁() & S₂[x,y] & S₁[y] ) )
assume ( x in F₁() & S₁[x] ) ; :: thesis: ex y being set st
( y in F₁() & S₂[x,y] & S₁[y] )
then consider t being Element of dom F₂() such that
A5: ( t in B & x = F₂() . t ) ;
consider t' being Element of dom F₂() such that
A6: ( t' in B & t' in succ t ) by A2, A5, Th24;
ex y being set st y = F₂() . t' ;
hence ex y being set st
( y in F₁() & S₂[x,y] & S₁[y] ) by A5, A6; :: thesis: verum

end;

ex g being Function st
( dom g = NAT & rng g c= F₁() & g . 0 = F₂() . {} & ( for k being Element of NAT holds
( S₂[g . k,g . (k + 1)] & S₁[g . k] ) ) ) from TREES_2:sch 5(A3, A4);
then consider g being Function such that
A7: ( dom g = NAT & rng g c= F₁() & g . 0 = F₂() . {} & ( for k being Element of NAT holds
( ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & g . k = F₂() . t & g . (k + 1) = F₂() . t' ) & ex t being Element of dom F₂() st
( t in B & g . k = F₂() . t ) ) ) ) ;
defpred S₃[ set , set ] means ex d being Element of F₁() st
( d = g . $1 & $2 = F₃(d) );
A8: for x being set st x in NAT holds
ex y being set st
( y in NAT & S₃[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in NAT & S₃[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in NAT & S₃[x,y] )
then reconsider k = x as Element of NAT ;
consider t being Element of dom F₂() such that
A9: ( t in B & g . k = F₂() . t ) by A7;
consider y being set such that
A10: y = F₃((F₂() . t)) ;
thus ex y being set st
( y in NAT & S₃[x,y] ) by A9, A10; :: thesis: verum

end;

ex f being Function of NAT , NAT st
for x being set st x in NAT holds
S₃[x,f . x] from FUNCT_2:sch 1(A8);
then consider f being Function of NAT , NAT such that
A11: for x being set st x in NAT holds
ex d being Element of F₁() st
( d = g . x & f . x = F₃(d) ) ;
A12: ( ex d being Element of F₁() st
( d = F₂() . {} & f . 0 = F₃(d) ) & ( for k being Element of NAT ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & f . k = F₃((F₂() . t)) & f . (k + 1) = F₃((F₂() . t')) ) ) )

proof

thus ex d being Element of F₁() st
( d = F₂() . {} & f . 0 = F₃(d) ) by A7, A11; :: thesis: for k being Element of NAT ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & f . k = F₃((F₂() . t)) & f . (k + 1) = F₃((F₂() . t')) )
thus for k being Element of NAT ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & f . k = F₃((F₂() . t)) & f . (k + 1) = F₃((F₂() . t')) ) :: thesis: verum

proof

let k be Element of NAT ; :: thesis: ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & f . k = F₃((F₂() . t)) & f . (k + 1) = F₃((F₂() . t')) )
consider d being Element of F₁() such that
A13: ( d = g . k & f . k = F₃(d) ) by A11;
consider d1 being Element of F₁() such that
A14: ( d1 = g . (k + 1) & f . (k + 1) = F₃(d1) ) by A11;
consider t, t' being Element of dom F₂() such that
A15: ( t' in succ t & t in B & t' in B & g . k = F₂() . t & g . (k + 1) = F₂() . t' ) by A7;
thus ex t, t' being Element of dom F₂() st
( t' in succ t & t in B & t' in B & f . k = F₃((F₂() . t)) & f . (k + 1) = F₃((F₂() . t')) ) by A13, A14, A15; :: thesis: verum

end;

end;

A16: for n being Element of NAT ex t, t' being Element of dom F₂() st
( t' in succ t & f . n = F₃((F₂() . t)) & f . (n + 1) = F₃((F₂() . t')) & f . (n + 1) < f . n )

proof

let n be Element of NAT ; :: thesis: ex t, t' being Element of dom F₂() st
( t' in succ t & f . n = F₃((F₂() . t)) & f . (n + 1) = F₃((F₂() . t')) & f . (n + 1) < f . n )
consider t, t' being Element of dom F₂() such that
A17: ( t' in succ t & t in B & t' in B & f . n = F₃((F₂() . t)) & f . (n + 1) = F₃((F₂() . t')) ) by A12;
thus ex t, t' being Element of dom F₂() st
( t' in succ t & f . n = F₃((F₂() . t)) & f . (n + 1) = F₃((F₂() . t')) & f . (n + 1) < f . n ) by A1, A17; :: thesis: verum

end;

ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m

proof

for n being Element of NAT holds f . (n + 1) <= f . n

proof

let n be Element of NAT ; :: thesis: f . (n + 1) <= f . n
consider t, t' being Element of dom F₂() such that
A18: ( t' in succ t & f . n = F₃((F₂() . t)) & f . (n + 1) = F₃((F₂() . t')) & f . (n + 1) < f . n ) by A16;
thus f . (n + 1) <= f . n by A18; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st m <= n holds
f . n = f . m by Th25; :: thesis: verum

end;

then consider m being Element of NAT such that
A19: for n being Element of NAT st m <= n holds
f . n = f . m ;
consider k being Element of NAT such that
A20: k = m + 1 ;
consider t, t' being Element of dom F₂() such that
A21: ( t' in succ t & f . m = F₃((F₂() . t)) & f . (m + 1) = F₃((F₂() . t')) & f . (m + 1) < f . m ) by A16;
m <= k

proof

m + 0 <= m + 1 by XREAL_1:8;
hence m <= k by A20; :: thesis: verum

end;

hence contradiction by A19, A20, A21; :: thesis: verum

end;

hence F₂() is finite ; :: thesis: verum