theorem Th4: :: CQC_SIM1:4

for x, y being set
for g being Function
for A being set st not y in g .: (A \ {x}) holds
(g +* (x .--> y)) .: (A \ {x}) = ((g +* (x .--> y)) .: A) \ {y}