deffunc H1( set ) -> set = F2((F1() . $1));
consider F being Sequence such that
A3: ( dom F = dom F1() & ( for a being Ordinal st a in dom F1() holds
F . a = H1(a) ) ) from ORDINAL2:sch 2();
per cases ( dom F in omega or omega c= dom F ) by ORDINAL6:4;
suppose dom F in omega ; :: thesis: F1() is finite
hence F1() is finite by A3, FINSET_1:10; :: thesis: verum
end;
suppose A4: omega c= dom F ; :: thesis: F1() is finite
set f = F | omega;
A5: dom (F | omega) = omega by A4, RELAT_1:62;
A6: len- (F | omega) = dom (F | omega) by Th24;
A7: (F | omega) . 0 = F . 0 by A5, FUNCT_1:47
.= H1( 0 ) by A3, A4 ;
defpred S9[ Nat] means (F | omega) . $1 is finite ;
A8: S9[ 0 ] by A1, A7;
A9: for n being Nat st S9[n] holds
S9[n + 1]
proof
let n be Nat; :: thesis: ( S9[n] implies S9[n + 1] )
set a = n;
assume A10: S9[n] ; :: thesis: S9[n + 1]
A11: ( n in omega & succ n in omega ) by ORDINAL1:def 12;
then A12: ( n in dom F & succ n in dom F & (F | omega) . n = F . n & (F | omega) . (succ n) = F . (succ n) ) by A4, A5, FUNCT_1:47;
A13: Segm (n + 1) = succ (Segm n) by NAT_1:38;
( F . n = H1(n) & F . (succ n) = H1( succ n) ) by A3, A4, A11;
then (F | omega) . (succ n) c< (F | omega) . n by A2, A3, A10, A12;
then (F | omega) . (succ n) c= (F | omega) . n ;
hence S9[n + 1] by A10, A13; :: thesis: verum
end;
A14: for n being Nat holds S9[n] from NAT_1:sch 2(A8, A9);
 for a being Ordinal st a in dom (F | omega) & succ a in dom (F | omega) holds
(F | omega) . (succ a) c< (F | omega) . a
proof
let a be Ordinal; :: thesis: ( a in dom (F | omega) & succ a in dom (F | omega) implies (F | omega) . (succ a) c< (F | omega) . a )
assume A15: ( a in dom (F | omega) & succ a in dom (F | omega) ) ; :: thesis: (F | omega) . (succ a) c< (F | omega) . a
then reconsider n = a as Nat by A5;
A16: ( S9[n] & (F | omega) . a = F . a & (F | omega) . (succ a) = F . (succ a) ) by A15, A14, FUNCT_1:47;
( F . a = H1(a) & F . (succ a) = H1( succ a) ) by A3, A15, A4, A5;
hence (F | omega) . (succ a) c< (F | omega) . a by A2, A3, A16, A15, A4, A5; :: thesis: verum
end;
then F | omega is descending by A6, Th26, A4, RELAT_1:62;
then F | omega is finite by A1, A7, Th27;
hence F1() is finite by A5; :: thesis: verum
end;
end;