let X be set ; :: thesis: for f, g being PartFunc of X,X
for h being Function of X,X st f tolerates h & g tolerates h holds
f tolerates g
let f, g be PartFunc of X,X; :: thesis: for h being Function of X,X st f tolerates h & g tolerates h holds
f tolerates g
let h be Function of X,X; :: thesis: ( f tolerates h & g tolerates h implies f tolerates g )
( X = {} implies X = {} ) ;
hence ( f tolerates h & g tolerates h implies f tolerates g ) by PARTFUN1:158; :: thesis: verum