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