theorem :: CARD_4:19

for X, Y being set st not X is finite & Y is finite & Y <> {} holds
( [:X,Y:],X are_equipotent & card [:X,Y:] = card X )