let X be non empty set ; :: thesis: for Y, Z being non empty Subset of ExtREAL
for F being Function of X,Y
for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let Y, Z be non empty Subset of ExtREAL ; :: thesis: for F being Function of X,Y
for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let F be Function of X,Y; :: thesis: for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G)
let G be Function of X,Z; :: thesis: rng (F + G) c= (rng F) + (rng G)
F + G is Function of X,((rng F) + (rng G))

proof

A1: dom (F + G) = X by FUNCT_2:def 1;
for x being set st x in X holds
(F + G) . x in (rng F) + (rng G)

proof

let x be set ; :: thesis: ( x in X implies (F + G) . x in (rng F) + (rng G) )
assume x in X ; :: thesis: (F + G) . x in (rng F) + (rng G)
then reconsider x = x as Element of X ;
reconsider a = F . x, b = G . x as R_eal ;
A2: (F + G) . x = a + b by Def9;
A3: a in rng F by FUNCT_2:6;
b in rng G by FUNCT_2:6;
hence (F + G) . x in (rng F) + (rng G) by A2, A3, Def5; :: thesis: verum

end;

hence F + G is Function of X,((rng F) + (rng G)) by A1, FUNCT_2:5; :: thesis: verum

end;

hence rng (F + G) c= (rng F) + (rng G) by RELAT_1:def 19; :: thesis: verum