let f, g be non empty real-valued positive FinSequence; :: thesis: ( len f = len g & Product f < Product g implies GMean f < GMean g )
A1: ( Product f >= 0 & len f >= 1 ) by NAT_1:14;
assume ( len f = len g & Product f < Product g ) ; :: thesis: GMean f < GMean g
hence GMean f < GMean g by POWER:17, A1; :: thesis: verum