let A, B be Sequence; :: thesis: rng (A ^ B) = (rng A) \/ (rng B)
( rng A c= rng (A ^ B) & rng B c= rng (A ^ B) ) by Th7A, Th8A;
then A1: (rng A) \/ (rng B) c= rng (A ^ B) by XBOOLE_1:8;
rng (A ^ B) c= (rng A) \/ (rng B) by Th2Lem;
hence rng (A ^ B) = (rng A) \/ (rng B) by A1; :: thesis: verum