A1: abs (0 - 0 ) = 0 by ABSVALUE:7;
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 A1, RCOMP_1:8;
then A2: 0 in dom (exp_R | ].(- r),r.[) by Th5;

now

let t be set ; :: thesis: ( t in NAT implies (Maclaurin exp_R ,].(- r),r.[,x) . t = (x rExpSeq ) . t )
assume t in NAT ; :: thesis: (Maclaurin exp_R ,].(- r),r.[,x) . t = (x rExpSeq ) . 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
.= ((exp_R . 0 ) * (x |^ n)) / (n ! ) by A2, FUNCT_1:70
.= (x rExpSeq ) . t by SIN_COS:def 9, SIN_COS2:13 ; :: thesis: verum

end;

then Maclaurin exp_R ,].(- r),r.[,x = x rExpSeq by FUNCT_2:18;
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 Th15, SIN_COS:def 26; :: thesis: verum