theorem Th28: :: TAYLOR_1:28

for n being Nat
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & f is_differentiable_on n,Z holds
for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ holds
for l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )