deffunc H₁( set ) -> set = F₂((F₁() . $1));
consider F being T-Sequence such that
A0: ( 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 A0, FINSET_1:10; :: thesis: verum

end;

suppose A1: omega c= dom F ; :: thesis: F₁() is finite

set f = F | omega;
A2: dom (F | omega) = omega by A1, RELAT_1:62;
A3: len- (F | omega) = dom (F | omega) by TT0;
B1: 0 in omega by ORDINAL1:def 11;
A4: (F | omega) . 0 = F . 0 by B1, A2, FUNCT_1:47
.= H₁( 0 ) by A0, B1, A1 ;
defpred S₉[ Nat] means (F | omega) . $1 is finite ;
J0: S₉[ 0 ] by C1, A4;
J1: for n being natural number st S₉[n] holds
S₉[n + 1]

proof

let n be natural number ; :: thesis: ( S₉[n] implies S₉[n + 1] )
set a = n;
assume B4: S₉[n] ; :: thesis: S₉[n + 1]
B6: ( n in omega & succ n in omega ) by ORDINAL1:def 12;
then B3: ( n in dom F & succ n in dom F & (F | omega) . n = F . n & (F | omega) . (succ n) = F . (succ n) ) by A1, A2, FUNCT_1:47;
( F . n = H₁(n) & F . (succ n) = H₁( succ n) ) by A0, A1, B6;
then (F | omega) . (succ n) c< (F | omega) . n by C2, A0, B4, B3;
then (F | omega) . (succ n) c= (F | omega) . n by XBOOLE_0:def 8;
hence S₉[n + 1] by B4, NAT_1:38; :: thesis: verum

end;

JJ: for n being natural number holds S₉[n] from NAT_1:sch 2(J0, J1);
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 Z0: ( 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 A2;
B4: ( S₉[n] & (F | omega) . a = F . a & (F | omega) . (succ a) = F . (succ a) ) by Z0, JJ, FUNCT_1:47;
( F . a = H₁(a) & F . (succ a) = H₁( succ a) ) by A0, Z0, A1, A2;
hence (F | omega) . (succ a) c< (F | omega) . a by C2, A0, B4, Z0, A1, A2; :: thesis: verum

end;

then F | omega is descending by A3, DSC2, A1, RELAT_1:62;
then F | omega is finite by C1, A4, TD1;
hence F₁() is finite by A2; :: thesis: verum

end;

end;