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) )
assume y in rng (f + g) ; :: thesis: y in (rng f) + (rng g)
then consider x1 being set such that
A1: ( x1 in dom (f + g) & y = (f + g) . x1 ) by FUNCT_1:def 5;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then ( x1 in dom f & x1 in dom g ) by A1, XBOOLE_0:def 4;
then A2: ( f . x1 in rng f & g . x1 in rng g ) by FUNCT_1:def 5;
A3: (rng f) + (rng g) = { (x + z) where x, z is Real : ( x in rng f & z in rng g ) } by COMPLSP1:def 21;
(f + g) . x1 = (f . x1) + (g . x1) by A1, VALUED_1:def 1;
hence y in (rng f) + (rng g) by A1, A2, A3; :: thesis: verum

end;

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