theorem :: NUMBER17:95

for a, b being Real holds Mean <*a,b*> = (a + b) / 2