theorem :: COMPLEX3:66

for k being positive Real
for n being positive heavy Real holds (k + 1) to_power n > (k to_power n) + 1