theorem Th17: :: NEWTON02:115

for f being FinSequence of REAL
for n being positive Nat st n + 1 = len f holds
Sum f = ((Sum ((f | n) /^ 1)) + (f . 1)) + (f . (n + 1))