deffunc H₁( set ) -> set = F₂((F₁() . $1));
consider F being T-Sequence such that
A3: ( dom F = dom F₁() & ( for a being ordinal number st a in dom F₁() holds
F . a = H₁(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: F₁() is finite

hence F₁() is finite by A3, FINSET_1:10; :: thesis: verum

end;

suppose A4: omega c= dom F ; :: thesis: F₁() 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: 0 in omega by ORDINAL1:def 11;
A8: (F | omega) . 0 = F . 0 by A7, A5, FUNCT_1:47
.= H₁( 0 ) by A3, A7, A4 ;
defpred S₉[ Nat] means (F | omega) . $1 is finite ;
A9: S₉[ 0 ] by A1, A8;
A10: for n being Nat st S₉[n] holds
S₉[n + 1]

proof

let n be Nat; :: thesis: ( S₉[n] implies S₉[n + 1] )
set a = n;
assume A11: S₉[n] ; :: thesis: S₉[n + 1]
A12: ( n in omega & succ n in omega ) by ORDINAL1:def 12;
then A13: ( 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;
( F . n = H₁(n) & F . (succ n) = H₁( succ n) ) by A3, A4, A12;
then (F | omega) . (succ n) c< (F | omega) . n by A2, A3, A11, A13;
then (F | omega) . (succ n) c= (F | omega) . n by XBOOLE_0:def 8;
hence S₉[n + 1] by A11, NAT_1:38; :: thesis: verum

end;

A14: for n being Nat holds S₉[n] from NAT_1:sch 2(A9, A10);
for a being ordinal number 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 number ; :: 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: ( S₉[n] & (F | omega) . a = F . a & (F | omega) . (succ a) = F . (succ a) ) by A15, A14, FUNCT_1:47;
( F . a = H₁(a) & F . (succ a) = H₁( 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, A8, Th27;
hence F₁() is finite by A5; :: thesis: verum

end;

end;