let i be Nat; :: thesis: for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R
let R be Element of i -tuples_on REAL; :: thesis: mlt ((i |-> 1),R) = R
thus mlt ((i |-> 1),R) = 1 * R by RVSUM_1:63
.= R by RVSUM_1:52 ; :: thesis: verum