let f, g be Function; :: thesis: ( f tolerates g iff f c= f +* g )
thus ( f tolerates g implies f c= f +* g ) :: thesis: ( f c= f +* g implies f tolerates g )

proof

(dom f) \/ (dom g) = dom (f +* g) by Def1;
then A1: dom f c= dom (f +* g) by XBOOLE_1:7;
assume f tolerates g ; :: thesis: f c= f +* g
then for x being object st x in dom f holds
(f +* g) . x = f . x by Th15;
hence f c= f +* g by A1, GRFUNC_1:2; :: thesis: verum

end;

thus ( f c= f +* g implies f tolerates g ) by Th27, PARTFUN1:54; :: thesis: verum