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

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