let f be Ordinal-Sequence of a,U; :: thesis: ( f is T-Sequence-like & f is Ordinal-yielding )
thus dom f is ordinal by FUNCT_2:def 1; :: according to ORDINAL1:def 7 :: thesis: f is Ordinal-yielding
take On U ; :: according to ORDINAL2:def 4 :: thesis: proj2 f c= On U
thus proj2 f c= On U by RELAT_1:def 19; :: thesis: verum