theorem LMN: :: COMPLEX3:69
for k being positive Real
for n being non positive Real holds (k + 1) to_power n < (k to_power n) + 1