let f be T-Sequence; :: thesis: ( f is descending & f . 0 is finite implies f is finite )
assume Z0: f is descending ; :: thesis: ( not f . 0 is finite or f is finite )
assume Z1: f . 0 is finite ; :: thesis: f is finite
deffunc H₁( set ) -> set = card (f . $1);
consider g being T-Sequence such that
A1: ( dom g = dom f & ( for a being ordinal number st a in dom f holds
g . a = H₁(a) ) ) from ORDINAL2:sch 2();
defpred S₉[ set ] means f . $1 is finite ;
A2: S₉[ {} ] by Z1;
A3: for a being ordinal number st S₉[a] holds
S₉[ succ a]

proof

let a be ordinal number ; :: thesis: ( S₉[a] implies S₉[ succ a] )

per cases ( succ a nin dom f or succ a in dom f ) ;

suppose succ a nin dom f ; :: thesis: ( S₉[a] implies S₉[ succ a] )

hence ( S₉[a] implies S₉[ succ a] ) by FUNCT_1:def 2; :: thesis: verum

end;

suppose C2: succ a in dom f ; :: thesis: ( S₉[a] implies S₉[ succ a] )

C3: a in succ a by ORDINAL1:6;
then a in dom f by C2, ORDINAL1:10;
then f . (succ a) c< f . a by Z0, C2, C3, DSC;
then f . (succ a) c= f . a by XBOOLE_0:def 8;
hence ( S₉[a] implies S₉[ succ a] ) ; :: thesis: verum

end;

end;

end;

A4: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₉[b] ) holds
S₉[a]

proof

let a be ordinal number ; :: thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₉[b] ) implies S₉[a] )
assume a <> {} ; :: thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S₉[b] ) or S₉[a] )
then B2: 0 in a by ORDINAL3:8;

per cases ( a in dom f or a nin dom f ) ;

suppose a in dom f ; :: thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S₉[b] ) or S₉[a] )

then ( 0 in dom f & a in dom f ) by ORDINAL3:8;
then f . a c< f . 0 by Z0, B2, DSC;
then f . a c= f . 0 by XBOOLE_0:def 8;
hence ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S₉[b] ) or S₉[a] ) by Z1; :: thesis: verum

end;

suppose a nin dom f ; :: thesis: ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S₉[b] ) or S₉[a] )

hence ( not a is limit_ordinal or ex b being ordinal number st
( b in a & not S₉[b] ) or S₉[a] ) by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

A5: for a being ordinal number holds S₉[a] from ORDINAL2:sch 1(A2, A3, A4);
g is decreasing

proof

let a be ordinal number ; :: according to ORDINAL5:def 1 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 g or g . b₁ in g . a )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 g or g . b in g . a )
assume B3: ( a in b & b in dom g ) ; :: thesis: g . b in g . a
then a in dom f by A1, ORDINAL1:10;
then ( g . a = H₁(a) & f . a is finite & f . b c< f . a & g . b = H₁(b) & f . b is finite ) by Z0, A1, B3, A5, DSC;
hence g . b in g . a by CARD_2:48; :: thesis: verum

end;

hence f is finite by A1, FINSET_1:10; :: thesis: verum