let X, Y be set ; :: thesis: for f, g being PartFunc of X,Y
for h being Function st f tolerates h & g c= f holds
g tolerates h
let f, g be PartFunc of X,Y; :: thesis: for h being Function st f tolerates h & g c= f holds
g tolerates h
let h be Function; :: thesis: ( f tolerates h & g c= f implies g tolerates h )
assume that
A1: f tolerates h and
A2: g c= f ; :: thesis: g tolerates h
A3: dom g c= dom f by A2, RELAT_1:11;
let x be object ; :: according to PARTFUN1:def 4 :: thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume A4: x in (dom g) /\ (dom h) ; :: thesis: g . x = h . x
then A5: x in dom g by XBOOLE_0:def 4;
then A6: f . x = g . x by A2, GRFUNC_1:2;
x in dom h by A4, XBOOLE_0:def 4;
then x in (dom f) /\ (dom h) by A5, A3, XBOOLE_0:def 4;
hence g . x = h . x by A1, A6; :: thesis: verum