A2: len f >= 1 by NAT_1:14;
(len f) -root (Product f) = (len f) -Root (Product f) by POWER:def 1, NAT_1:14;
hence GMean f is positive by A2, PREPOWER:def 2; :: thesis: verum