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 A1: f c= f +* g by Th29;
A2: f +* g c= f \/ g by Th30;
g c= f +* g by Th26;
then f \/ g c= f +* g by A1, XBOOLE_1:8;
hence f \/ g = f +* g by A2, XBOOLE_0:def 10; :: thesis: verum

end;

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