let S1, S2 be T-Sequence; :: thesis: ( S1 ^ S2 is Ordinal-yielding implies ( S1 is Ordinal-yielding & S2 is Ordinal-yielding ) )
given a being ordinal number such that A1: rng (S1 ^ S2) c= a ; :: according to ORDINAL2:def 4 :: thesis: ( S1 is Ordinal-yielding & S2 is Ordinal-yielding )
thus S1 is Ordinal-yielding :: thesis: S2 is Ordinal-yielding

proof

take a ; :: according to ORDINAL2:def 4 :: thesis: proj2 S1 c= a
rng S1 c= rng (S1 ^ S2) by Th3;
hence proj2 S1 c= a by A1, XBOOLE_1:1; :: thesis: verum

end;

take a ; :: according to ORDINAL2:def 4 :: thesis: proj2 S2 c= a
rng S2 c= rng (S1 ^ S2) by Th3;
hence proj2 S2 c= a by A1, XBOOLE_1:1; :: thesis: verum