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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in A ^^ (B \/ C) ; :: thesis:
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:

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (B \/ C) ^^ A ; :: thesis:
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:

end;