theorem Th16: :: TAYLOR_1:16

( exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )