theorem :: PARTFUN1:82
for x, y being object
for f, g being Function st f . x = g . x & f . y = g . y holds
f | {x,y} tolerates g | {x,y}