let r, r1 be Real; :: thesis: (multreal [;] (r,(id REAL))) . r1 = r * r1
reconsider a = r, s = r1 as Element of REAL by XREAL_0:def 1;
thus (multreal [;] (r,(id REAL))) . r1 = multreal . (a,((id REAL) . s)) by FUNCOP_1:53
.= multreal . (a,s)
.= r * r1 by BINOP_2:def 11 ; :: thesis: verum