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