let r, r1 be real number ; :: 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:66
.= multreal . a,s by FUNCT_1:35
.= r * r1 by BINOP_2:def 11 ; :: thesis: verum