let f be homogeneous non empty real-valued positive FinSequence; :: thesis: Mean f = GMean f
the_value_of f = Mean f by ConstantMean;
hence Mean f = GMean f by ConstantGMean; :: thesis: verum