let G be Group; :: thesis: for A, B, C being Subset of G holds (A |^ B) |^ C = A |^ (B * C)
let A, B, C be Subset of G; :: thesis: (A |^ B) |^ C = A |^ (B * C)
thus (A |^ B) |^ C c= A |^ (B * C) :: according to XBOOLE_0:def 10 :: thesis: A |^ (B * C) c= (A |^ B) |^ C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ B) |^ C or x in A |^ (B * C) )
assume x in (A |^ B) |^ C ; :: thesis: x in A |^ (B * C)
then consider a, c being Element of G such that
A1: ( x = a |^ c & a in A |^ B & c in C ) ;
consider g, h being Element of G such that
A2: ( a = g |^ h & g in A & h in B ) by A1;
( x = g |^ (h * c) & h * c in B * C ) by A1, A2, Th29;
hence x in A |^ (B * C) by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A |^ (B * C) or x in (A |^ B) |^ C )
assume x in A |^ (B * C) ; :: thesis: x in (A |^ B) |^ C
then consider a, b being Element of G such that
A3: ( x = a |^ b & a in A & b in B * C ) ;
consider g, h being Element of G such that
A4: ( b = g * h & g in B & h in C ) by A3;
a |^ g in A |^ B by A3, A4;
then ( x = (a |^ g) |^ h & (a |^ g) |^ h in (A |^ B) |^ C ) by A3, A4, Th29;
hence x in (A |^ B) |^ C ; :: thesis: verum