theorem :: RVSUM_1:51

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