:: deftheorem defm defines '-' VECTSP13:def 12 :
for X being non empty set
for L being non empty addLoopStr
for f, b₄ being Function of X,L holds
( b₄ = '-' f iff for x being Element of X holds b₄ . x = - (f . x) );