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)
A1: for x being object st x in X holds
(F + G) . x in (rng F) + (rng G)

proof

let x be object ; :: 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: a in rng F by FUNCT_2:4;
A3: b in rng G by FUNCT_2:4;
(F + G) . x = a + b by Def3;
hence (F + G) . x in (rng F) + (rng G) by A2, A3; :: thesis: verum

end;

dom (F + G) = X by FUNCT_2:def 1;
then F + G is Function of X,((rng F) + (rng G)) by A1, FUNCT_2:3;
hence rng (F + G) c= (rng F) + (rng G) by RELAT_1:def 19; :: thesis: verum