let A, B, C be complex-membered set ; :: thesis: (A ** B) ** C = A ** (B ** C)
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in (A ** B) ** C or a in A ** (B ** C) ) & ( not a in A ** (B ** C) or a in (A ** B) ** C ) )

hereby :: thesis: ( not a in A ** (B ** C) or a in (A ** B) ** C )

assume a in (A ** B) ** C ; :: thesis: a in A ** (B ** C)
then consider c, c1 being Element of COMPLEX such that
A1: a = c * c1 and
A2: c in A ** B and
A3: c1 in C ;
consider c2, c3 being Element of COMPLEX such that
A4: c = c2 * c3 and
A5: c2 in A and
A6: c3 in B by A2;
A7: a = c2 * (c3 * c1) by A1, A4;
c3 * c1 in B ** C by A6, A3;
hence a in A ** (B ** C) by A5, A7; :: thesis: verum

end;

assume a in A ** (B ** C) ; :: thesis: a in (A ** B) ** C
then consider c, c1 being Element of COMPLEX such that
A8: a = c * c1 and
A9: c in A and
A10: c1 in B ** C ;
consider c2, c3 being Element of COMPLEX such that
A11: c1 = c2 * c3 and
A12: c2 in B and
A13: c3 in C by A10;
A14: a = (c * c2) * c3 by A8, A11;
c * c2 in A ** B by A9, A12;
hence a in (A ** B) ** C by A13, A14; :: thesis: verum