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 2 :: 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 A4: x in (dom f) /\ (dom g) ; :: thesis: f . x = g . x
then x in dom f by XBOOLE_0:def 4;
then x in (dom f) /\ (dom h) by A3, XBOOLE_0:def 4;
then A5: f . x = h . x by A1;
x in dom g by A4, XBOOLE_0:def 4;
then x in (dom g) /\ (dom h) by A3, XBOOLE_0:def 4;
hence f . x = g . x by A2, A5; :: thesis: verum