theorem :: RVSUM_1:5

for r, r1 being Real holds (r multreal) . r1 = r * r1 by Lm1;