theorem :: PARTFUN1:61

for y being object
for X being set
for f, g being PartFunc of X,{y} holds f tolerates g