theorem :: RVSUM_1:65

for r being Real
for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:12;