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 object ; :: 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 and
A2: a in A |^ B and
A3: c in C ;
consider g, h being Element of G such that
A4: a = g |^ h and
A5: g in A and
A6: h in B by A2;
( x = g |^ (h * c) & h * c in B * C ) by A1, A3, A4, A6, Th24;
hence x in A |^ (B * C) by A5; :: thesis: verum

end;

let x be object ; :: 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
A7: ( x = a |^ b & a in A ) and
A8: b in B * C ;
consider g, h being Element of G such that
A9: ( b = g * h & g in B ) and
A10: h in C by A8;
( a |^ g in A |^ B & x = (a |^ g) |^ h ) by A7, A9, Th24;
hence x in (A |^ B) |^ C by A10; :: thesis: verum