:: deftheorem defines 0-preserving HAHNBAN1:def 9 :
for K being non empty ZeroStr
for V being non empty ModuleStr over K
for F being Functional of V holds
( F is 0-preserving iff F . (0. V) = 0. K );