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

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
A1: a in A and
A2: bc in B /\ C and
A3: x = a ^ bc by Def1;
bc in C by A2, XBOOLE_0:def 4;
then A4: x in A ^^ C by A1, A3, Def1;
bc in B by A2, XBOOLE_0:def 4;
then x in A ^^ B by A1, A3, Def1;
hence x in (A ^^ B) /\ (A ^^ C) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

thus (B /\ C) ^^ A c= (B ^^ A) /\ (C ^^ A) :: thesis: verum

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
A5: bc in B /\ C and
A6: ( a in A & x = bc ^ a ) by Def1;
bc in C by A5, XBOOLE_0:def 4;
then A7: x in C ^^ A by A6, Def1;
bc in B by A5, XBOOLE_0:def 4;
then x in B ^^ A by A6, Def1;
hence x in (B ^^ A) /\ (C ^^ A) by A7, XBOOLE_0:def 4; :: thesis: verum

end;