theorem Th74: :: RVSUM_1:74

for r being Real
for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r