theorem Th77: :: PARTFUN1:77

for f, g being Function
for x, y, z being object st f tolerates g & [x,y] in f & [x,z] in g holds
y = z