theorem :: RVSUM_1:64

for i being natural Number
for r1, r2 being Real holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2)