theorem Th17: :: LPSPACE2:17

for a, b, k being Real st a >= 0 & b >= 0 & k > 0 holds
(max (a,b)) to_power k <= (a to_power k) + (b to_power k)