thus multcomplex is commutative :: thesis: multcomplex is associative

proof

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