let X, Y be set ; :: thesis: for f being PartFunc of X,Y
for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being object st x in dom f holds
f . x = g . x )
let f be PartFunc of X,Y; :: thesis: for g being Function of X,Y st ( Y = {} implies X = {} ) holds
( f tolerates g iff for x being object st x in dom f holds
f . x = g . x )
let g be Function of X,Y; :: thesis: ( ( Y = {} implies X = {} ) implies ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x ) )
assume ( Y = {} implies X = {} ) ; :: thesis: ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x )
then dom g = X by Def1;
hence ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x ) by PARTFUN1:53; :: thesis: verum