let f, g be Function; :: thesis: ( f .: ((dom f) /\ (dom g)) c= rng g implies (rng f) \ (rng g) c= rng (f +* g) )
assume A1: f .: ((dom f) /\ (dom g)) c= rng g ; :: thesis: (rng f) \ (rng g) c= rng (f +* g)
let y1 be set ; :: according to TARSKI:def 3 :: thesis: ( not y1 in (rng f) \ (rng g) or y1 in rng (f +* g) )
assume A2: y1 in (rng f) \ (rng g) ; :: thesis: y1 in rng (f +* g)
then consider x1 being set such that
A3: ( x1 in dom f & y1 = f . x1 ) by FUNCT_1:def 5;
A4: x1 in (dom f) \/ (dom g) by A3, XBOOLE_0:def 3;
then A5: x1 in dom (f +* g) by FUNCT_4:def 1;

now

assume x1 in dom g ; :: thesis: contradiction
then x1 in (dom f) /\ (dom g) by A3, XBOOLE_0:def 4;
then f . x1 in f .: ((dom f) /\ (dom g)) by A3, FUNCT_1:def 12;
hence contradiction by A1, A2, A3, XBOOLE_0:def 5; :: thesis: verum

end;

then (f +* g) . x1 = f . x1 by A4, FUNCT_4:def 1;
hence y1 in rng (f +* g) by A3, A5, FUNCT_1:def 5; :: thesis: verum