let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y 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 X,Y; :: 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 consider h being PartFunc of X,Y such that
A1: h is total and
A2: ( f tolerates h & g tolerates h ) by PARTFUN1:162;
thus ex h being Function of X,Y st
( f tolerates h & g tolerates h ) by A1, A2; :: thesis: verum