let A, B be Sequence; :: thesis: ( A ^ B is Ordinal-yielding implies ( A is Ordinal-yielding & B is Ordinal-yielding ) )
assume A ^ B is Ordinal-yielding ; :: thesis: ( A is Ordinal-yielding & B is Ordinal-yielding )
then consider c being Ordinal such that
A1: rng (A ^ B) c= c by ORDINAL2:def 4;
rng A c= rng (A ^ B) by ORDINAL4:39;
hence A is Ordinal-yielding by A1, XBOOLE_1:1, ORDINAL2:def 4; :: thesis: B is Ordinal-yielding
rng B c= rng (A ^ B) by ORDINAL4:40;
hence B is Ordinal-yielding by A1, XBOOLE_1:1, ORDINAL2:def 4; :: thesis: verum