theorem Th37: :: CARD_1:38
for X, Y being set st X,Y are_equipotent & X is finite holds
Y is finite