let a, b be positive Real; :: thesis: for n being Nat holds max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n
let n be Nat; :: thesis: max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n

per cases ( a >= b or b >= a ) ;

suppose A1: a >= b ; :: thesis: max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n

then max (a,b) = a by XXREAL_0:def 10;
hence max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n by A1, NEWTON02:41, XXREAL_0:def 10; :: thesis: verum

end;

suppose A1: b >= a ; :: thesis: max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n

then max (a,b) = b by XXREAL_0:def 10;
hence max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n by A1, NEWTON02:41, XXREAL_0:def 10; :: thesis: verum

end;

end;