:: deftheorem defines compcomplex BINOP_2:def 1 :
for b₁ being UnOp of COMPLEX holds
( b₁ = compcomplex iff for c being Complex holds b₁ . c = - c );