theorem :: PARTFUN1:63

for Y being set
for f being Function holds Y |` f tolerates f