let y be object ; :: thesis: for X being set
for f, g being PartFunc of X,{y} holds f tolerates g
let X 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 object ; :: according to PARTFUN1:def 4 :: thesis: ( x in (dom f) /\ (dom g) implies f . x = g . x )
assume A1: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then x in dom f by XBOOLE_0:def 4;
then A2: f . x = y by Th20;
x in dom g by A1, XBOOLE_0:def 4;
hence f . x = g . x by A2, Th20; :: thesis: verum