theorem Th20: :: FLEXARY1:20

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