let f be PartFunc of REAL , REAL ; :: thesis: for Z being Subset of REAL st Z c= dom f holds
for n being Element of 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . n) ) holds
( g . a = 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) * ((a - x) |^ n)) / (n ! )) ) )
let Z be Subset of REAL ; :: thesis: ( Z c= dom f implies for n being Element of 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . n) ) holds
( g . a = 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) * ((a - x) |^ n)) / (n ! )) ) ) )
assume A0: Z c= dom f ; :: thesis: for n being Element of 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . n) ) holds
( g . a = 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) * ((a - x) |^ n)) / (n ! )) ) )
defpred S₁[ Element of 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . $1) ) holds
( g . a = 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) * ((a - x) |^ $1)) / ($1 ! )) ) ) );
A1: 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) ) holds
( g . a = 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) * ((a - 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) ) holds
( g . a = 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) * ((a - x) |^ 0 )) / (0 ! )) ) ) )
assume that
A2: a < b and
A3: [.a,b.] c= Z and
A4: ((diff f,Z) . 0 ) | [.a,b.] is continuous and
A5: 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) ) holds
( g . a = 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) * ((a - x) |^ 0 )) / (0 ! )) ) )
let g be PartFunc of REAL , REAL ; :: thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) ) implies ( g . a = 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) * ((a - x) |^ 0 )) / (0 ! )) ) ) )
assume that
A6: dom g = Z and
A7: for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) ; :: thesis: ( g . a = 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) * ((a - x) |^ 0 )) / (0 ! )) ) )
A8: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A9: ].a,b.[ c= Z by A3, XBOOLE_1:1;
A10: a in [.a,b.] by A2, XXREAL_1:1;
hence g . a = (f . a) - ((Partial_Sums (Taylor f,Z,a,a)) . 0 ) by A3, A7
.= (f . a) - ((Taylor f,Z,a,a) . 0 ) by SERIES_1:def 1
.= (f . a) - (((((diff f,Z) . 0 ) . a) * ((a - a) |^ 0 )) / (0 ! )) by Def7
.= (f . a) - ((((f | Z) . a) * ((a - a) |^ 0 )) / (0 ! )) by Def5
.= (f . a) - (((f . a) * ((a - a) |^ 0 )) / (0 ! )) by A3, A10, FUNCT_1:72
.= (f . a) - ((f . a) * 1) by NEWTON:9, NEWTON:18
.= 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) * ((a - x) |^ 0 )) / (0 ! )) ) )
consider y being PartFunc of REAL , REAL such that
A11: dom y = [#] REAL and
A12: for x being Real holds y . x = (f . a) - x and
A13: for x being Real holds
( y is_differentiable_in x & diff y,x = - 1 ) by Lm5;
(f | Z) | [.a,b.] is continuous by A4, Def5;
then ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:16;
then (f | [.a,b.]) | [.a,b.] is continuous by A3, FUNCT_1:82;
then A14: f | [.a,b.] is continuous by FCONT_1:16;
A15: [.a,b.] c= dom f by A3, A0, XBOOLE_1:1;
rng f c= REAL ;
then A16: dom (y * f) = dom f by A11, RELAT_1:46;
A17: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by FUNCT_1:68
.= [.a,b.] by A15, A16, XBOOLE_1:28
.= Z /\ [.a,b.] by A3, XBOOLE_1:28
.= dom (g | [.a,b.]) by A6, FUNCT_1:68 ;
A18: g | [.a,b.] = (y * f) | [.a,b.]

proof

now

let xx be set ; :: thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx )
assume A19: xx in dom (g | [.a,b.]) ; :: thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx
dom (g | [.a,b.]) = (dom g) /\ [.a,b.] by FUNCT_1:68;
then A20: dom (g | [.a,b.]) c= [.a,b.] by XBOOLE_1:17;
reconsider x = xx as Real by A19;
A21: x in [.a,b.] by A19, A20;
thus (g | [.a,b.]) . xx = g . x by A19, FUNCT_1:70
.= (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) by A3, A7, A21
.= (f . a) - ((Taylor f,Z,x,a) . 0 ) by SERIES_1:def 1
.= (f . a) - (((((diff f,Z) . 0 ) . x) * ((a - x) |^ 0 )) / (0 ! )) by Def7
.= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0 )) / (0 ! )) by Def5
.= (f . a) - (((f . x) * ((a - x) |^ 0 )) / (0 ! )) by A3, A21, FUNCT_1:72
.= (f . a) - ((f . x) * 1) by NEWTON:9, NEWTON:18
.= y . (f . x) by A12
.= (y * f) . x by A15, A21, FUNCT_1:23
.= ((y * f) | [.a,b.]) . xx by A17, A19, FUNCT_1:70 ; :: thesis: verum

