for x being Element of REAL holds 1 + x <= exp_R . x