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 )

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

(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 A3:
[z,s] in (O1 \& O) AND (O2 \& O)
; :: thesis: [z,s] in (O1 OR O2) \& O
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;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

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