let X, Y be set ; :: thesis: ( X <> {} & X is finite & not Y is finite implies (card Y) *` (card X) = card Y )
assume A1: ( X <> {} & X is finite & not Y is finite ) ; :: thesis: (card Y) *` (card X) = card Y
then ( card X in card Y & 0 in card X ) by CARD_3:103, ORDINAL3:10;
hence (card Y) *` (card X) = card Y by A1, Th78; :: thesis: verum