:: deftheorem Def4 defines - HAHNBAN1:def 4 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, b₄ being Functional of V holds
( b₄ = - f iff for x being Element of V holds b₄ . x = - (f . x) );