let i be Nat; :: thesis: for r being real number
for R being Element of i -tuples_on REAL holds mlt (i |-> r),R = r * R
let r be real number ; :: 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:21
.= r * R by FINSEQOP:23 ;
hence mlt (i |-> r),R = r * R ; :: thesis: verum