theorem :: RVSUM_1:46

for r being Real holds r * (<*> REAL) = <*> REAL ;