theorem :: NEWTON05:10

for a being non zero Nat
for m, n being Nat holds max ((a |^ n),(a |^ m)) = a |^ (max (n,m))