let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL st Z c= dom f holds
for n being Nat st 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 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) ) holds
( 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 implies for n being Nat st 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 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) ) holds
( 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 ; :: thesis: for n being Nat st 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 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) ) holds
( 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 !)) ) )
defpred S₁[ Nat] means ( f is_differentiable_on $1,Z implies for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . $1) | [.a,b.] is continuous & f is_differentiable_on $1 + 1,].a,b.[ holds
for 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))) . $1) ) holds
( 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.[)) . ($1 + 1)) . x) * ((b - x) |^ $1)) / ($1 !)) ) ) );
A2: S₁[ 0 ]

proof

assume f is_differentiable_on 0 ,Z ; :: thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ holds
for 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))) . 0) ) holds
( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . 0) | [.a,b.] is continuous & f is_differentiable_on 0 + 1,].a,b.[ implies for 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))) . 0) ) holds
( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) )
assume that
A3: a < b and
A4: [.a,b.] c= Z and
A5: ((diff (f,Z)) . 0) | [.a,b.] is continuous and
A6: f is_differentiable_on 0 + 1,].a,b.[ ; :: thesis: for 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))) . 0) ) holds
( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
A7: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A8: ].a,b.[ c= Z by A4, XBOOLE_1:1;
let g be PartFunc of REAL,REAL; :: thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ) implies ( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) ) )
assume that
A9: dom g = Z and
A10: for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) ; :: thesis: ( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
A11: b in [.a,b.] by A3, XXREAL_1:1;
hence g . b = (f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . 0) by A4, A10
.= (f . b) - ((Taylor (f,Z,b,b)) . 0) by SERIES_1:def 1
.= (f . b) - (((((diff (f,Z)) . 0) . b) * ((b - b) |^ 0)) / (0 !)) by Def7
.= (f . b) - ((((f | Z) . b) * ((b - b) |^ 0)) / (0 !)) by Def5
.= (f . b) - (((f . b) * ((b - b) |^ 0)) / (0 !)) by A4, A11, FUNCT_1:49
.= (f . b) - ((f . b) * 1) by NEWTON:4, NEWTON:12
.= 0 ;
:: thesis: ( 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.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
consider y being PartFunc of REAL,REAL such that
A12: dom y = [#] REAL and
A13: for x being Real holds y . x = (f . b) - x and
A14: for x being Real holds
( y is_differentiable_in x & diff (y,x) = - 1 ) by Lm5;
rng f c= REAL ;
then A15: dom (y * f) = dom f by A12, RELAT_1:27;
for x being Real st x in REAL holds
y is_differentiable_in x by A14;
then y is_differentiable_on REAL by A12, FDIFF_1:9;
then y | REAL is continuous by FDIFF_1:25;
then A16: y | (f .: [.a,b.]) is continuous by FCONT_1:16;
rng f c= dom y by A12;
then A17: dom (y * f) = dom f by RELAT_1:27;
A18: [.a,b.] c= dom f by A1, A4, XBOOLE_1:1;
then A19: ].a,b.[ c= dom f by A7, XBOOLE_1:1;
(diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A6;
then f | ].a,b.[ is_differentiable_on ].a,b.[ by Def5;
then for x being Real st x in ].a,b.[ holds
f | ].a,b.[ is_differentiable_in x by FDIFF_1:9;
then A20: f is_differentiable_on ].a,b.[ by A19, FDIFF_1:def 6;
A21: for x being Real st x in ].a,b.[ holds
( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) )

proof

A22: (diff (f,].a,b.[)) . (0 + 1) = ((diff (f,].a,b.[)) . 0) `| ].a,b.[ by Def5
.= (f | ].a,b.[) `| ].a,b.[ by Def5
.= f `| ].a,b.[ by A20, FDIFF_2:16 ;
let x be Real; :: thesis: ( x in ].a,b.[ implies ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
assume A23: x in ].a,b.[ ; :: thesis: ( y * f is_differentiable_in x & diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) )
A24: f is_differentiable_in x by A20, A23, FDIFF_1:9;
A25: y is_differentiable_in f . x by A14;
hence y * f is_differentiable_in x by A24, FDIFF_2:13; :: thesis: diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !))
A26: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus diff ((y * f),x) = (diff (y,(f . x))) * (diff (f,x)) by A25, A24, FDIFF_2:13
.= (diff (y,(f . x))) * ((f `| ].a,b.[) . x) by A20, A23, FDIFF_1:def 7
.= (- 1) * (((diff (f,].a,b.[)) . (0 + 1)) . x) by A14, A22
.= - ((((diff (f,].a,b.[)) . (0 + 1)) . x) * (((b - x) |^ 0) / (0 !))) by A26
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) by XCMPLX_1:74 ; :: thesis: verum

