theorem :: RVSUM_1:47

for r, r1 being Real holds r * <*r1*> = <*(r * r1)*>