theorem :: TAYLOR_2:14

for r, e being Real st 0 < r & 0 < e holds
ex n being Nat st
for m being Nat st n <= m holds
for x being Real st x in ].(- r),r.[ holds
|.((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)).| < e