let X be set ; :: thesis: for R being Relation st X c= dom R holds
dom (R | X) = X
let R be Relation; :: thesis: ( X c= dom R implies dom (R | X) = X )
dom (R | X) = (dom R) /\ X by Th55;
hence ( X c= dom R implies dom (R | X) = X ) by XBOOLE_1:28; :: thesis: verum