end;

hence g | [.a,b.] = (y * f) | [.a,b.] by A17, FUNCT_1:9; :: thesis: verum

end;

for x being Real st x in REAL holds
y is_differentiable_in x by A13;
then y is_differentiable_on REAL by A11, FDIFF_1:16;
then y | REAL is continuous by FDIFF_1:33;
then y | (f .: [.a,b.]) is continuous by FCONT_1:17;
then (y * f) | [.a,b.] is continuous by A14, FCONT_1:26;
then ((y * f) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:16;
hence g | [.a,b.] is continuous by A18, FCONT_1:16; :: 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) * ((a - x) |^ 0 )) / (0 ! )) ) )
0 <= (0 + 1) - 1 ;
then (diff f,].a,b.[) . 0 is_differentiable_on ].a,b.[ by A5, Def6;
then f | ].a,b.[ is_differentiable_on ].a,b.[ by Def5;
then A22: ( ].a,b.[ c= dom f & ( for x being Real st x in ].a,b.[ holds
f | ].a,b.[ is_differentiable_in x ) ) by A8, A15, FDIFF_1:16, XBOOLE_1:1;
then A23: f is_differentiable_on ].a,b.[ by FDIFF_1:def 7;
A24: 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) * ((a - x) |^ 0 )) / (0 ! )) )

proof

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) * ((a - x) |^ 0 )) / (0 ! )) ) )
assume A25: x in ].a,b.[ ; :: thesis: ( y * f is_differentiable_in x & diff (y * f),x = - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! )) )
A26: ((a - x) |^ 0 ) / (0 ! ) = 1 by NEWTON:9, NEWTON:18;
A27: y is_differentiable_in f . x by A13;
A28: (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 A23, FDIFF_2:16 ;
A29: f is_differentiable_in x by A23, A25, FDIFF_1:16;
hence y * f is_differentiable_in x by A27, FDIFF_2:13; :: thesis: diff (y * f),x = - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! ))
thus diff (y * f),x = (diff y,(f . x)) * (diff f,x) by A27, A29, FDIFF_2:13
.= (diff y,(f . x)) * ((f `| ].a,b.[) . x) by A23, A25, FDIFF_1:def 8
.= (- 1) * (((diff f,].a,b.[) . (0 + 1)) . x) by A13, A28
.= - ((((diff f,].a,b.[) . (0 + 1)) . x) * (((a - x) |^ 0 ) / (0 ! ))) by A26
.= - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! )) by XCMPLX_1:75 ; :: thesis: verum

end;

rng f c= dom y by A11;
then A30: dom (y * f) = dom f by RELAT_1:46;
A31: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by FUNCT_1:68
.= ].a,b.[ by A22, A30, XBOOLE_1:28
.= Z /\ ].a,b.[ by A3, A8, XBOOLE_1:1, XBOOLE_1:28
.= dom (g | ].a,b.[) by A6, FUNCT_1:68 ;
A32: g | ].a,b.[ = (y * f) | ].a,b.[

proof

now

let xx be set ; :: thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx )
assume A33: xx in dom (g | ].a,b.[) ; :: thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx
dom (g | ].a,b.[) = (dom g) /\ ].a,b.[ by FUNCT_1:68;
then A34: dom (g | ].a,b.[) c= ].a,b.[ by XBOOLE_1:17;
reconsider x = xx as Real by A33;
A35: ((a - x) |^ 0 ) / (0 ! ) = 1 by NEWTON:9, NEWTON:18;
A36: x in ].a,b.[ by A33, A34;
thus (g | ].a,b.[) . xx = g . x by A33, FUNCT_1:70
.= (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . 0 ) by A7, A9, A36
.= (f . a) - ((Taylor f,Z,x,a) . 0 ) by SERIES_1:def 1
.= (f . a) - (((((diff f,Z) . 0 ) . x) * ((a - x) |^ 0 )) / (0 ! )) by Def7
.= (f . a) - ((((f | Z) . x) * ((a - x) |^ 0 )) / (0 ! )) by Def5
.= (f . a) - (((f . x) * ((a - x) |^ 0 )) / (0 ! )) by A9, A36, FUNCT_1:72
.= (f . a) - ((f . x) * (((a - x) |^ 0 ) / (0 ! ))) by XCMPLX_1:75
.= y . (f . x) by A12, A35
.= (y * f) . x by A22, A36, FUNCT_1:23
.= ((y * f) | ].a,b.[) . xx by A31, A33, FUNCT_1:70 ; :: thesis: verum

end;

hence g | ].a,b.[ = (y * f) | ].a,b.[ by A31, FUNCT_1:9; :: thesis: verum

end;

for x being Real st x in ].a,b.[ holds
y * f is_differentiable_in x by A24;
then A37: y * f is_differentiable_on ].a,b.[ by A22, A30, FDIFF_1:16;
then ( g | ].a,b.[ is_differentiable_on ].a,b.[ & (y * f) `| ].a,b.[ = (g | ].a,b.[) `| ].a,b.[ ) by A32, FDIFF_2:16;
then for x being Real st x in ].a,b.[ holds
g | ].a,b.[ is_differentiable_in x by FDIFF_1:16;
hence A38: g is_differentiable_on ].a,b.[ by A6, A9, FDIFF_1:def 7; :: thesis: for x being Real st x in ].a,b.[ holds
diff g,x = - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! ))

now

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) * ((a - 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) * ((a - x) |^ 0 )) / (0 ! )) )
thus g is_differentiable_in x by A38, A39, FDIFF_1:16; :: thesis: diff g,x = - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! ))
thus diff g,x = (g `| ].a,b.[) . x by A38, A39, FDIFF_1:def 8
.= ((g | ].a,b.[) `| ].a,b.[) . x by A38, FDIFF_2:16
.= ((y * f) `| ].a,b.[) . x by A32, A37, FDIFF_2:16
.= diff (y * f),x by A37, A39, FDIFF_1:def 8
.= - (((((diff f,].a,b.[) . (0 + 1)) . x) * ((a - x) |^ 0 )) / (0 ! )) by A24, 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) * ((a - x) |^ 0 )) / (0 ! )) ; :: thesis: verum

