let a be Real; :: thesis: for p being Tuple of 1, REAL holds multreal .: (((dom p) --> a),p) = a * p
let p be Tuple of 1, REAL ; :: thesis: multreal .: (((dom p) --> a),p) = a * p
consider d being Element of REAL such that
A1: p = <*d*> by FINSEQ_2:97;
A2: a * p = <*(a * d)*> by A1, RVSUM_1:47;
dom p = Seg 1 by A1, FINSEQ_1:def 8;
hence multreal .: (((dom p) --> a),p) = a * p by A1, A2, Th21; :: thesis: verum