:: deftheorem defines comp VECTSP_1:def 12 :
for F being non empty addLoopStr
for b₂ being UnOp of the carrier of F holds
( b₂ = comp F iff for x being Element of F holds b₂ . x = - x );