theorem Th97: :: NUMBER17:97

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