let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f [#] r) or y in REAL n )
assume y in rng (f [#] r) ; :: thesis: y in REAL n
then consider x being object such that
A1: x in dom (f [#] r) and
A2: (f [#] r) . x = y by FUNCT_1:def 3;
dom (f [#] r) = dom f by VALUED_2:def 39;
then A3: f . x = f /. x by A1, PARTFUN1:def 6;
r * (f /. x) in REAL n ;
hence y in REAL n by A2, A3, A1, VALUED_2:def 39; :: thesis: verum