theorem Th3: :: CQC_SIM1:3

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