let s be Ordinal-Sequence of W; :: thesis: ( s is T-Sequence-like & s is Ordinal-yielding )
thus dom s is ordinal by FUNCT_2:def 1; :: according to ORDINAL1:def 7 :: thesis: s is Ordinal-yielding
take On W ; :: according to ORDINAL2:def 8 :: thesis: rng s c= On W
thus rng s c= On W by RELAT_1:def 19; :: thesis: verum