theorem Th4: :: TAYLOR_2:4

for n being Nat
for f being PartFunc of REAL,REAL
for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds
for x being Real st x in ].(- r),r.[ holds
ex s being Real st
( 0 < s & s < 1 & |.((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)).| = |.(((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)).| )