for A, B, C, x being set st C c= A holds
((id A) +* (B --> x)) " (C \ {x}) = (C \ B) \ {x}