let X be set ; :: thesis: 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)
let O, O1, O2 be Operation of X; :: thesis: ( dom O1 = X & dom O2 = X implies (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) )
assume A1: ( dom O1 = X & dom O2 = X ) ; :: thesis: (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
let z, s be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [z,s] in (O1 OR O2) \& O or [z,s] in (O1 \& O) AND (O2 \& O) ) & ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O ) )
thus ( [z,s] in (O1 OR O2) \& O implies [z,s] in (O1 \& O) AND (O2 \& O) ) :: thesis: ( not [z,s] in (O1 \& O) AND (O2 \& O) or [z,s] in (O1 OR O2) \& O )

proof

assume A2: [z,s] in (O1 OR O2) \& O ; :: thesis: [z,s] in (O1 \& O) AND (O2 \& O)
then reconsider z = z, s = s as Element of X by ZFMISC_1:87;
s in z . ((O1 OR O2) \& O) by A2, RELAT_1:169;
then s in (z . (O1 OR O2)) \& O by Th35;
then ( s in ((z . O1) OR (z . O2)) \& O & z . O1 <> {} & z . O2 <> {} ) by A1, RELAT_1:170, RELSET_2:10;
then s in ((z . O1) \& O) AND ((z . O2) \& O) by Th24;
then s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th35;
then s in (z . (O1 \& O)) AND (z . (O2 \& O)) by Th35;
then s in z . ((O1 \& O) AND (O2 \& O)) by RELSET_2:11;
hence [z,s] in (O1 \& O) AND (O2 \& O) by RELAT_1:169; :: thesis: verum

end;

assume A3: [z,s] in (O1 \& O) AND (O2 \& O) ; :: thesis: [z,s] in (O1 OR O2) \& O
then reconsider z = z, s = s as Element of X by ZFMISC_1:87;
s in z . ((O1 \& O) AND (O2 \& O)) by A3, RELAT_1:169;
then s in (z . (O1 \& O)) AND (z . (O2 \& O)) by RELSET_2:11;
then s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th35;
then ( s in ((z . O1) \& O) AND ((z . O2) \& O) & z . O1 <> {} & z . O2 <> {} ) by Th35, A1, RELAT_1:170;
then s in ((z . O1) OR (z . O2)) \& O by Th24;
then s in (z . (O1 OR O2)) \& O by RELSET_2:10;
then s in z . ((O1 OR O2) \& O) by Th35;
hence [z,s] in (O1 OR O2) \& O by RELAT_1:169; :: thesis: verum