let i be natural Number ; :: thesis: for r being Real
for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R
let r be Real; :: thesis: for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R
let R be Element of i -tuples_on REAL; :: thesis: mlt ((i |-> r),R) = r * R
reconsider s = r as Element of REAL by XREAL_0:def 1;
mlt ((i |-> s),R) = multreal [;] (s,R) by FINSEQOP:20
.= r * R by FINSEQOP:22 ;
hence mlt ((i |-> r),R) = r * R ; :: thesis: verum