for S1, S2 being Sequence st S1 ^ S2 is Ordinal-yielding holds
( S1 is Ordinal-yielding & S2 is Ordinal-yielding )