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 ;
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
.= g . a by ;
hence contradiction by A5, A8, FUNCT_1:def 3; :: thesis: verum
end;
then a in (dom f) \ (dom g) by ;
then x in f .: ((dom f) \ (dom g)) by ;
hence x in rng (f +* g) by ; :: thesis: verum
end;
end;