theorem SUM: :: NEWTON04:37

for i being Nat
for f being complex-valued FinSequence holds Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))