let n be Element of NAT ; :: thesis: for r, x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
|.(((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| <= (|.(exp_R . (s * x)).| * (|.x.| |^ (n + 1))) / ((n + 1) !)

let r, x, s be Real; :: thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies |.(((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| <= (|.(exp_R . (s * x)).| * (|.x.| |^ (n + 1))) / ((n + 1) !) )
assume that
A1: x in ].(- r),r.[ and
A2: 0 < s and
A3: s < 1 ; :: thesis: |.(((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| <= (|.(exp_R . (s * x)).| * (|.x.| |^ (n + 1))) / ((n + 1) !)
A4: |.((s * x) - 0).| = |.s.| * |.x.| by COMPLEX1:65
.= s * |.x.| by ;
x in ].(0 - r),(0 + r).[ by A1;
then A5: |.(x - 0).| < r by RCOMP_1:1;
|.x.| >= 0 by COMPLEX1:46;
then |.x.| * s < r * 1 by ;
then s * x in ].(0 - r),(0 + r).[ by ;
then A6: s * x in dom (exp_R | ].(- r),r.[) by Th5;
A7: |.((n + 1) !).| = (n + 1) ! by ABSVALUE:def 1;
|.(((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| = |.((((exp_R | ].(- r),r.[) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| by Th6
.= |.(((exp_R . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| by
.= |.((exp_R . (s * x)) * (x |^ (n + 1))).| / |.((n + 1) !).| by COMPLEX1:67
.= (|.(exp_R . (s * x)).| * |.(x |^ (n + 1)).|) / ((n + 1) !) by ;
hence |.(((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| <= (|.(exp_R . (s * x)).| * (|.x.| |^ (n + 1))) / ((n + 1) !) by Th1; :: thesis: verum