theorem :: RVSUM_3:47

for f being non empty real-valued positive FinSequence holds GMean f <= Mean f