theorem Th21: :: LPSPACE2:21

for a, b, k being Real st k > 0 holds
|.(a + b).| to_power k <= (2 to_power k) * ((|.a.| to_power k) + (|.b.| to_power k))