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