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 Th28;
A2: f +* g c= f \/ g by Th29;
g c= f +* g by Th25;
then f \/ g c= f +* g by A1, XBOOLE_1:8;
hence f \/ g = f +* g by A2; :: thesis: verum
end;
thus ( f \/ g = f +* g implies f tolerates g ) by PARTFUN1:51; :: thesis: verum