for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R) by XTUPLE_0:27;