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