let f, g be Function; :: thesis: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g)
thus rng (f +* g) c= (f .: ((dom f) \ (dom g))) \/ (rng g) :: according to XBOOLE_0:def 10 :: thesis: (f .: ((dom f) \ (dom g))) \/ (rng g) c= rng (f +* g)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f +* g) or y in (f .: ((dom f) \ (dom g))) \/ (rng g) )
assume y in rng (f +* g) ; :: thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)
then consider x being object such that
A1: x in dom (f +* g) and
A2: (f +* g) . x = y by FUNCT_1:def 3;

per cases ( x in dom g or not x in dom g ) ;

suppose A3: x in dom g ; :: thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)

then y = g . x by A2, FUNCT_4:13;
then y in rng g by A3, FUNCT_1:def 3;
hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose A4: not x in dom g ; :: thesis: y in (f .: ((dom f) \ (dom g))) \/ (rng g)

x in (dom f) \/ (dom g) by A1, FUNCT_4:def 1;
then x in dom f by A4, XBOOLE_0:def 3;
then A5: x in (dom f) \ (dom g) by A4, XBOOLE_0:def 5;
y = f . x by A2, A4, FUNCT_4:11;
then y in f .: ((dom f) \ (dom g)) by A5, FUNCT_1:def 6;
hence y in (f .: ((dom f) \ (dom g))) \/ (rng g) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (f .: ((dom f) \ (dom g))) \/ (rng g) or y in rng (f +* g) )
assume A6: y in (f .: ((dom f) \ (dom g))) \/ (rng g) ; :: thesis: y in rng (f +* g)

per cases ( y in f .: ((dom f) \ (dom g)) or y in rng g ) by A6, XBOOLE_0:def 3;

suppose y in f .: ((dom f) \ (dom g)) ; :: thesis: y in rng (f +* g)

then consider x being object such that
A7: x in dom f and
A8: x in (dom f) \ (dom g) and
A9: f . x = y by FUNCT_1:def 6;
not x in dom g by A8, XBOOLE_0:def 5;
then A10: (f +* g) . x = f . x by FUNCT_4:11;
x in (dom f) \/ (dom g) by A7, XBOOLE_0:def 3;
then x in dom (f +* g) by FUNCT_4:def 1;
hence y in rng (f +* g) by A9, A10, FUNCT_1:def 3; :: thesis: verum

end;

suppose A11: y in rng g ; :: thesis: y in rng (f +* g)

rng g c= rng (f +* g) by FUNCT_4:18;
hence y in rng (f +* g) by A11; :: thesis: verum

end;

end;