theorem ConstantGMean: :: RVSUM_3:11

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