theorem Th11: :: TAYLOR_2:11

for r being Real st 0 < r holds
ex M, L being Real st
( 0 <= M & 0 <= L & ( for n being Nat
for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds
|.(((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)).| <= (M * (L |^ n)) / (n !) ) )