theorem MM1: :: NEWTON03:42

for n being Nat
for a, b being non negative Real holds
( max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n & min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n )