let X be set ; :: thesis: for O1, O2, O being Operation of X st dom O1 = X & dom O2 = X holds
(O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
let O1, O2, O be Operation of X; :: thesis: ( dom O1 = X & dom O2 = X implies (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O) )
assume A0: ( dom O1 = X & dom O2 = X ) ; :: thesis: (O1 OR O2) \& O = (O1 \& O) AND (O2 \& O)
let z be set ; :: according to RELAT_1:def 2 :: thesis: for b₁ being set holds
( ( not [z,b₁] in (O1 OR O2) \& O or [z,b₁] in (O1 \& O) AND (O2 \& O) ) & ( not [z,b₁] in (O1 \& O) AND (O2 \& O) or [z,b₁] in (O1 OR O2) \& O ) )
let s be set ; :: 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 Z0: [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 Z0, RELAT_1:169;
then s in (z . (O1 OR O2)) \& O by Th25;
then ( s in ((z . O1) OR (z . O2)) \& O & z . O1 <> {} & z . O2 <> {} ) by A0, RELAT_1:170, RELSET_2:10;
then s in ((z . O1) \& O) AND ((z . O2) \& O) by Th17;
then s in (z . (O1 \& O)) AND ((z . O2) \& O) by Th25;
then s in (z . (O1 \& O)) AND (z . (O2 \& O)) by Th25;
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 Z1: [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 Z1, 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 Th25;
then ( s in ((z . O1) \& O) AND ((z . O2) \& O) & z . O1 <> {} & z . O2 <> {} ) by Th25, A0, RELAT_1:170;
then s in ((z . O1) OR (z . O2)) \& O by Th17;
then s in (z . (O1 OR O2)) \& O by RELSET_2:10;
then s in z . ((O1 OR O2) \& O) by Th25;
hence [z,s] in (O1 OR O2) \& O by RELAT_1:169; :: thesis: verum