theorem Th21: :: CARD_4:21

for X being set st not X is finite holds
card X = omega *` (card X)