let n be Element of NAT ; :: thesis: for r, x being Real st 0 < r holds
(Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !)
A1: |.(0 - 0).| = 0 by ABSVALUE:2;
let r, x be Real; :: thesis: ( 0 < r implies (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) )
assume r > 0 ; :: thesis: (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !)
then 0 in ].(0 - r),(0 + r).[ by A1, RCOMP_1:1;
then A2: 0 in dom (exp_R | ].(- r),r.[) by Th5;
(Maclaurin (exp_R,].(- r),r.[,x)) . n = ((((diff (exp_R,].(- r),r.[)) . n) . 0) * ((x - 0) |^ n)) / (n !) by TAYLOR_1:def 7
.= (((exp_R | ].(- r),r.[) . 0) * (x |^ n)) / (n !) by Th6
.= ((exp_R . 0) * (x |^ n)) / (n !) by A2, FUNCT_1:47
.= (x |^ n) / (n !) by SIN_COS2:13 ;
hence (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) ; :: thesis: verum