let r1, r2 be real number ; :: 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:88
.= <*(r1 * r2)*> by BINOP_2:def 11 ;
hence mlt <*r1*>,<*r2*> = <*(r1 * r2)*> ; :: thesis: verum