theorem Th63: :: RVSUM_1:63

for i being natural Number
for r being Real
for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R