theorem :: CARD_2:78

for X, Y being set st not X is finite & Y is finite holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )