let r1, r2 be Real; :: thesis: mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*>
reconsider s1 = r1, s2 = r2 as Element of REAL by XREAL_0:def 1;
mlt (<*s1*>,<*s2*>) = <*(multreal . (s1,s2))*> by FINSEQ_2:74
.= <*(r1 * r2)*> by BINOP_2:def 11 ;
hence mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*> ; :: thesis: verum