let k be positive Real; :: thesis: for n being positive heavy Real holds (k + 1) to_power n > (k to_power n) + 1
let n be positive heavy Real; :: thesis: (k + 1) to_power n > (k to_power n) + 1
(k + 1) to_power n > (k to_power n) + (1 to_power n) by APB;
hence (k + 1) to_power n > (k to_power n) + 1 ; :: thesis: verum