:: deftheorem defines - HAHNBAN1:def 5 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, g being Functional of V holds f - g = f + (- g);