thus
addcomplex is commutative
addcomplex is associative
let c1, c2, c3 be Element of COMPLEX ; BINOP_1:def 3 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
; verum