let X, Y be set ; :: thesis: ( X <> {} & X is finite & not Y is finite implies (card Y) *` (card X) = card Y )
assume that
A1: ( X <> {} & X is finite ) and
A2: not Y is finite ; :: thesis: (card Y) *` (card X) = card Y
( card X in card Y & 0 in card X ) by A1, A2, CARD_3:86, ORDINAL3:8;
hence (card Y) *` (card X) = card Y by A2, Th16; :: thesis: verum