let n be 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
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
let f be 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
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
let Z be Subset of REAL; ( Z c= dom f & f is_differentiable_on n,Z implies 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
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) )
assume A1:
( Z c= dom f & f is_differentiable_on n,Z )
; 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
ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
let a, b be Real; ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) ) )
assume A2:
( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ )
; ex g being PartFunc of REAL,REAL st
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
consider g being PartFunc of REAL,REAL such that
A3:
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
by Lm7;
take
g
; ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
thus
( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & g . b = 0 & g | [.a,b.] is continuous & g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) ) )
by A1, A2, A3, Lm8; verum