set F = f [#] r;

rng (f [#] r) c= REAL n

rng (f [#] r) c= REAL n

proof

hence
f [#] r is PartFunc of Z,(REAL n)
by RELSET_1:6; :: thesis: verum
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

end;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