end;

A40: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

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

now

let gk1 be PartFunc of REAL , REAL ; :: thesis: ( dom gk1 = Z & ( for x being Real st x in Z holds
gk1 . x = (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . (k + 1)) ) implies ( gk1 . a = 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) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) ) ) )
assume that
A55: dom gk1 = Z and
A56: for x being Real st x in Z holds
gk1 . x = (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . (k + 1)) ; :: thesis: ( gk1 . a = 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) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) ) )
consider h being PartFunc of REAL , REAL such that
A57: dom h = [#] REAL and
A58: for x being Real holds h . x = (1 * ((a - x) |^ (k + 1))) / ((k + 1) ! ) and
A59: for x being Real holds
( h is_differentiable_in x & diff h,x = - ((1 * ((a - x) |^ k)) / (k ! )) ) by Lm6;
thus gk1 . a = 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) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) ) )

proof

A60: a in [.a,b.] by A43, XXREAL_1:1;
hence gk1 . a = (f . a) - ((Partial_Sums (Taylor f,Z,a,a)) . (k + 1)) by A44, A56
.= (f . a) - (((Partial_Sums (Taylor f,Z,a,a)) . k) + ((Taylor f,Z,a,a) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor f,Z,a,a)) . k)) - ((Taylor f,Z,a,a) . (k + 1))
.= (gk . a) - ((Taylor f,Z,a,a) . (k + 1)) by A44, A53, A60
.= 0 - ((Taylor f,Z,a,a) . (k + 1)) by A41, A42, A43, A44, A49, A50, A51, A52, A53, Th23
.= 0 - (((((diff f,Z) . (k + 1)) . a) * ((a - a) |^ (k + 1))) / ((k + 1) ! )) by Def7
.= 0 - (((((diff f,Z) . (k + 1)) . a) * ((0 |^ k) * 0 )) / ((k + 1) ! )) by NEWTON:11
.= 0 ;
:: thesis: verum

end;

