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;

hence y1 in rng (f +* g) by A4, A6, FUNCT_1:def 3; :: thesis: verum

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

then
(f +* g) . x1 = f . x1
by A5, FUNCT_4:def 1;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 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

hence y1 in rng (f +* g) by A4, A6, FUNCT_1:def 3; :: thesis: verum