let f, g be Function; :: thesis: ( f tolerates g implies rng (f +* g) = (rng f) \/ (rng g) )
assume A1: f tolerates g ; :: thesis: rng (f +* g) = (rng f) \/ (rng g)
thus rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f +* g)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )
assume A2: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f +* g)
A3: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12;
A4: rng g c= rng (f +* g) by FUNCT_4:18;

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

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

hence x in rng (f +* g) by A4; :: thesis: verum

end;

suppose A5: not x in rng g ; :: thesis: x in rng (f +* g)

then x in rng f by A2, XBOOLE_0:def 3;
then consider a being object such that
A6: a in dom f and
A7: x = f . a by FUNCT_1:def 3;

now :: thesis: not a in dom g

assume A8: a in dom g ; :: thesis: contradiction
x = (f +* g) . a by A1, A6, A7, FUNCT_4:15
.= g . a by A8, FUNCT_4:13 ;
hence contradiction by A5, A8, FUNCT_1:def 3; :: thesis: verum

end;

then a in (dom f) \ (dom g) by A6, XBOOLE_0:def 5;
then x in f .: ((dom f) \ (dom g)) by A7, FUNCT_1:def 6;
hence x in rng (f +* g) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;