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