let A, B, C be complex-membered set ; :: thesis: (A ** B) ** C = A ** (B ** C)
let a be Complex; :: 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 Complex such that
A1: a = c * c1 and
A2: c in A ** B and
A3: c1 in C ;
consider c2, c3 being Complex such that
A4: c = c2 * c3 and
A5: c2 in A and
A6: c3 in B by A2;
( a = c2 * (c3 * c1) & c3 * c1 in B ** C ) by A1, A3, A4, A6;
hence a in A ** (B ** C) by A5; :: thesis: verum

end;

assume a in A ** (B ** C) ; :: thesis: a in (A ** B) ** C
then consider c, c1 being Complex such that
A7: ( a = c * c1 & c in A ) and
A8: c1 in B ** C ;
consider c2, c3 being Complex such that
A9: ( c1 = c2 * c3 & c2 in B ) and
A10: c3 in C by A8;
( a = (c * c2) * c3 & c * c2 in A ** B ) by A7, A9;
hence a in (A ** B) ** C by A10; :: thesis: verum