theorem :: RVSUM_1:6

for r being Real holds r multreal is_distributive_wrt addreal