let f be Sequence; :: thesis: ( f is descending & f . 0 is finite & ( for a being Ordinal st f . a <> {} holds
succ a in dom f ) implies last f = {} )
assume that
A1: ( f is descending & f . 0 is finite ) and
A2: for a being Ordinal st f . a <> {} holds
succ a in dom f ; :: thesis: last f = {}
f is finite by A1, Th27;
then reconsider d = dom f as finite Ordinal ;
set u = union d;

per cases ( d = 0 or d <> 0 ) ;

suppose d = 0 ; :: thesis: last f = {}

hence last f = {} by FUNCT_1:def 2; :: thesis: verum

end;

suppose d <> 0 ; :: thesis: last f = {}

then consider n being Nat such that
A3: d = n + 1 by NAT_1:6;
d = Segm (n + 1) by A3;
then A4: d = succ (Segm n) by NAT_1:38;
then A5: union d = n by ORDINAL2:2;
( f . (union d) <> 0 implies d in d ) by A2, A4, A5;
hence last f = {} ; :: thesis: verum

end;

end;