:: deftheorem Def12 defines additive HAHNBAN1:def 12 :
for K being 1-sorted
for V being non empty ModuleStr over K
for F being RFunctional of V holds
( F is additive iff for x, y being Vector of V holds F . (x + y) = (F . x) + (F . y) );