theorem Th4: :: NUMBER17:4

for s being positive Nat
for f being b₁ -element complex-valued FinSequence holds Sum (f | (s - 1)) = (Sum f) - (f . s)