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

now

let x be set ; :: thesis: ( ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) & ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C ) )
thus ( x in (A ^^ B) ^^ C implies x in A ^^ (B ^^ C) ) :: thesis: ( x in A ^^ (B ^^ C) implies x in (A ^^ B) ^^ C )

proof

assume x in (A ^^ B) ^^ C ; :: thesis: x in A ^^ (B ^^ C)
then consider ab, c being Element of E ^omega such that
A1: ( ab in A ^^ B & c in C & x = ab ^ c ) by Def1;
consider a, b being Element of E ^omega such that
A2: ( a in A & b in B & ab = a ^ b ) by A1, Def1;
A3: x = a ^ (b ^ c) by A1, A2, AFINSQ_1:30;
b ^ c in B ^^ C by A1, A2, Def1;
hence x in A ^^ (B ^^ C) by A2, A3, Def1; :: thesis: verum

end;

assume x in A ^^ (B ^^ C) ; :: thesis: x in (A ^^ B) ^^ C
then consider a, bc being Element of E ^omega such that
A4: ( a in A & bc in B ^^ C & x = a ^ bc ) by Def1;
consider b, c being Element of E ^omega such that
A5: ( b in B & c in C & bc = b ^ c ) by A4, Def1;
A6: x = (a ^ b) ^ c by A4, A5, AFINSQ_1:30;
a ^ b in A ^^ B by A4, A5, Def1;
hence x in (A ^^ B) ^^ C by A5, A6, Def1; :: thesis: verum

end;

hence (A ^^ B) ^^ C = A ^^ (B ^^ C) by TARSKI:2; :: thesis: verum