let G be addGroup; :: 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