:: deftheorem defines * RVSUM_1:def 7 :
for F being real-valued FinSequence
for r being Real holds r * F = (r multreal) * F;