for X, Y being set st X <> {} & X is finite & not Y is finite holds
(card Y) *` (card X) = card Y