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