let psi be Ordinal-Sequence; :: thesis: for e being set st e in rng psi holds
e is Ordinal
let e be set ; :: thesis: ( e in rng psi implies e is Ordinal )
assume e in rng psi ; :: thesis: e is Ordinal
then ex u being object st
( u in dom psi & e = psi . u ) by FUNCT_1:def 3;
hence e is Ordinal ; :: thesis: verum