for fi being Ordinal-Sequence st dom fi <> {} & dom fi is limit_ordinal & fi is increasing holds
( sup fi is_limes_of fi & lim fi = sup fi )