theorem :: NEWTON05:7

for a, b being positive Real
for n being Nat holds min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n