let n be Nat; :: thesis: 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 )
let a, b be non negative Real; :: thesis: ( max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n & min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n )

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

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

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

end;

suppose a < b ; :: thesis: ( max ((a |^ n),(b |^ n)) = (max (a,b)) |^ n & min ((a |^ n),(b |^ n)) = (min (a,b)) |^ n )

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

end;

end;