let X be set ; :: thesis: ( not X is finite implies card X = omega *` (card X) )
assume Z: not X is finite ; :: thesis: card X = omega *` (card X)
then ( 0 in omega & omega c= card X ) by CARD_3:102;
hence card X = omega *` (card X) by Th78, Z; :: thesis: verum