:: deftheorem Def2 defines additive HAHNBAN:def 2 :
for V being RealLinearSpace
for IT being Functional of V holds
( IT is additive iff for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y) );