for i being Nat
for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R