let X be set ; :: thesis: for R being Relation holds dom (R | X) = (dom R) /\ X
let R be Relation; :: thesis: dom (R | X) = (dom R) /\ X
for x being object holds
( x in dom (R | X) iff x in (dom R) /\ X )

proof

let x be object ; :: thesis: ( x in dom (R | X) iff x in (dom R) /\ X )
( x in dom (R | X) iff ( x in dom R & x in X ) ) by Th51;
hence ( x in dom (R | X) iff x in (dom R) /\ X ) by XBOOLE_0:def 4; :: thesis: verum

end;

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