theorem Th12: :: FLEXARY1:12

for k, n being Nat
for f being complex-valued Function st k <= n + 1 holds
(f,k) +...+ (f,(n + 1)) = ((f,k) +...+ (f,n)) + (f . (n + 1))