:: deftheorem defines 0-preserving ZMODLAT1:def 23 :
for V being non empty ModuleStr over INT.Ring
for F being FrFunctional of V holds
( F is 0-preserving iff F . (0. V) = 0. F_Real );