theorem Th6: :: TAYLOR_2:6
for Z being open Subset of REAL
for n being Nat holds (diff (exp_R,Z)) . n = exp_R | Z