:: deftheorem Def5 defines multcomplex BINOP_2:def 5 :
for b₁ being BinOp of COMPLEX holds
( b₁ = multcomplex iff for c1, c2 being Complex holds b₁ . (c1,c2) = c1 * c2 );