theorem :: NUMBER17:90

for a being positive Real holds GMean <*a*> = a