let M, N be finite Cardinal; :: thesis: M *` N is finite
A1: card M = M by CARD_1:def 2;
card N = N by CARD_1:def 2;
then M *` N = card ((card M) * (card N)) by A1, Th52;
hence M *` N is finite ; :: thesis: verum