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:51;
hence M +` N is finite ; :: thesis: verum