let k be Nat; for r being Real st 0 < r & r < 1 / 2 holds
(1 + r) |^ k < 1 + (r * (2 |^ k))
let r be Real; ( 0 < r & r < 1 / 2 implies (1 + r) |^ k < 1 + (r * (2 |^ k)) )
assume A1:
( 0 < r & r < 1 / 2 )
; (1 + r) |^ k < 1 + (r * (2 |^ k))
defpred S1[ Nat] means (1 + r) |^ $1 < 1 + (r * (2 |^ $1));