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

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

end;

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