theorem Th17: :: FRECHET:17

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