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

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

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

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

end;

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

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

end;

end;