theorem :: RVSUM_4:48

for f being complex-valued XFinSequence holds Sum (f | 1) = f . 0