let a, r be Real; :: thesis: multreal .: (((Seg 1) --> a),<*r*>) = <*(a * r)*>
reconsider r1 = a, r2 = r as Element of REAL by XREAL_0:def 1;
a is Element of REAL by XREAL_0:def 1;
then multreal .: (((Seg 1) --> a),<*r*>) = multreal .: (<*a*>,<*r*>) by Th20
.= <*(multreal . (r1,r2))*> by FINSEQ_2:74
.= <*(r1 * r2)*> by BINOP_2:def 11 ;
hence multreal .: (((Seg 1) --> a),<*r*>) = <*(a * r)*> ; :: thesis: verum