let r, r1 be Real; :: thesis: r * <*r1*> = <*(r * r1)*>
reconsider s = r, s1 = r1 as Element of REAL by XREAL_0:def 1;
s * <*s1*> = <*((multreal [;] (s,(id REAL))) . s1)*> by FINSEQ_2:35
.= <*(r * r1)*> by Lm1 ;
hence r * <*r1*> = <*(r * r1)*> ; :: thesis: verum