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

proof

let a be Ordinal; :: 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 A6: succ a in dom f ; :: thesis: ( S₉[a] implies S₉[ succ a] )

A7: a in succ a by ORDINAL1:6;
then a in dom f by A6, ORDINAL1:10;
then f . (succ a) c< f . a by A1, A6, A7;
then f . (succ a) c= f . a ;
hence ( S₉[a] implies S₉[ succ a] ) ; :: thesis: verum

end;

end;

end;

A8: for a being Ordinal st a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S₉[b] ) holds
S₉[a]

proof

let a be Ordinal; :: thesis: ( a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S₉[b] ) implies S₉[a] )
assume a <> 0 ; :: thesis: ( not a is limit_ordinal or ex b being Ordinal st
( b in a & not S₉[b] ) or S₉[a] )
then A9: 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 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 A1, A9;
then f . a c= f . 0 ;
hence ( not a is limit_ordinal or ex b being Ordinal st
( b in a & not S₉[b] ) or S₉[a] ) by A2; :: thesis: verum

end;

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

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

end;

end;

end;

A10: for a being Ordinal holds S₉[a] from ORDINAL2:sch 1(A4, A5, A8);
g is decreasing

proof

let a be Ordinal; :: 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; :: thesis: ( not a in b or not b in proj1 g or g . b in g . a )
assume A11: ( a in b & b in dom g ) ; :: thesis: g . b in g . a
then a in dom f by A3, ORDINAL1:10;
then A12: ( g . a = H₁(a) & f . a is finite & f . b c< f . a & g . b = H₁(b) & f . b is finite ) by A1, A3, A11, A10;
reconsider ga = g . a as Nat by A12;
g . b in Segm ga by CARD_2:48, A12;
hence g . b in g . a ; :: thesis: verum

end;

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