let X, Y be set ; :: thesis: for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds
f tolerates g
let f, g, h be PartFunc of X,Y; :: thesis: ( f tolerates h & g tolerates h & h is total implies f tolerates g )
assume that
A1: f tolerates h and
A2: g tolerates h and
A3: dom h = X ; :: according to PARTFUN1:def 4 :: 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 & dom f c= X & dom g c= X ) by XBOOLE_0:def 4;
then ( x in (dom f) /\ (dom h) & x in (dom g) /\ (dom h) ) by A3, XBOOLE_0:def 4;
then ( f . x = h . x & g . x = h . x ) by A1, A2, Def6;
hence f . x = g . x ; :: thesis: verum