for fi being Ordinal-Sequence
for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )