theorem :: PARTFUN1:59

for f being Function holds {} tolerates f ;