let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (- f) or y in INT )
assume y in rng (- f) ; :: thesis: y in INT
then consider x being object such that
A1: x in dom (- f) and
A2: (- f) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;
(- f) . x = (- f) /. x
.= - (f /. x) by A1, VFUNCT_1:def 5
.= - (f . x) ;
hence y in INT by A2, INT_1:def 2; :: thesis: verum