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