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, Def5;
hence y in INT by A2, INT_1:def 2; :: thesis: verum