theorem :: RVSUM_4:6

for f being complex-valued FinSequence holds Sum f = (f . 1) + (Sum (f /^ 1))