theorem Th18: :: FRECHET:18

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