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)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f + g) or y in (rng f) ++ (rng g) )
assume y in rng (f + g) ; :: thesis: y in (rng f) ++ (rng g)
then consider x1 being object such that
A1: x1 in dom (f + g) and
A2: y = (f + g) . x1 by FUNCT_1:def 3;
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then x1 in dom f by A1, XBOOLE_0:def 4;
then A4: f . x1 in rng f by FUNCT_1:def 3;
x1 in dom g by A1, A3, XBOOLE_0:def 4;
then A5: g . x1 in rng g by FUNCT_1:def 3;
(f + g) . x1 = (f . x1) + (g . x1) by A1, VALUED_1:def 1;
hence y in (rng f) ++ (rng g) by A2, A4, A5, MEMBER_1:46; :: thesis: verum