let r, e be Real; :: thesis: ( 0 < r & 0 < e implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e )
assume that
A1: r > 0 and
A2: e > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e
consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e by A1, A2, Th13;
take n ; :: thesis: for m being Element of NAT st n <= m holds
for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e
let m be Element of NAT ; :: thesis: ( n <= m implies for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e )
assume A4: n <= m ; :: thesis: for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e

now

m <= m + 1 by NAT_1:11;
then A5: n <= m + 1 by A4, XXREAL_0:2;
let x be Real; :: thesis: ( x in ].(- r),r.[ implies abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e )
assume A6: x in ].(- r),r.[ ; :: thesis: abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e
ex s being Real st
( 0 < s & s < 1 & abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) = abs (((((diff (exp_R,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)) ) by A1, A6, Th4, Th10, SIN_COS:47;
hence abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e by A3, A6, A5; :: thesis: verum

end;

hence for x being real number st x in ].(- r),r.[ holds
abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ; :: thesis: verum