let k be positive Real; :: thesis: for n being positive light Real holds (k + 1) to_power n < (k to_power n) + 1
let n be positive light 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 BPA;
hence (k + 1) to_power n < (k to_power n) + 1 ; :: thesis: verum