let a be positive Real; :: thesis: GMean <*a*> = a
len <*a*> = 1 by CARD_1:def 7;
hence GMean <*a*> = a by POWER:9; :: thesis: verum