theorem Th87: :: RVSUM_1:87

for r being Real
for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F)