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)

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

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

dom (F + G) = X
by FUNCT_2:def 1;
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;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

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