theorem ConstantMean: :: RVSUM_3:9

for f being constant non empty real-valued FinSequence holds Mean f = the_value_of f