let X, y be set ; :: thesis: for f, g being PartFunc of X,{y} holds f tolerates g
let f, g be PartFunc of X,{y}; :: thesis: f tolerates g
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then ( x in dom f & x in dom g ) by XBOOLE_0:def 4;
then ( f . x = y & g . x = y ) by Th73;
hence f . x = g . x ; :: thesis: verum