set F = f <--> g;
rng (f <--> g) c= REAL n

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f <--> g) or y in REAL n )
assume y in rng (f <--> g) ; :: thesis: y in REAL n
then consider x being object such that
A4: x in dom (f <--> g) and
A5: (f <--> g) . x = y by FUNCT_1:def 3;
dom (f <--> g) = (dom f) /\ (dom g) by VALUED_2:def 46;
then ( x in dom f & x in dom g ) by A4, XBOOLE_0:def 4;
then A6: ( f . x = f /. x & g . x = g /. x ) by PARTFUN1:def 6;
(f /. x) - (g /. x) in REAL n ;
hence y in REAL n by A5, A6, A4, VALUED_2:def 46; :: thesis: verum

end;

hence f <--> g is PartFunc of Z,(REAL n) by RELSET_1:6; :: thesis: verum