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 set st y in rng (f + g) holds
y in (rng f) ++ (rng g)

proof

let y be set ; :: 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
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, MEMBER_1:46; :: thesis: verum

end;

hence rng (f + g) c= (rng f) ++ (rng g) by TARSKI:def 3; :: thesis: verum