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 A2, ABSVALUE:def 1 ;
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 A2, A3, A5, XREAL_1:97;
then s * x in ].(0 - r),(0 + r).[ by A4, RCOMP_1:1;
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 A6, FUNCT_1:47
.= |.((exp_R . (s * x)) * (x |^ (n + 1))).| / |.((n + 1) !).| by COMPLEX1:67
.= (|.(exp_R . (s * x)).| * |.(x |^ (n + 1)).|) / ((n + 1) !) by A7, COMPLEX1:65 ;
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