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