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
A1: x in dom (f <++> g) and
A2: (f <++> g) . x = y by FUNCT_1:def 3;
dom (f <++> g) = (dom f) /\ (dom g) by VALUED_2:def 45;
then ( x in dom f & x in dom g ) by A1, XBOOLE_0:def 4;
then A3: ( 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 A2, A3, A1, VALUED_2:def 45; :: thesis: verum

end;

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