M +` N = card ((card M) + (card N)) by Th37;
hence M +` N is finite ; :: thesis: verum