theorem Th71: :: PARTFUN1:71

for X, Y being set
for f being PartFunc of X,Y
for g being Function st g in TotFuncs f holds
f tolerates g