theorem Th2: :: ORDINAL4:2

for A, B being Sequence holds rng (A ^ B) = (rng A) \/ (rng B)