for k, n being Nat holds (n + 1) block (k + 1) = ((k + 1) * (n block (k + 1))) + (n block k)