for m, n being Nat holds card (n * m) = (card n) *` (card m)