A1: |.().| = 0 by ABSVALUE:2;
let r, x be Real; :: thesis: ( 0 < r implies ( Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq & Maclaurin (exp_R,].(- r),r.[,x) is absolutely_summable & exp_R . x = Sum (Maclaurin (exp_R,].(- r),r.[,x)) ) )
assume r > 0 ; :: thesis: ( Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq & Maclaurin (exp_R,].(- r),r.[,x) is absolutely_summable & exp_R . x = Sum (Maclaurin (exp_R,].(- r),r.[,x)) )
then 0 in ].(0 - r),(0 + r).[ by ;
then A2: 0 in dom (exp_R | ].(- r),r.[) by Th5;
now :: thesis: for t being object st t in NAT holds
(Maclaurin (exp_R,].(- r),r.[,x)) . t = () . t
let t be object ; :: thesis: ( t in NAT implies (Maclaurin (exp_R,].(- r),r.[,x)) . t = () . t )
assume t in NAT ; :: thesis: (Maclaurin (exp_R,].(- r),r.[,x)) . t = () . t
then reconsider n = t as Element of NAT ;
thus (Maclaurin (exp_R,].(- r),r.[,x)) . t = ((((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
.= (() * (x |^ n)) / (n !) by
.= () . t by ; :: thesis: verum
end;
then Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq by FUNCT_2:12;
hence ( Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq & Maclaurin (exp_R,].(- r),r.[,x) is absolutely_summable & exp_R . x = Sum (Maclaurin (exp_R,].(- r),r.[,x)) ) by ; :: thesis: verum