let P, R be Relation; :: thesis: rng (P \/ R) = (rng P) \/ (rng R)
thus rng (P \/ R) c= (rng P) \/ (rng R) :: according to XBOOLE_0:def 10 :: thesis: (rng P) \/ (rng R) c= rng (P \/ R)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (P \/ R) or y in (rng P) \/ (rng R) )
assume y in rng (P \/ R) ; :: thesis: y in (rng P) \/ (rng R)
then consider x being set such that
A1: [x,y] in P \/ R by Def5;
( [x,y] in P or [x,y] in R ) by A1, XBOOLE_0:def 3;
then ( y in rng P or y in rng R ) by Def5;
hence y in (rng P) \/ (rng R) by XBOOLE_0:def 3; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng P) \/ (rng R) or y in rng (P \/ R) )
assume A2: y in (rng P) \/ (rng R) ; :: thesis: y in rng (P \/ R)

per cases ( y in rng R or y in rng P ) by A2, XBOOLE_0:def 3;

suppose y in rng R ; :: thesis: y in rng (P \/ R)

then consider x being set such that
A3: [x,y] in R by Def5;
[x,y] in P \/ R by A3, XBOOLE_0:def 3;
hence y in rng (P \/ R) by Def5; :: thesis: verum

end;

suppose y in rng P ; :: thesis: y in rng (P \/ R)

then consider x being set such that
A4: [x,y] in P by Def5;
[x,y] in P \/ R by A4, XBOOLE_0:def 3;
hence y in rng (P \/ R) by Def5; :: thesis: verum

end;

end;