A61: (diff f,Z) . (k + 1) = ((diff f,Z) . k) `| Z by Def5;
k <= (k + 1) - 1 ;
then A62: (diff f,Z) . k is_differentiable_on Z by A42, Def6;
A63: dom (((diff f,Z) . (k + 1)) (#) h) = (dom ((diff f,Z) . (k + 1))) /\ (dom h) by VALUED_1:def 4
.= Z /\ REAL by A57, A61, A62, FDIFF_1:def 8
.= Z by XBOOLE_1:28 ;
A64: dom (gk - (((diff f,Z) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff f,Z) . (k + 1)) (#) h)) by VALUED_1:12
.= Z by A52, A63 ;
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) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) ) )

proof

set ghk = gk - (((diff f,Z) . (k + 1)) (#) h);

now

let x be Real; :: thesis: ( x in Z implies gk1 . x = (gk - (((diff f,Z) . (k + 1)) (#) h)) . x )
assume A65: x in Z ; :: thesis: gk1 . x = (gk - (((diff f,Z) . (k + 1)) (#) h)) . x
thus gk1 . x = (f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . (k + 1)) by A56, A65
.= (f . a) - (((Partial_Sums (Taylor f,Z,x,a)) . k) + ((Taylor f,Z,x,a) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . k)) - ((Taylor f,Z,x,a) . (k + 1))
.= (gk . x) - ((Taylor f,Z,x,a) . (k + 1)) by A53, A65
.= (gk . x) - (((((diff f,Z) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) by Def7
.= (gk . x) - ((((diff f,Z) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! ))) by XCMPLX_1:75
.= (gk . x) - ((((diff f,Z) . (k + 1)) . x) * (h . x)) by A58
.= (gk . x) - ((((diff f,Z) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff f,Z) . (k + 1)) (#) h)) . x by A64, A65, VALUED_1:13 ; :: thesis: verum

end;

then A66: gk1 = gk - (((diff f,Z) . (k + 1)) (#) h) by A55, A64, PARTFUN1:34;
dom ((diff f,Z) . (k + 1)) = Z by A61, A62, FDIFF_1:def 8;
then I: [.a,b.] c= dom ((diff f,Z) . (k + 1)) by A44;
J: [.a,b.] c= dom h by A57;
K: [.a,b.] c= dom gk by A52, A44;
L: [.a,b.] c= dom (((diff f,Z) . (k + 1)) (#) h) by A63, A44;
for x being Real st x in REAL holds
h is_differentiable_in x by A59;
then h is_differentiable_on REAL by A57, FDIFF_1:16;
then h | REAL is continuous by FDIFF_1:33;
then h | [.a,b.] is continuous by FCONT_1:17;
then (((diff f,Z) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A45, I, J, FCONT_1:20;
hence gk1 | [.a,b.] is continuous by A54, A66, K, L, FCONT_1:20; :: thesis: verum

end;

A67: (diff f,].a,b.[) . (k + 1) = ((diff f,].a,b.[) . k) `| ].a,b.[ by Def5;
k <= ((k + 1) + 1) - 1 by NAT_1:11;
then A68: (diff f,].a,b.[) . k is_differentiable_on ].a,b.[ by A46, Def6;
A69: 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 A57, A67, A68, FDIFF_1:def 8
.= ].a,b.[ by XBOOLE_1:28 ;
A70: dom (gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) = Z /\ (dom (((diff f,].a,b.[) . (k + 1)) (#) h)) by A52, VALUED_1:12
.= ].a,b.[ by A44, A47, A69, XBOOLE_1:1, XBOOLE_1:28 ;
k + 1 <= ((k + 1) + 1) - 1 ;
then A71: (diff f,].a,b.[) . (k + 1) is_differentiable_on ].a,b.[ by A46, Def6;
set gfh = gk - (((diff f,].a,b.[) . (k + 1)) (#) h);
A72: dom (gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A44, A47, A55, A70, XBOOLE_1:1, XBOOLE_1:28;
A73: 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 A74: 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 A70, A74, 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, A47, Th24, XBOOLE_1:1
.= (gk . x) - ((((diff f,Z) . (k + 1)) . x) * (h . x)) by A74, FUNCT_1:72
.= (gk . x) - ((((diff f,Z) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff f,Z) . (k + 1)) (#) h)) . x by A48, A64, A74, VALUED_1:13 ; :: thesis: verum

end;

now

let xx be set ; :: 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . (k + 1)) by A48, A56, A70, A75
.= (f . a) - (((Partial_Sums (Taylor f,Z,x,a)) . k) + ((Taylor f,Z,x,a) . (k + 1))) by SERIES_1:def 1
.= ((f . a) - ((Partial_Sums (Taylor f,Z,x,a)) . k)) - ((Taylor f,Z,x,a) . (k + 1))
.= (gk . x) - ((Taylor f,Z,x,a) . (k + 1)) by A48, A53, A70, A75
.= (gk . x) - (((((diff f,Z) . (k + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) by Def7
.= (gk . x) - ((((diff f,Z) . (k + 1)) . x) * ((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! ))) by XCMPLX_1:75
.= (gk . x) - ((((diff f,Z) . (k + 1)) . x) * (h . x)) by A58
.= (gk . x) - ((((diff f,Z) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff f,Z) . (k + 1)) (#) h)) . x by A48, A64, A70, A75, VALUED_1:13
.= (gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) . xx by A70, A73, A75 ; :: thesis: verum

end;

then A76: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) | ].a,b.[ by A72, FUNCT_1:68;
then A77: (gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) | ].a,b.[ = gk1 | ].a,b.[ by FUNCT_1:82;
for x being Real st x in ].a,b.[ holds
h is_differentiable_in x by A59;
then A78: h is_differentiable_on ].a,b.[ by A57, FDIFF_1:16;
then A79: ( ((diff f,].a,b.[) . (k + 1)) (#) h is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
((((diff f,].a,b.[) . (k + 1)) (#) h) `| ].a,b.[) . x = ((h . x) * (diff ((diff f,].a,b.[) . (k + 1)),x)) + ((((diff f,].a,b.[) . (k + 1)) . x) * (diff h,x)) ) ) by A69, A71, FDIFF_1:29;
then A80: ( gk - (((diff f,].a,b.[) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ & ( for x being Real st x in ].a,b.[ holds
((gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) `| ].a,b.[) . x = (diff gk,x) - (diff (((diff f,].a,b.[) . (k + 1)) (#) h),x) ) ) by A54, A70, FDIFF_1:27;
then for x being Real st x in ].a,b.[ holds
gk1 | ].a,b.[ is_differentiable_in x by A77, FDIFF_1:def 7;
hence A81: gk1 is_differentiable_on ].a,b.[ by A48, A55, FDIFF_1:def 7; :: thesis: for x being Real st x in ].a,b.[ holds
diff gk1,x = - (((((diff f,].a,b.[) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! ))

now

let x be Real; :: thesis: ( x in ].a,b.[ implies diff gk1,x = - (((((diff f,].a,b.[) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) )
assume A82: x in ].a,b.[ ; :: thesis: diff gk1,x = - (((((diff f,].a,b.[) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! ))
thus diff gk1,x = (gk1 `| ].a,b.[) . x by A81, A82, FDIFF_1:def 8
.= ((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 A76, FUNCT_1:82
.= ((gk - (((diff f,].a,b.[) . (k + 1)) (#) h)) `| ].a,b.[) . x by A80, FDIFF_2:16
.= (diff gk,x) - (diff (((diff f,].a,b.[) . (k + 1)) (#) h),x) by A54, A70, A79, A82, FDIFF_1:27
.= (- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - (diff (((diff f,].a,b.[) . (k + 1)) (#) h),x) by A41, A42, A43, A44, A49, A50, A51, A52, A53, A82, Th23
.= (- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - (((((diff f,].a,b.[) . (k + 1)) (#) h) `| ].a,b.[) . x) by A79, A82, FDIFF_1:def 8
.= (- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - (((h . x) * (diff ((diff f,].a,b.[) . (k + 1)),x)) + ((((diff f,].a,b.[) . (k + 1)) . x) * (diff h,x))) by A69, A71, A78, A82, FDIFF_1:29
.= ((- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - 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) * ((a - x) |^ k)) / (k ! ))) - (((1 * ((a - x) |^ (k + 1))) / ((k + 1) ! )) * (diff ((diff f,].a,b.[) . (k + 1)),x))) - ((((diff f,].a,b.[) . (k + 1)) . x) * (diff h,x)) by A58
.= ((- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (diff ((diff f,].a,b.[) . (k + 1)),x))) - ((((diff f,].a,b.[) . (k + 1)) . x) * (- ((1 * ((a - x) |^ k)) / (k ! )))) by A59
.= ((- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) + ((((diff f,].a,b.[) . (k + 1)) . x) * ((1 * ((a - x) |^ k)) / (k ! )))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (diff ((diff f,].a,b.[) . (k + 1)),x))
.= ((- (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) + (((((diff f,].a,b.[) . (k + 1)) . x) * ((a - x) |^ k)) / (k ! ))) - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (diff ((diff f,].a,b.[) . (k + 1)),x)) by XCMPLX_1:75
.= - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (diff ((diff f,].a,b.[) . (k + 1)),x))
.= - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * ((((diff f,].a,b.[) . (k + 1)) `| ].a,b.[) . x)) by A71, A82, FDIFF_1:def 8
.= - ((((a - x) |^ (k + 1)) / ((k + 1) ! )) * (((diff f,].a,b.[) . ((k + 1) + 1)) . x)) by Def5
.= - (((((diff f,].a,b.[) . ((k + 1) + 1)) . x) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) by XCMPLX_1:75 ; :: 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) * ((a - 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . (k + 1)) ) holds
( g . a = 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) * ((a - x) |^ (k + 1))) / ((k + 1) ! )) ) ) ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A40);
hence for n being Element of 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 . a) - ((Partial_Sums (Taylor f,Z,x,a)) . n) ) holds
( g . a = 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) * ((a - x) |^ n)) / (n ! )) ) ) ; :: thesis: verum