let X be set ; :: thesis: for R being Relation holds R | X = R | ((dom R) /\ X)
let R be Relation; :: thesis: R | X = R | ((dom R) /\ X)
thus R | X = (R | (dom R)) | X by Th97
.= R | ((dom R) /\ X) by Th100 ; :: thesis: verum