let i be Nat; :: thesis: for r1, r2 being real number holds mlt (i |-> r1),(i |-> r2) = i |-> (r1 * r2)
let r1, r2 be real number ; :: thesis: mlt (i |-> r1),(i |-> r2) = i |-> (r1 * r2)
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
mlt (i |-> s1),(i |-> s2) = s1 * (i |-> s2) by Th92
.= i |-> (r1 * r2) by Th70 ;
hence mlt (i |-> r1),(i |-> r2) = i |-> (r1 * r2) ; :: thesis: verum