for i being Nat
for f being FinSequence of COMPLEX holds Sum f = ((Sum (f | i)) + (f . (i + 1))) + (Sum (f /^ (i + 1)))