:: deftheorem defines Union CARD_3:def 4 :
for f being Function holds Union f = union (rng f);