theorem Pow: :: COMPLEX3:62

for a, b being positive Real
for m being non negative Real
for n being positive Real st (a to_power m) + (b to_power m) <= 1 holds
(a to_power (m + n)) + (b to_power (m + n)) < 1