theorem :: PARTFUN1:80

for x being object
for X, Y being set
for f being b₃ -valued Function st x in dom (f | X) holds
(f | X) /. x = f /. x