:: deftheorem Def1 defines sqrcomplex RVSUM_2:def 1 :
for b₁ being UnOp of COMPLEX holds
( b₁ = sqrcomplex iff for c being Complex holds b₁ . c = c ^2 );