theorem :: PARTFUN1:62

for X being set
for f being Function holds f | X tolerates f