let x, r be Real; :: thesis: ( x > 0 & r > 0 implies Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding )
assume A0: ( x > 0 & r > 0 ) ; :: thesis: Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding
set f = Maclaurin (exp_R,].(- r),r.[,x);
for r being Real st r in rng (Maclaurin (exp_R,].(- r),r.[,x)) holds
0 < r

proof

let r be Real; :: thesis: ( r in rng (Maclaurin (exp_R,].(- r),r.[,x)) implies 0 < r )
assume r in rng (Maclaurin (exp_R,].(- r),r.[,x)) ; :: thesis: 0 < r
then consider xx being object such that
A1: ( xx in dom (Maclaurin (exp_R,].(- r),r.[,x)) & r = (Maclaurin (exp_R,].(- r),r.[,x)) . xx ) by FUNCT_1:def 3;
reconsider nn = xx as Element of NAT by A1;
r = (x |^ nn) / (nn !) by A1, TAYLOR_2:8, A0;
hence 0 < r by A0; :: thesis: verum

end;

hence Maclaurin (exp_R,].(- r),r.[,x) is positive-yielding by PARTFUN3:def 1; :: thesis: verum