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