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 object ; :: 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 object such that
A3: x1 in dom f and
A4: y1 = f . x1 by FUNCT_1:def 3;
A5: x1 in (dom f) \/ (dom g) by A3, XBOOLE_0:def 3;
then A6: x1 in dom (f +* g) by FUNCT_4:def 1;
now :: thesis: not x1 in dom g
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 6;
hence contradiction by A1, A2, A4, XBOOLE_0:def 5; :: thesis: verum
end;
then (f +* g) . x1 = f . x1 by A5, FUNCT_4:def 1;
hence y1 in rng (f +* g) by A4, A6, FUNCT_1:def 3; :: thesis: verum