thus multcomplex is commutative :: thesis: multcomplex is associative

proof

let c1, c2 be Element of COMPLEX ; :: according to BINOP_1:def 2 :: thesis: multcomplex . (c1,c2) = multcomplex . (c2,c1)
thus multcomplex . (c1,c2) = c1 * c2 by Def5
.= multcomplex . (c2,c1) by Def5 ; :: thesis: verum

end;

let c1, c2, c3 be Element of COMPLEX ; :: according to BINOP_1:def 3 :: thesis: 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 ; :: thesis: verum