thus
multcomplex is commutative
multcomplex is associative
let c1, c2, c3 be Element of COMPLEX ; BINOP_1:def 3 multcomplex . (c1,(multcomplex . (c2,c3))) = multcomplex . ((multcomplex . (c1,c2)),c3)
thus multcomplex . (c1,(multcomplex . (c2,c3))) =
c1 * (multcomplex . (c2,c3))
by Def5
.=
c1 * (c2 * c3)
by Def5
.=
(c1 * c2) * c3
.=
(multcomplex . (c1,c2)) * c3
by Def5
.=
multcomplex . ((multcomplex . (c1,c2)),c3)
by Def5
; verum