:: deftheorem Def3 defines + HAHNBAN1:def 3 :
for K being non empty addLoopStr
for V being non empty ModuleStr over K
for f, g, b₅ being Functional of V holds
( b₅ = f + g iff for x being Element of V holds b₅ . x = (f . x) + (g . x) );