let n be Nat; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
let Z be Subset of REAL; :: thesis:
assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; :: thesis:
let a, b be Real; :: thesis:
assume that
A2: a < b and
A3: [.a,b.] c= Z and
A4: ( ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; :: thesis:
let l be Real; :: thesis:
consider p being PartFunc of REAL,REAL such that
A5: dom p = [#] REAL and
A6: for x being Real holds p . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) and
A7: for x being Real holds
( p is_differentiable_in x & diff (p,x) = - ((l * ((b - x) |^ n)) / (n !)) ) by Lm6;
consider h being PartFunc of REAL,REAL such that
A8: dom h = Z and
A9: for x being Real st x in Z holds
h . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) and
A10: h . b = 0 and
A11: h | [.a,b.] is continuous and
A12: h is_differentiable_on ].a,b.[ and
A13: for x being Real st x in ].a,b.[ holds
diff (h,x) = - (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !)) by A1, A2, A3, A4, Lm9;
A14: [.a,b.] c= (dom h) /\ (dom p) by A3, A8, A5, XBOOLE_1:19;
let g be PartFunc of REAL,REAL; :: thesis:
assume that
A15: dom g = [#] REAL and
A16: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) and
A17: ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 ; :: thesis:
set hp = h - p;
A18: dom (h - p) = (dom h) /\ (dom p) by VALUED_1:12
.= Z by A8, A5, XBOOLE_1:28 ;
A19: for x being object st x in dom (h - p) holds
(h - p) . x = g . x

proof

let x be object ; :: thesis:
assume A20: x in dom (h - p) ; :: thesis:
reconsider xx = x as Real by A20;
thus (h - p) . x = (h . xx) - (p . xx) by A20, VALUED_1:13
.= ((f . b) - ((Partial_Sums (Taylor (f,Z,xx,b))) . n)) - (p . xx) by A9, A18, A20
.= ((f . b) - ((Partial_Sums (Taylor (f,Z,xx,b))) . n)) - ((l * ((b - xx) |^ (n + 1))) / ((n + 1) !)) by A6
.= g . x by A16 ; :: thesis:

end;

for x being Real st x in REAL holds
p is_differentiable_in x by A7;
then p is_differentiable_on REAL by A5, FDIFF_1:9;
then p | REAL is continuous by FDIFF_1:25;
then A21: p | [.a,b.] is continuous by FCONT_1:16;
].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A22: ].a,b.[ c= Z by A3, XBOOLE_1:1;
A23: dom (h - p) = (dom g) /\ Z by A15, A18, XBOOLE_1:28;
then A24: (h - p) | ].a,b.[ = (g | Z) | ].a,b.[ by A19, FUNCT_1:46
.= g | ].a,b.[ by A22, FUNCT_1:51 ;
A25: for x being Real st x in ].a,b.[ holds
( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) )

proof

let x be Real; :: thesis:
assume A26: x in ].a,b.[ ; :: thesis:
A27: h is_differentiable_in x by A12, A26, FDIFF_1:9;
A28: p is_differentiable_in x by A7;
hence h - p is_differentiable_in x by A27, FDIFF_1:14; :: thesis:
thus diff ((h - p),x) = (diff (h,x)) - (diff (p,x)) by A27, A28, FDIFF_1:14
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) - (diff (p,x)) by A13, A26
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) - (- ((l * ((b - x) |^ n)) / (n !))) by A7
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) ; :: thesis:

end;

then for x being Real st x in ].a,b.[ holds
h - p is_differentiable_in x ;
then A29: h - p is_differentiable_on ].a,b.[ by A18, A22, FDIFF_1:9;
then for x being Real st x in ].a,b.[ holds
(h - p) | ].a,b.[ is_differentiable_in x by FDIFF_1:def 6;
hence A30: g is_differentiable_on ].a,b.[ by A15, A24, FDIFF_1:def 6; :: thesis:
reconsider aa = a as Real ;
g . aa = 0 by A16, A17;
hence g . a = 0 ; :: thesis:
A31: b in [.a,b.] by A2, XXREAL_1:1;
then g . b = (h - p) . b by A3, A18, A19
.= (h . b) - (p . b) by A3, A18, A31, VALUED_1:13
.= 0 - ((l * ((b - b) |^ (n + 1))) / ((n + 1) !)) by A10, A6
.= 0 - ((l * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6
.= 0 ;
hence g . b = 0 ; :: thesis:
(h - p) | [.a,b.] = (g | Z) | [.a,b.] by A23, A19, FUNCT_1:46
.= g | [.a,b.] by A3, FUNCT_1:51 ;
hence g | [.a,b.] is continuous by A11, A14, A21, FCONT_1:18; :: thesis:
thus for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) :: thesis:

proof

let x be Real; :: thesis:
assume A32: x in ].a,b.[ ; :: thesis:
thus diff (g,x) = (g `| ].a,b.[) . x by A30, A32, FDIFF_1:def 7
.= ((g | ].a,b.[) `| ].a,b.[) . x by A30, FDIFF_2:16
.= ((h - p) `| ].a,b.[) . x by A24, A29, FDIFF_2:16
.= diff ((h - p),x) by A29, A32, FDIFF_1:def 7
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) by A25, A32 ; :: thesis:

end;