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