thus addcomplex is commutative :: thesis: addcomplex is associative

proof

let c1 be Element of COMPLEX ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of COMPLEX holds addcomplex . c1,b₁ = addcomplex . b₁,c1
let c2 be Element of COMPLEX ; :: 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 be Element of COMPLEX ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of COMPLEX holds addcomplex . c1,(addcomplex . b₁,b₂) = addcomplex . (addcomplex . c1,b₁),b₂
let c2, c3 be Element of COMPLEX ; :: 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