let X be set ; :: thesis: ( not X is finite implies card X = omega *` (card X) )
assume A1: not X is finite ; :: thesis: card X = omega *` (card X)
then omega c= card X by CARD_3:85;
hence card X = omega *` (card X) by A1, Th16; :: thesis: verum