theorem ConstantSum: :: RVSUM_3:7

for f being constant non empty real-valued FinSequence holds Sum f = (the_value_of f) * (len f)