let f be constant non empty real-valued positive FinSequence; :: thesis: GMean f = the_value_of f
reconsider v = the_value_of f as Real ;
A3: len f >= 1 by NAT_1:14;
A4: v >= 0 by PosLeq;
Product f = v |^ (len f) by ConstantProduct;
hence GMean f = the_value_of f by A4, A3, POWER:4; :: thesis: verum