let R, S be Relation; :: thesis: R | (dom S) = R | (dom (S | (dom R)))
thus R | (dom S) = (R | (dom R)) | (dom S) by Th97
.= R | ((dom S) /\ (dom R)) by Th100
.= R | (dom (S | (dom R))) by Th90 ; :: thesis: verum