let x be set ; :: according to ORDINAL6:def 9 :: thesis: ( x in rng <%f%> implies x is Ordinal-Sequence )
assume x in rng <%f%> ; :: thesis: x is Ordinal-Sequence
then x in {f} by AFINSQ_1:33;
hence x is Ordinal-Sequence by TARSKI:def 1; :: thesis: verum