let X be set ; :: thesis: for f being PartFunc of X,X
for g being Function of X,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,X; :: thesis: for g being Function of X,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,X; :: thesis: ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x )
( X = {} implies X = {} ) ;
hence ( f tolerates g iff for x being object st x in dom f holds
f . x = g . x ) by Th74; :: thesis: verum