let f be T-Sequence; :: thesis: ( f is descending & f . 0 is finite & ( for a being ordinal number st f . a <> {} holds
succ a in dom f ) implies last f = {} )
assume that
Z0: ( f is descending & f . 0 is finite ) and
Z1: for a being ordinal number st f . a <> {} holds
succ a in dom f ; :: thesis: last f = {}
f is finite by Z0, TD1;
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;
A4: d = succ n by A3, NAT_1:38;
then A5: union d = n by ORDINAL2:2;
( f . (union d) <> 0 implies d in d ) by Z1, A4, A5;
hence last f = {} ; :: thesis: verum

end;

end;