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 H1( 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 = H1(a) ) ) from ORDINAL2:sch 2();
 defpred S9[ set ] means f . $1 is finite ;
A4: S9[ 0 ] by A2;
A5: for a being Ordinal st S9[a] holds
S9[ succ a]
proof
let a be Ordinal; :: thesis: ( S9[a] implies S9[ succ a] )
per cases ( succ a nin dom f or succ a in dom f ) ;
suppose succ a nin dom f ; :: thesis: ( S9[a] implies S9[ succ a] )
hence ( S9[a] implies S9[ succ a] ) by FUNCT_1:def 2; :: thesis: verum
end;
suppose A6: succ a in dom f ; :: thesis: ( S9[a] implies S9[ 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 ( S9[a] implies S9[ 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
S9[b] ) holds
S9[a]
proof
let a be Ordinal; :: thesis: ( a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S9[b] ) implies S9[a] )
assume a <> 0 ; :: thesis: ( not a is limit_ordinal or ex b being Ordinal st
( b in a & not S9[b] ) or S9[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 S9[b] ) or S9[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 S9[b] ) or S9[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 S9[b] ) or S9[a] )
hence ( not a is limit_ordinal or ex b being Ordinal st
( b in a & not S9[b] ) or S9[a] ) by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
A10: for a being Ordinal holds S9[a] from ORDINAL2:sch 1(A4, A5, A8);
 g is decreasing
proof
let a be Ordinal; :: according to ORDINAL5:def 1 :: thesis: for b1 being set holds
( not a in b1 or not b1 in proj1 g or g . b1 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 = H1(a) & f . a is finite & f . b c< f . a & g . b = H1(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