theorem :: PARTFUN2:21

for X being set
for C, D being non empty set
for c being Element of C
for f being PartFunc of C,D st c in dom (X |` f) holds
(X |` f) /. c = f /. c by Th19;