theorem :: NEWTON02:134

for n being Nat holds Sum (Newton_Coeff n) = (Sum ((Newton_Coeff n) | n)) + 1