let i be Nat; :: thesis: for r being real number
for R1, R2 being Element of i -tuples_on REAL holds r * (mlt R1,R2) = mlt (r * R1),R2
let r be real number ; :: thesis: for R1, R2 being Element of i -tuples_on REAL holds r * (mlt R1,R2) = mlt (r * R1),R2
let R1, R2 be Element of i -tuples_on REAL ; :: thesis: r * (mlt R1,R2) = mlt (r * R1),R2
r in REAL by XREAL_0:def 1;
hence r * (mlt R1,R2) = mlt (r * R1),R2 by FINSEQOP:27; :: thesis: verum