:: deftheorem defines 0-preserving HAHNBAN1:def 15 :
for K being 1-sorted
for V being ModuleStr over K
for F being RFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0 );