let s be positive Nat; :: thesis: for f being s -element complex-valued FinSequence holds Sum (f | (s - 1)) = (Sum f) - (f . s)
let f be s -element complex-valued FinSequence; :: thesis: Sum (f | (s - 1)) = (Sum f) - (f . s)
A1: len f = s by CARD_1:def 7;
s - 1 < s by XREAL_1:147;
then Sum (f | ((s - 1) + 1)) = (Sum (f | (s - 1))) + (f . ((s - 1) + 1)) by A1, POLYNOM3:20;
hence Sum (f | (s - 1)) = (Sum f) - (f . s) by A1; :: thesis: verum