let G be non empty multMagma ; :: thesis: for A, B, C being Subset of G st G is associative holds

(A * B) * C = A * (B * C)

let A, B, C be Subset of G; :: thesis: ( G is associative implies (A * B) * C = A * (B * C) )

assume A1: G is associative ; :: 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

assume x in A * (B * C) ; :: thesis: x in (A * B) * C

then consider g, h being Element of G such that

A8: x = g * h and

A9: g in A and

A10: h in B * C ;

consider g1, g2 being Element of G such that

A11: h = g1 * g2 and

A12: g1 in B and

A13: g2 in C by A10;

A14: g * g1 in A * B by A9, A12;

x = (g * g1) * g2 by A1, A8, A11;

hence x in (A * B) * C by A13, A14; :: thesis: verum

(A * B) * C = A * (B * C)

let A, B, C be Subset of G; :: thesis: ( G is associative implies (A * B) * C = A * (B * C) )

assume A1: G is associative ; :: 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 )
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 g, h being Element of G such that

A2: x = g * h and

A3: g in A * B and

A4: h in C ;

consider g1, g2 being Element of G such that

A5: g = g1 * g2 and

A6: g1 in A and

A7: g2 in B by A3;

( x = g1 * (g2 * h) & g2 * h in B * C ) by A1, A2, A4, A5, A7;

hence x in A * (B * C) by A6; :: thesis: verum

end;assume x in (A * B) * C ; :: thesis: x in A * (B * C)

then consider g, h being Element of G such that

A2: x = g * h and

A3: g in A * B and

A4: h in C ;

consider g1, g2 being Element of G such that

A5: g = g1 * g2 and

A6: g1 in A and

A7: g2 in B by A3;

( x = g1 * (g2 * h) & g2 * h in B * C ) by A1, A2, A4, A5, A7;

hence x in A * (B * C) by A6; :: thesis: verum

assume x in A * (B * C) ; :: thesis: x in (A * B) * C

then consider g, h being Element of G such that

A8: x = g * h and

A9: g in A and

A10: h in B * C ;

consider g1, g2 being Element of G such that

A11: h = g1 * g2 and

A12: g1 in B and

A13: g2 in C by A10;

A14: g * g1 in A * B by A9, A12;

x = (g * g1) * g2 by A1, A8, A11;

hence x in (A * B) * C by A13, A14; :: thesis: verum