end;

then for x being Real st x in ].a,b.[ holds
y * f is_differentiable_in x ;
then A27: y * f is_differentiable_on ].a,b.[ by A19, A17, FDIFF_1:9;
A28: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by RELAT_1:61
.= [.a,b.] by A1, A4, A15, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ [.a,b.] by A4, XBOOLE_1:28
.= dom (g | [.a,b.]) by A9, RELAT_1:61 ;

A29: now :: thesis: for xx being object st xx in dom (g | [.a,b.]) holds
(g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx

let xx be object ; :: thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx )
assume A30: xx in dom (g | [.a,b.]) ; :: thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx
reconsider x = xx as Real by A30;
dom (g | [.a,b.]) = (dom g) /\ [.a,b.] by RELAT_1:61;
then dom (g | [.a,b.]) c= [.a,b.] by XBOOLE_1:17;
then A31: x in [.a,b.] by A30;
A32: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus (g | [.a,b.]) . xx = g . x by A30, FUNCT_1:47
.= (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) by A4, A10, A31
.= (f . b) - ((Taylor (f,Z,x,b)) . 0) by SERIES_1:def 1
.= (f . b) - (((((diff (f,Z)) . 0) . x) * ((b - x) |^ 0)) / (0 !)) by Def7
.= (f . b) - ((((f | Z) . x) * ((b - x) |^ 0)) / (0 !)) by Def5
.= (f . b) - (((f . x) * ((b - x) |^ 0)) / (0 !)) by A4, A31, FUNCT_1:49
.= (f . b) - ((f . x) * (((b - x) |^ 0) / (0 !))) by XCMPLX_1:74
.= y . (f . x) by A13, A32
.= (y * f) . x by A18, A31, FUNCT_1:13
.= ((y * f) | [.a,b.]) . xx by A28, A30, FUNCT_1:47 ; :: thesis: verum

end;

(f | Z) | [.a,b.] is continuous by A5, Def5;
then ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:15;
then (f | [.a,b.]) | [.a,b.] is continuous by A4, FUNCT_1:51;
then f | [.a,b.] is continuous by FCONT_1:15;
then (y * f) | [.a,b.] is continuous by A16, FCONT_1:25;
hence g | [.a,b.] is continuous by A28, A29, FUNCT_1:2; :: thesis: ( g is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
A33: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A7, A18, A17, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ ].a,b.[ by A4, A7, XBOOLE_1:1, XBOOLE_1:28
.= dom (g | ].a,b.[) by A9, RELAT_1:61 ;

now :: thesis: for xx being object st xx in dom (g | ].a,b.[) holds
(g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx

let xx be object ; :: thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx )
assume A34: xx in dom (g | ].a,b.[) ; :: thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx
reconsider x = xx as Real by A34;
dom (g | ].a,b.[) = (dom g) /\ ].a,b.[ by RELAT_1:61;
then dom (g | ].a,b.[) c= ].a,b.[ by XBOOLE_1:17;
then A35: x in ].a,b.[ by A34;
A36: ((b - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus (g | ].a,b.[) . xx = g . x by A34, FUNCT_1:47
.= (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . 0) by A10, A8, A35
.= (f . b) - ((Taylor (f,Z,x,b)) . 0) by SERIES_1:def 1
.= (f . b) - (((((diff (f,Z)) . 0) . x) * ((b - x) |^ 0)) / (0 !)) by Def7
.= (f . b) - ((((f | Z) . x) * ((b - x) |^ 0)) / (0 !)) by Def5
.= (f . b) - (((f . x) * ((b - x) |^ 0)) / (0 !)) by A8, A35, FUNCT_1:49
.= (f . b) - ((f . x) * (((b - x) |^ 0) / (0 !))) by XCMPLX_1:74
.= y . (f . x) by A13, A36
.= (y * f) . x by A19, A35, FUNCT_1:13
.= ((y * f) | ].a,b.[) . xx by A33, A34, FUNCT_1:47 ; :: thesis: verum

end;

then A37: g | ].a,b.[ = (y * f) | ].a,b.[ by A33, FUNCT_1:2;
then g | ].a,b.[ is_differentiable_on ].a,b.[ by A27, FDIFF_2:16;
then for x being Real st x in ].a,b.[ holds
g | ].a,b.[ is_differentiable_in x by FDIFF_1:9;
hence A38: g is_differentiable_on ].a,b.[ by A9, A8, FDIFF_1:def 6; :: thesis: for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !))

now :: thesis: for x being Real st x in ].a,b.[ holds
( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) )

let x be Real; :: thesis: ( x in ].a,b.[ implies ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ) )
assume A39: x in ].a,b.[ ; :: thesis: ( g is_differentiable_in x & diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) )
thus g is_differentiable_in x by A38, A39, FDIFF_1:9; :: thesis: diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !))
thus diff (g,x) = (g `| ].a,b.[) . x by A38, A39, FDIFF_1:def 7
.= ((g | ].a,b.[) `| ].a,b.[) . x by A38, FDIFF_2:16
.= ((y * f) `| ].a,b.[) . x by A37, A27, FDIFF_2:16
.= diff ((y * f),x) by A27, A39, FDIFF_1:def 7
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) by A21, A39 ; :: thesis: verum

end;

hence for x being Real st x in ].a,b.[ holds
diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((b - x) |^ 0)) / (0 !)) ; :: thesis: verum

end;

A40: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A41: S₁[k] ; :: thesis: S₁[k + 1]
assume A42: f is_differentiable_on k + 1,Z ; :: thesis: for a, b being Real st a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ holds
for 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))) . (k + 1)) ) holds
( 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.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )
let a, b be Real; :: thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous & f is_differentiable_on (k + 1) + 1,].a,b.[ implies for 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))) . (k + 1)) ) holds
( 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.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) )
assume that
A43: a < b and
A44: [.a,b.] c= Z and
A45: ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous and
A46: f is_differentiable_on (k + 1) + 1,].a,b.[ ; :: thesis: for 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))) . (k + 1)) ) holds
( 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.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )
(diff (f,Z)) . k is_differentiable_on Z by A42;
then ((diff (f,Z)) . k) | Z is continuous by FDIFF_1:25;
then A47: ((diff (f,Z)) . k) | [.a,b.] is continuous by A44, FCONT_1:16;
A48: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A49: ].a,b.[ c= Z by A44, XBOOLE_1:1;
consider gk being PartFunc of REAL,REAL such that
A50: dom gk = Z and
A51: for x being Real st x in Z holds
gk . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k) by Lm7;
A52: f is_differentiable_on k + 1,].a,b.[ by A46, Th23, NAT_1:11;
then A53: gk is_differentiable_on ].a,b.[ by A41, A42, A43, A44, A47, A50, A51, Th23, NAT_1:11;
A54: gk | [.a,b.] is continuous by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1:11;

now :: thesis: for gk1 being PartFunc of REAL,REAL st dom gk1 = Z & ( for x being Real st x in Z holds
gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) holds
( gk1 . b = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )

A55: (diff (f,Z)) . k is_differentiable_on Z by A42;
k <= ((k + 1) + 1) - 1 by NAT_1:11;
then A56: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A46;
A57: (diff (f,Z)) . (k + 1) = ((diff (f,Z)) . k) `| Z by Def5;
let gk1 be PartFunc of REAL,REAL; :: thesis: ( dom gk1 = Z & ( for x being Real st x in Z holds
gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ) implies ( gk1 . b = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) )
assume that
A58: dom gk1 = Z and
A59: for x being Real st x in Z holds
gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) ; :: thesis: ( gk1 . b = 0 & gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )
A60: b in [.a,b.] by A43, XXREAL_1:1;
then gk1 . b = (f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . (k + 1)) by A44, A59
.= (f . b) - (((Partial_Sums (Taylor (f,Z,b,b))) . k) + ((Taylor (f,Z,b,b)) . (k + 1))) by SERIES_1:def 1
.= ((f . b) - ((Partial_Sums (Taylor (f,Z,b,b))) . k)) - ((Taylor (f,Z,b,b)) . (k + 1))
.= (gk . b) - ((Taylor (f,Z,b,b)) . (k + 1)) by A44, A51, A60
.= 0 - ((Taylor (f,Z,b,b)) . (k + 1)) by A41, A42, A43, A44, A47, A52, A50, A51, Th23, NAT_1:11
.= 0 - (((((diff (f,Z)) . (k + 1)) . b) * ((b - b) |^ (k + 1))) / ((k + 1) !)) by Def7
.= 0 - (((((diff (f,Z)) . (k + 1)) . b) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6
.= 0 ;
hence gk1 . b = 0 ; :: thesis: ( gk1 | [.a,b.] is continuous & gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )
consider h being PartFunc of REAL,REAL such that
A61: dom h = [#] REAL and
A62: for x being Real holds h . x = (1 * ((b - x) |^ (k + 1))) / ((k + 1) !) and
A63: for x being Real holds
( h is_differentiable_in x & diff (h,x) = - ((1 * ((b - x) |^ k)) / (k !)) ) by Lm6;
A64: dom (((diff (f,Z)) . (k + 1)) (#) h) = (dom ((diff (f,Z)) . (k + 1))) /\ (dom h) by VALUED_1:def 4
.= Z /\ REAL by A61, A57, A55, FDIFF_1:def 7
.= Z by XBOOLE_1:28 ;
A65: dom (gk - (((diff (f,Z)) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff (f,Z)) . (k + 1)) (#) h)) by VALUED_1:12
.= Z by A50, A64 ;
thus gk1 | [.a,b.] is continuous :: thesis: ( gk1 is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) )

proof

set ghk = gk - (((diff (f,Z)) . (k + 1)) (#) h);
for x being Real st x in REAL holds
h is_differentiable_in x by A63;
then h is_differentiable_on REAL by A61, FDIFF_1:9;
then h | REAL is continuous by FDIFF_1:25;
then A66: h | [.a,b.] is continuous by FCONT_1:16;

now :: thesis: for x being Element of REAL st x in Z holds
gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x

let x be Element of REAL ; :: thesis: ( x in Z implies gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x )
assume A67: x in Z ; :: thesis: gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x
thus gk1 . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) by A59, A67
.= (f . b) - (((Partial_Sums (Taylor (f,Z,x,b))) . k) + ((Taylor (f,Z,x,b)) . (k + 1))) by SERIES_1:def 1
.= ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k)) - ((Taylor (f,Z,x,b)) . (k + 1))
.= (gk . x) - ((Taylor (f,Z,x,b)) . (k + 1)) by A51, A67
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by Def7
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A62
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A65, A67, VALUED_1:13 ; :: thesis: verum

end;

then A68: gk1 = gk - (((diff (f,Z)) . (k + 1)) (#) h) by A58, A65, PARTFUN1:5;
[.a,b.] c= dom ((diff (f,Z)) . (k + 1)) by A44, A57, A55, FDIFF_1:def 7;
then (((diff (f,Z)) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A45, A61, A66, FCONT_1:19;
hence gk1 | [.a,b.] is continuous by A44, A50, A54, A64, A68, FCONT_1:19; :: thesis: verum

end;

A69: (diff (f,].a,b.[)) . (k + 1) = ((diff (f,].a,b.[)) . k) `| ].a,b.[ by Def5;
set gfh = gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h);
A70: dom (((diff (f,].a,b.[)) . (k + 1)) (#) h) = (dom ((diff (f,].a,b.[)) . (k + 1))) /\ (dom h) by VALUED_1:def 4
.= ].a,b.[ /\ REAL by A61, A69, A56, FDIFF_1:def 7
.= ].a,b.[ by XBOOLE_1:28 ;
then A71: dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = Z /\ ].a,b.[ by A50, VALUED_1:12
.= ].a,b.[ by A44, A48, XBOOLE_1:1, XBOOLE_1:28 ;
A72: for x being Real st x in ].a,b.[ holds
(gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x

proof

let x be Real; :: thesis: ( x in ].a,b.[ implies (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x )
assume A73: x in ].a,b.[ ; :: thesis: (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x
thus (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . x = (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) (#) h) . x) by A71, A73, VALUED_1:13
.= (gk . x) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (h . x)) by VALUED_1:5
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) | ].a,b.[) . x) * (h . x)) by A42, A43, A44, A48, Th24, XBOOLE_1:1
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A73, FUNCT_1:49
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A49, A65, A73, VALUED_1:13 ; :: thesis: verum

end;

A74: now :: thesis: for xx being object st xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) holds
gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx

let xx be object ; :: thesis: ( xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) implies gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx )
assume A75: xx in dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) ; :: thesis: gk1 . xx = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx
reconsider x = xx as Real by A75;
thus gk1 . xx = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . (k + 1)) by A49, A59, A71, A75
.= (f . b) - (((Partial_Sums (Taylor (f,Z,x,b))) . k) + ((Taylor (f,Z,x,b)) . (k + 1))) by SERIES_1:def 1
.= ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . k)) - ((Taylor (f,Z,x,b)) . (k + 1))
.= (gk . x) - ((Taylor (f,Z,x,b)) . (k + 1)) by A49, A51, A71, A75
.= (gk . x) - (((((diff (f,Z)) . (k + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by Def7
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * ((1 * ((b - x) |^ (k + 1))) / ((k + 1) !))) by XCMPLX_1:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A62
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A49, A65, A71, A75, VALUED_1:13
.= (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx by A71, A72, A75 ; :: thesis: verum

end;

A76: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A46;
for x being Real st x in ].a,b.[ holds
h is_differentiable_in x by A63;
then A77: h is_differentiable_on ].a,b.[ by A61, FDIFF_1:9;
then A78: ((diff (f,].a,b.[)) . (k + 1)) (#) h is_differentiable_on ].a,b.[ by A70, A76, FDIFF_1:21;
then A79: gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ by A53, A71, FDIFF_1:19;
dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A44, A48, A58, A71, XBOOLE_1:1, XBOOLE_1:28;
then A80: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ by A74, FUNCT_1:46;
then (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ = gk1 | ].a,b.[ by FUNCT_1:51;
then for x being Real st x in ].a,b.[ holds
gk1 | ].a,b.[ is_differentiable_in x by A79, FDIFF_1:def 6;
hence A81: gk1 is_differentiable_on ].a,b.[ by A49, A58, FDIFF_1:def 6; :: thesis: for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !))

now :: thesis: for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !))

let x be Real; :: thesis: ( x in ].a,b.[ implies diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) )
assume A82: x in ].a,b.[ ; :: thesis: diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !))
thus diff (gk1,x) = (gk1 `| ].a,b.[) . x by A81, A82, FDIFF_1:def 7
.= ((gk1 | ].a,b.[) `| ].a,b.[) . x by A81, FDIFF_2:16
.= (((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[) `| ].a,b.[) . x by A80, FUNCT_1:51
.= ((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) `| ].a,b.[) . x by A79, FDIFF_2:16
.= (diff (gk,x)) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A53, A71, A78, A82, FDIFF_1:19
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A41, A42, A43, A44, A47, A52, A50, A51, A82, Th23, NAT_1:11
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((((diff (f,].a,b.[)) . (k + 1)) (#) h) `| ].a,b.[) . x) by A78, A82, FDIFF_1:def 7
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))) by A70, A76, A77, A82, FDIFF_1:21
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((h . x) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x)))
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - (((1 * ((b - x) |^ (k + 1))) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (diff (h,x))) by A62
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))) - ((((diff (f,].a,b.[)) . (k + 1)) . x) * (- ((1 * ((b - x) |^ k)) / (k !)))) by A63
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) + ((((diff (f,].a,b.[)) . (k + 1)) . x) * ((1 * ((b - x) |^ k)) / (k !)))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))
.= ((- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) + (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((b - x) |^ k)) / (k !))) - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x))) by XCMPLX_1:74
.= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (diff (((diff (f,].a,b.[)) . (k + 1)),x)))
.= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * ((((diff (f,].a,b.[)) . (k + 1)) `| ].a,b.[) . x)) by A76, A82, FDIFF_1:def 7
.= - ((((b - x) |^ (k + 1)) / ((k + 1) !)) * (((diff (f,].a,b.[)) . ((k + 1) + 1)) . x)) by Def5
.= - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) by XCMPLX_1:74 ; :: thesis: verum

end;

hence for x being Real st x in ].a,b.[ holds
diff (gk1,x) = - (((((diff (f,].a,b.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ; :: thesis: verum

end;

hence for 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))) . (k + 1)) ) holds
( 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.[)) . ((k + 1) + 1)) . x) * ((b - x) |^ (k + 1))) / ((k + 1) !)) ) ) ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A40);
hence for n being Nat st 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 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) ) holds
( 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 !)) ) ) ; :: thesis: verum