theorem :: TAYLOR_2:16

for r, x being Real st 0 < r holds
( 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)) )