theorem :: RVSUM_1:59

for s being set
for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;