let n be Element of NAT ; 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; ( 0 < r implies (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) )
assume
r > 0
; (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 !)
; verum