:: deftheorem defines multreal RVSUM_1:def 3 :
for x being Real holds x multreal = multreal [;] (x,(id REAL));