theorem Th17: :: TAYLOR_1:17

( exp_R " is_differentiable_on dom (exp_R ") & ( for x being Real st x in dom (exp_R ") holds
diff ((exp_R "),x) = 1 / x ) )