theorem Th67: :: PARTFUN1:67

for X, Y being set
for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds
f tolerates g