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