let X, Y be set ; :: thesis: for f being PartFunc of X,Y st ( Y = {} implies X = {} ) holds
ex g being Function of X,Y st f tolerates g
let f be PartFunc of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies ex g being Function of X,Y st f tolerates g )
assume A1: ( Y = {} implies X = {} ) ; :: thesis: ex g being Function of X,Y st f tolerates g
then consider g being Function of X,Y such that
A2: for x being object st x in dom f holds
g . x = f . x by Th70;
take g ; :: thesis: f tolerates g
thus f tolerates g by A1, A2, Th74; :: thesis: verum