theorem :: RVSUM_1:45

for s being set
for r being Real
for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;