thus addcomplex is commutative :: thesis: addcomplex is associative

proof

let c1, c2 be Element of COMPLEX ; :: according to BINOP_1:def 2 :: thesis: addcomplex . (c1,c2) = addcomplex . (c2,c1)
thus addcomplex . (c1,c2) = c1 + c2 by Def3
.= addcomplex . (c2,c1) by Def3 ; :: thesis: verum

end;

let c1, c2, c3 be Element of COMPLEX ; :: according to BINOP_1:def 3 :: thesis: addcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((addcomplex . (c1,c2)),c3)
thus addcomplex . (c1,(addcomplex . (c2,c3))) = c1 + (addcomplex . (c2,c3)) by Def3
.= c1 + (c2 + c3) by Def3
.= (c1 + c2) + c3
.= (addcomplex . (c1,c2)) + c3 by Def3
.= addcomplex . ((addcomplex . (c1,c2)),c3) by Def3 ; :: thesis: verum