let f be Function of a,b; :: thesis: ( f is Ordinal-yielding & f is T-Sequence-like )
rng f c= b by RELAT_1:def 19;
hence ex c being ordinal number st rng f c= c ; :: according to ORDINAL2:def 4 :: thesis: f is T-Sequence-like
( b = {} implies f = {} ) ;
hence dom f is ordinal by FUNCT_2:def 1; :: according to ORDINAL1:def 7 :: thesis: verum