let f be Function; :: thesis: for o1, o2 being object holds
( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )
let o1, o2 be object ; :: thesis: ( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )

hereby :: thesis: ( o1 in dom f & f . o1 = 0 implies o1 in ZeroPointSet f )

assume A1: o1 in ZeroPointSet f ; :: thesis: ( o1 in dom f & f . o1 = 0 )
then not o1 in support f by XBOOLE_0:def 5;
hence ( o1 in dom f & f . o1 = 0 ) by PRE_POLY:def 7, A1; :: thesis: verum

end;

assume that
A1: o1 in dom f and
A2: f . o1 = 0 ; :: thesis: o1 in ZeroPointSet f
not o1 in support f by A2, PRE_POLY:def 7;
hence o1 in ZeroPointSet f by A1, XBOOLE_0:def 5; :: thesis: verum