theorem :: ORDINAL1:31

for F being Function st dom F is Ordinal holds
F is Sequence of rng F by Def7, RELAT_1:def 19;