theorem :: NUMBER17:96

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