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