theorem HomGMean: :: RVSUM_3:45

for f being heterogeneous non empty real-valued positive FinSequence holds GMean (Homogen f) > GMean f