let a, b, k be Real; :: thesis: ( a >= 0 & b >= 0 & k > 0 implies (max a,b) to_power k <= (a to_power k) + (b to_power k) )
assume A0: ( a >= 0 & b >= 0 & k > 0 ) ; :: thesis: (max a,b) to_power k <= (a to_power k) + (b to_power k)

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

suppose ( a <> 0 & b <> 0 ) ; :: thesis: (max a,b) to_power k <= (a to_power k) + (b to_power k)

then A1: ( a to_power k >= 0 & b to_power k >= 0 ) by A0, POWER:39;
( max a,b = a or max a,b = b ) by XXREAL_0:def 10;
hence (max a,b) to_power k <= (a to_power k) + (b to_power k) by A1, XREAL_1:42; :: thesis: verum

end;

suppose A3: a = 0 ; :: thesis: (max a,b) to_power k <= (a to_power k) + (b to_power k)

then a to_power k = 0 by A0, POWER:def 2;
hence (max a,b) to_power k <= (a to_power k) + (b to_power k) by A0, A3, XXREAL_0:def 10; :: thesis: verum

end;

suppose A6: b = 0 ; :: thesis: (max a,b) to_power k <= (a to_power k) + (b to_power k)

then b to_power k = 0 by A0, POWER:def 2;
hence (max a,b) to_power k <= (a to_power k) + (b to_power k) by A0, A6, XXREAL_0:def 10; :: thesis: verum

end;

end;