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