let f, g be Function; :: thesis: ( f tolerates g iff ex h being Function st
( f c= h & g c= h ) )

now :: thesis: ( ( ex h being Function st
( f c= h & g c= h ) implies ex h being Function st f \/ g = h ) & ( ex h being Function st f \/ g = h implies ex h being Function st
( f c= h & g c= h ) ) )

thus ( ex h being Function st
( f c= h & g c= h ) implies ex h being Function st f \/ g = h ) :: thesis: ( ex h being Function st f \/ g = h implies ex h being Function st
( f c= h & g c= h ) )

proof

given h being Function such that A1: ( f c= h & g c= h ) ; :: thesis: ex h being Function st f \/ g = h
f \/ g is Function by A1, GRFUNC_1:1, XBOOLE_1:8;
hence ex h being Function st f \/ g = h ; :: thesis: verum

end;

given h being Function such that A2: f \/ g = h ; :: thesis: ex h being Function st
( f c= h & g c= h )
( f c= h & g c= h ) by A2, XBOOLE_1:7;
hence ex h being Function st
( f c= h & g c= h ) ; :: thesis: verum

end;

hence ( f tolerates g iff ex h being Function st
( f c= h & g c= h ) ) by Th51; :: thesis: verum