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:18; :: according to XBOOLE_0:def 10 :: thesis: (rng f) \/ (rng g) c= rng (f +* g)
A2: rng (f +* g) = (f .: ((dom f) \ (dom g))) \/ (rng g) by Th12;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (rng f) \/ (rng g) or x in rng (f +* g) )
assume A3: x in (rng f) \/ (rng g) ; :: thesis: x in rng (f +* g)
A4: rng g c= rng (f +* g) by FUNCT_4:19;

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 A3, XBOOLE_0:def 3;
then consider a being set such that
A6: ( a in dom f & x = f . a ) by FUNCT_1:def 5;

now

assume A7: a in dom g ; :: thesis: contradiction
x = (f +* g) . a by A1, A6, FUNCT_4:16
.= g . a by A7, FUNCT_4:14 ;
hence contradiction by A5, A7, FUNCT_1:def 5; :: 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 A6, FUNCT_1:def 12;
hence x in rng (f +* g) by A2, XBOOLE_0:def 3; :: thesis: verum

end;

end;