:: deftheorem defines 0-preserving HAHNBAN:def 7 :
for V being RealLinearSpace
for IT being Functional of V holds
( IT is 0-preserving iff IT . (0. V) = 0 );