theorem Th16: :: PARTFUN2:16

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 f) /\ X holds
(f | X) /. c = f /. c