let X be non empty set ; :: thesis: for f, g being PartFunc of X,REAL holds rng (f + g) c= (rng f) + (rng g)
let f, g be PartFunc of X,REAL ; :: thesis: rng (f + g) c= (rng f) + (rng g)
for y being Real st y in rng (f + g) holds
y in (rng f) + (rng g)

proof

let y be Real; :: thesis: ( y in rng (f + g) implies y in (rng f) + (rng g) )
A1: (rng f) + (rng g) = { (x + z) where x, z is Real : ( x in rng f & z in rng g ) } by COMPLSP1:def 21;
assume y in rng (f + g) ; :: thesis: y in (rng f) + (rng g)
then consider x1 being set such that
A2: x1 in dom (f + g) and
A3: y = (f + g) . x1 by FUNCT_1:def 5;
A4: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then x1 in dom f by A2, XBOOLE_0:def 4;
then A5: f . x1 in rng f by FUNCT_1:def 5;
x1 in dom g by A2, A4, XBOOLE_0:def 4;
then A6: g . x1 in rng g by FUNCT_1:def 5;
(f + g) . x1 = (f . x1) + (g . x1) by A2, VALUED_1:def 1;
hence y in (rng f) + (rng g) by A3, A5, A6, A1; :: thesis: verum

end;

hence rng (f + g) c= (rng f) + (rng g) by SUBSET_1:7; :: thesis: verum