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

proof

assume f tolerates g ; :: thesis: f \/ g = f +* g
then ( f c= f +* g & g c= f +* g ) by Th26, Th29;
then ( f \/ g c= f +* g & f +* g c= f \/ g ) by Th30, XBOOLE_1:8;
hence f \/ g = f +* g by XBOOLE_0:def 10; :: thesis: verum

end;

thus ( f \/ g = f +* g implies f tolerates g ) by PARTFUN1:130; :: thesis: verum