for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)