let M, N be finite Cardinal; :: thesis: M *` N is finite
( card M = card (card M) & card N = card (card N) & card M = M & card N = N ) by CARD_1:def 5;
then M *` N = card ((card M) * (card N)) by CARD_2:52;
hence M *` N is finite ; :: thesis: verum