let n be Element of NAT ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( 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.[ ) ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum