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