theorem Th66: :: PARTFUN1:66

for X, Y being set
for f, g being PartFunc of X,Y st f is total & g is total & f tolerates g holds
f = g ;