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 A1: ( 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 A2: ( a to_power k >= 0 & b to_power k >= 0 ) by A1, POWER:34;
( 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 A2, XREAL_1:40; :: 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 A1, POWER:def 2;
hence (max (a,b)) to_power k <= (a to_power k) + (b to_power k) by A1, A3, XXREAL_0:def 10; :: thesis: verum

end;

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

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

end;

end;