let i be natural Number ; :: thesis: for r1, r2 being Real holds r1 * (i |-> r2) = i |-> (r1 * r2)
let r1, r2 be Real; :: thesis: r1 * (i |-> r2) = i |-> (r1 * r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
s1 * (i |-> s2) = i |-> ((multreal [;] (s1,(id REAL))) . s2) by FINSEQOP:16
.= i |-> (r1 * r2) by Lm1 ;
hence r1 * (i |-> r2) = i |-> (r1 * r2) ; :: thesis: verum