theorem :: NEWTON02:135

for n being Nat holds len ((Newton_Coeff n) | n) = n