theorem :: TAYLOR_2:3

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