let S1, S2 be Sequence; :: thesis: ( S1 ^ S2 is Ordinal-yielding implies ( S1 is Ordinal-yielding & S2 is Ordinal-yielding ) )
given a being Ordinal 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: not rng S1 c/= a
rng S1 c= rng (S1 ^ S2) by Th3;
hence not rng S1 c/= a by A1; :: thesis: verum
end;
take a ; :: according to ORDINAL2:def 4 :: thesis: not rng S2 c/= a
rng S2 c= rng (S1 ^ S2) by Th3;
hence not rng S2 c/= a by A1; :: thesis: verum