let P, R be Relation; :: thesis: rng (P \/ R) = (rng P) \/ (rng R)

now

let y be set ; :: thesis: ( y in rng (P \/ R) iff y in (rng P) \/ (rng R) )

A1: now

A2: now

assume 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;

A4: now

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

end;

assume y in (rng P) \/ (rng R) ; :: thesis: y in rng (P \/ R)
hence y in rng (P \/ R) by A4, A2, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume y in rng (P \/ R) ; :: thesis: y in (rng P) \/ (rng R)
then consider x being set such that
A6: [x,y] in P \/ R by Def5;
( [x,y] in P or [x,y] in R ) by A6, 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;

hence ( y in rng (P \/ R) iff y in (rng P) \/ (rng R) ) by A1; :: thesis: verum

end;

hence rng (P \/ R) = (rng P) \/ (rng R) by TARSKI:2; :: thesis: verum