theorem :: RVSUM_2:33

for c being Complex
for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)