theorem :: RVSUM_1:62

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