theorem :: PARTFUN2:28

for C, D being non empty set
for f, g being PartFunc of C,D holds
( f tolerates g iff for c being Element of C st c in (dom f) /\ (dom g) holds
f /. c = g /. c )