let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng (r + f) or y in INT )
assume y in rng (r + f) ; :: thesis: y in INT
then consider x being object such that
A1: x in dom (r + f) and
A2: (r + f) . x = y by FUNCT_1:def 3;
(r + f) . x = r + (f . x) by A1, Def2;
hence y in INT by A2, INT_1:def 2; :: thesis: verum