theorem Th19: :: FRECHET:19
for A, B, C, x being set st C c= A & not x in A holds
((id A) +* (B --> x)) " (C \ {x}) = C \ B