for f, g being FinSequence of COMPLEX
for n being Nat st len f = n + 1 & g = f | n holds
Sum f = (Sum g) + (f /. (len f))