theorem Th13: :: DIOPHAN2:7

for f being Function
for o1, o2 being object holds
( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )