theorem Th37: :: CARD_2:38

for m, n being Nat holds card (n + m) = (card n) +` (card m) by Th35;