theorem :: PARTFUN1:55

for f, g being Function st dom f = dom g & f tolerates g holds
f = g ;