let f, g be Function; :: thesis: ( f tolerates g iff ex h being Function st
( f c= h & g c= h ) )
thus ( f tolerates g implies ex h being Function st
( f c= h & g c= h ) ) :: thesis: ( ex h being Function st
( f c= h & g c= h ) implies f tolerates g )
proof
assume f tolerates g ; :: thesis: ex h being Function st
( f c= h & g c= h )
then reconsider h = f \/ g as Function by Th1;
take h ; :: thesis: ( f c= h & g c= h )
thus ( f c= h & g c= h ) by XBOOLE_1:7; :: thesis: verum
end;
given h being Function such that A1: ( f c= h & g c= h ) ; :: thesis: f tolerates g
f \/ g is Function by A1, GRFUNC_1:1, XBOOLE_1:8;
hence f tolerates g by Th51; :: thesis: verum