thus addcomplex is commutative :: thesis: addcomplex is associative

proof

let c1, c2 be Element of COMPLEX ; :: according to BINOP_1:def 13 :: 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 14 :: 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