theorem :: PARTFUN1:60

for X, Y being set
for f being Function holds <:{},X,Y:> tolerates f