set F = f <++> g;

rng (f <++> g) c= REAL n

rng (f <++> g) c= REAL n

proof

hence
f <++> g 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 <++> 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;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