:: deftheorem defines non-zero NDIFF_1:def 1 :
for X being set
for S being ZeroStr
for f being Function of X,S holds
( f is non-zero iff rng f c= NonZero S );