let E be set ; :: thesis: for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
let A, B, C be Subset of (E ^omega); :: thesis: ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )
A1: A ^^ (B \/ C) c= (A ^^ B) \/ (A ^^ C)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^^ (B \/ C) or x in (A ^^ B) \/ (A ^^ C) )
assume x in A ^^ (B \/ C) ; :: thesis: x in (A ^^ B) \/ (A ^^ C)
then consider a, bc being Element of E ^omega such that
A2: a in A and
A3: bc in B \/ C and
A4: x = a ^ bc by Def1;
( bc in B or bc in C ) by A3, XBOOLE_0:def 3;
then ( x in A ^^ B or x in A ^^ C ) by A2, A4, Def1;
hence x in (A ^^ B) \/ (A ^^ C) by XBOOLE_0:def 3; :: thesis: verum

end;

A5: (B \/ C) ^^ A c= (B ^^ A) \/ (C ^^ A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (B \/ C) ^^ A or x in (B ^^ A) \/ (C ^^ A) )
assume x in (B \/ C) ^^ A ; :: thesis: x in (B ^^ A) \/ (C ^^ A)
then consider bc, a being Element of E ^omega such that
A6: bc in B \/ C and
A7: ( a in A & x = bc ^ a ) by Def1;
( bc in B or bc in C ) by A6, XBOOLE_0:def 3;
then ( x in B ^^ A or x in C ^^ A ) by A7, Def1;
hence x in (B ^^ A) \/ (C ^^ A) by XBOOLE_0:def 3; :: thesis: verum

end;

C c= B \/ C by XBOOLE_1:7;
then A8: C ^^ A c= (B \/ C) ^^ A by Th17;
B c= B \/ C by XBOOLE_1:7;
then B ^^ A c= (B \/ C) ^^ A by Th17;
then A9: (B ^^ A) \/ (C ^^ A) c= (B \/ C) ^^ A by A8, XBOOLE_1:8;
C c= B \/ C by XBOOLE_1:7;
then A10: A ^^ C c= A ^^ (B \/ C) by Th17;
B c= B \/ C by XBOOLE_1:7;
then A ^^ B c= A ^^ (B \/ C) by Th17;
then (A ^^ B) \/ (A ^^ C) c= A ^^ (B \/ C) by A10, XBOOLE_1:8;
hence ( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A ) by A1, A5, A9, XBOOLE_0:def 10; :: thesis: verum