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

now

let x be set ; :: thesis: ( x in dom (P \/ R) iff x in (dom P) \/ (dom R) )

A1: now

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

now

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

A4: now

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

now

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

end;

hence x in dom (P \/ R) by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( x in dom (P \/ R) iff x in (dom P) \/ (dom R) ) by A1; :: thesis: verum

end;

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