for X being set
for O, O1, O2 being Operation of X st dom O1 = X & dom O2 = X holds
(O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)