theorem Th48: :: RVSUM_1:48

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