theorem Th10: :: ORDINAL7:7

for A, B being Sequence st A ^ B is Ordinal-yielding holds
( A is Ordinal-yielding & B is Ordinal-yielding )