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

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