theorem Th87: :: CARD_2:88

for f being Function st dom f is finite & ( for x being object st x in dom f holds
f . x is finite ) holds
Union f is finite