let i be Element of 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:92
.= R by RVSUM_1:74 ; :: thesis: verum