theorem Th31: :: RVSUM_2:31

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