theorem Th24: :: AFINSQ_1:26

for p, q being XFinSequence holds rng (p ^ q) = (rng p) \/ (rng q) by ORDINAL4:2;