theorem :: PARTFUN1:65

for X, Y being set
for f being Function holds <:f,X,Y:> tolerates f by Th64;