theorem Th53: :: CARD_FIN:54

for x being set
for F being Function st x in dom F holds
union (rng F) = (union (rng (F | ((dom F) \ {x})))) \/ (F . x)