theorem Th66: :: AFINSQ_2:67

for x, y being object
for f being Function st f . y <> x holds
(f | ((dom f) \ {y})) " {x} = f " {x}