theorem Th7: :: TAYLOR_2:7

for Z being open Subset of REAL
for n being Nat
for x being Real st x in Z holds
((diff (exp_R,Z)) . n) . x = exp_R . x