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
let x be set ; :: according to PARTFUN1:def 6 :: thesis: ( x in (dom g) /\ (dom h) implies g . x = h . x )
assume x in (dom g) /\ (dom h) ; :: thesis: g . x = h . x
then ( x in dom g & x in dom h & dom g c= dom f ) by A2, RELAT_1:25, XBOOLE_0:def 4;
then ( x in (dom f) /\ (dom h) & f . x = g . x ) by A2, GRFUNC_1:8, XBOOLE_0:def 4;
hence g . x = h . x by A1, Def6; :: thesis: verum