let R be Relation; :: thesis: for A being set holds dom (R | ((dom R) \ A)) = (dom R) \ A
let A be set ; :: thesis: dom (R | ((dom R) \ A)) = (dom R) \ A
thus dom (R | ((dom R) \ A)) = (dom R) /\ ((dom R) \ A) by Th90
.= ((dom R) /\ (dom R)) \ A by XBOOLE_1:49
.= (dom R) \ A ; :: thesis: verum