theorem :: RVSUM_1:49

for r1, r2 being Real
for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:17;