theorem :: NEWTON:26

for n, m being Nat
for F being FinSequence of REAL st m <> 0 & len F = m & ( for i, l being Nat st i in dom F & l = (n + i) - 1 holds
F . i = l choose n ) holds
Sum F = (n + m) choose (n + 1)