let X, Y be set ; :: thesis: for f, g being PartFunc of , st ( Y = {} implies X = {} ) & f tolerates g holds
ex h being Function of X,Y st
( f tolerates h & g tolerates h )
let f, g be PartFunc of ,; :: thesis: ( ( Y = {} implies X = {} ) & f tolerates g implies ex h being Function of X,Y st
( f tolerates h & g tolerates h ) )
assume ( ( Y = {} implies X = {} ) & f tolerates g ) ; :: thesis: ex h being Function of X,Y st
( f tolerates h & g tolerates h )
then ex h being PartFunc of , st
( h is total & f tolerates h & g tolerates h ) by PARTFUN1:162;
hence ex h being Function of X,Y st
( f tolerates h & g tolerates h ) ; :: thesis: verum