theorem :: RELAT_1:154
for R, S being Relation holds R | (dom S) = R | (dom (S | (dom R)))