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

proof

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

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom P) \/ (dom R) or x in dom (P \/ R) )
assume A1: x in (dom P) \/ (dom R) ; :: thesis: x in dom (P \/ R)

per cases ( x in dom R or x in dom P ) by A1, XBOOLE_0:def 3;

suppose x in dom R ; :: thesis: x in dom (P \/ R)

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

end;

suppose x in dom P ; :: thesis: x in dom (P \/ R)

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

end;

end;