theorem :: NUMBER17:94

for a being Real holds Mean <*a*> = a