now :: thesis: F2() is finite
assume not F2() is finite ; :: thesis: contradiction
then not dom F2() is finite by FINSET_1:10;
then consider B being Branch of dom F2() such that
A2: not B is finite by Th49;
defpred S1[ object , object ] means ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & $1 = F2() . t & $2 = F2() . t9 );
defpred S2[ object ] means ex t being Element of dom F2() st
( t in B & $1 = F2() . t );
A3: for x being object st x in F1() & S2[x] holds
ex y being object st
( y in F1() & S1[x,y] & S2[y] )
proof
let x be object ; :: thesis: ( x in F1() & S2[x] implies ex y being object st
( y in F1() & S1[x,y] & S2[y] ) )
assume that
x in F1() and
A4: S2[x] ; :: thesis: ex y being object st
( y in F1() & S1[x,y] & S2[y] )
consider t being Element of dom F2() such that
A5: t in B and
A6: x = F2() . t by A4;
consider t9 being Element of dom F2() such that
A7: ( t9 in B & t9 in succ t ) by A2, A5, Th51;
ex y being set st y = F2() . t9 ;
hence ex y being object st
( y in F1() & S1[x,y] & S2[y] ) by A5, A6, A7; :: thesis: verum
end;
{} in B by TREES_2:26;
then S2[F2() . {}] ;
then A8: ( F2() . {} in F1() & S2[F2() . {}] ) ;
ex g being Function st
( dom g = NAT & rng g c= F1() & g . 0 = F2() . {} & ( for k being Nat holds
( S1[g . k,g . (k + 1)] & S2[g . k] ) ) ) from TREES_2:sch 5(A8, A3);
then consider g being Function such that
dom g = NAT and
rng g c= F1() and
g . 0 = F2() . {} and
A9: for k being Nat holds
( ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & g . k = F2() . t & g . (k + 1) = F2() . t9 ) & ex t being Element of dom F2() st
( t in B & g . k = F2() . t ) ) ;
defpred S3[ object , object ] means ex d being Element of F1() st
( d = g . $1 & $2 = F3(d) );
A10: for x being object st x in NAT holds
ex y being object st
( y in NAT & S3[x,y] )
proof
let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in NAT & S3[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in NAT & S3[x,y] )
then reconsider k = x as Element of NAT ;
consider t being Element of dom F2() such that
t in B and
A11: g . k = F2() . t by A9;
reconsider y = F3((F2() . t)) as set ;
take y ; :: thesis: ( y in NAT & S3[x,y] )
y in NAT by ORDINAL1:def 12;
hence ( y in NAT & S3[x,y] ) by A11; :: thesis: verum
end;
ex f being sequence of NAT st
for x being object st x in NAT holds
S3[x,f . x] from FUNCT_2:sch 1(A10);
then consider f being sequence of NAT such that
A12: for x being object st x in NAT holds
ex d being Element of F1() st
( d = g . x & f . x = F3(d) ) ;
A13: for k being Nat ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) )
proof
let k be Nat; :: thesis: ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) )
A14: ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & g . k = F2() . t & g . (k + 1) = F2() . t9 ) by A9;
k in NAT by ORDINAL1:def 12;
then ( ex d being Element of F1() st
( d = g . k & f . k = F3(d) ) & ex d1 being Element of F1() st
( d1 = g . (k + 1) & f . (k + 1) = F3(d1) ) ) by A12;
hence ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . k = F3((F2() . t)) & f . (k + 1) = F3((F2() . t9)) ) by A14; :: thesis: verum
end;
A15: for n being Nat ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n )
proof
let n be Nat; :: thesis: ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n )
ex t, t9 being Element of dom F2() st
( t9 in succ t & t in B & t9 in B & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) ) by A13;
hence ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n ) by A1; :: thesis: verum
end;
for n being Nat holds f . (n + 1) <= f . n
proof
let n be Nat; :: thesis: f . (n + 1) <= f . n
ex t, t9 being Element of dom F2() st
( t9 in succ t & f . n = F3((F2() . t)) & f . (n + 1) = F3((F2() . t9)) & f . (n + 1) < f . n ) by A15;
hence f . (n + 1) <= f . n ; :: thesis: verum
end;
then consider m being Nat such that
A16: for n being Nat st m <= n holds
f . n = f . m by Th52;
A17: m + 0 <= m + 1 by XREAL_1:6;
ex t, t9 being Element of dom F2() st
( t9 in succ t & f . m = F3((F2() . t)) & f . (m + 1) = F3((F2() . t9)) & f . (m + 1) < f . m ) by A15;
hence contradiction by A16, A17; :: thesis: verum
end;
hence F2() is finite ; :: thesis: verum