let n be Nat; :: thesis: for f being PartFunc of REAL,REAL
for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let f be PartFunc of REAL,REAL; :: thesis: for x0, r being Real st ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds
for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let x0, r be Real; :: thesis: ( ].(x0 - r),(x0 + r).[ c= dom f & 0 < r & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ implies for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) )
assume that
A1: ].(x0 - r),(x0 + r).[ c= dom f and
A2: 0 < r and
A3: f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ ; :: thesis: for x being Real st x in ].(x0 - r),(x0 + r).[ holds
ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
let x be Real; :: thesis: ( x in ].(x0 - r),(x0 + r).[ implies ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) )
assume A4: x in ].(x0 - r),(x0 + r).[ ; :: thesis: ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )

now :: thesis: ( ( x < x0 & ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) or ( x = x0 & ex s being set st
( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x ) ) or ( x > x0 & ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) )

per cases ( x < x0 or x = x0 or x > x0 ) by XXREAL_0:1;

case A5: x < x0 ; :: thesis: ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )

|.(x0 - x0).| = 0 by ABSVALUE:2;
then x0 in ].(x0 - r),(x0 + r).[ by A2, RCOMP_1:1;
then A6: [.x,x0.] c= ].(x0 - r),(x0 + r).[ by A4, XXREAL_2:def 12;
(diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3;
then ((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is continuous by FDIFF_1:25;
then A7: ((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x,x0.] is continuous by A6, FCONT_1:16;
A8: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A3, Th23, NAT_1:11;
set t = x0 - x;
A9: x0 - x > 0 by A5, XREAL_1:50;
A10: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
then f is_differentiable_on n + 1,].x,x0.[ by A3, A6, Th31, XBOOLE_1:1;
then consider c being Real such that
A11: c in ].x,x0.[ and
A12: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x,x0.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A1, A5, A6, A8, A7, Th29;
take s = (x0 - c) / (x0 - x); :: thesis: ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
A13: x0 + (s * (x - x0)) = x0 - (((x0 - c) / (x0 - x)) * (x0 - x))
.= x0 - (x0 - c) by A9, XCMPLX_1:87
.= c ;
c in { p where p is Real : ( x0 - (x0 - x) < p & p < x0 ) } by A11, RCOMP_1:def 2;
then A14: ex g being Real st
( g = c & x0 - (x0 - x) < g & g < x0 ) ;
then 0 < x0 - c by XREAL_1:50;
then 0 / (x0 - x) < (x0 - c) / (x0 - x) by A9, XREAL_1:74;
hence 0 < s ; :: thesis: ( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
(x0 - (x0 - x)) + (x0 - x) < c + (x0 - x) by A14, XREAL_1:8;
then x0 - c < x0 - x by XREAL_1:19;
then (x0 - c) / (x0 - x) < (x0 - x) / (x0 - x) by A9, XREAL_1:74;
hence s < 1 by A9, XCMPLX_1:60; :: thesis: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
((diff (f,].x,x0.[)) . (n + 1)) . c = (((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x,x0.[) . c by A3, A6, A10, Th30, XBOOLE_1:1
.= ((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c by A11, FUNCT_1:49 ;
hence f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A12, A13; :: thesis: verum

end;

case A15: x = x0 ; :: thesis: ex s being set st
( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x )

set s = 1 / 2;
take s = 1 / 2; :: thesis: ( 0 < s & s < 1 & ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x )
thus ( 0 < s & s < 1 ) ; :: thesis: ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = f . x
set c = x0 + (s * (x - x0));
thus ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) = (f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x) |^ (n + 1))) / ((n + 1) !)) by A4, A15, Th32
.= (f . x) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6
.= f . x ; :: thesis: verum

end;

case A16: x > x0 ; :: thesis: ex s being set st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )

set t = x - x0;
A17: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A3, Th23, NAT_1:11;
|.(x0 - x0).| = 0 by ABSVALUE:2;
then x0 in ].(x0 - r),(x0 + r).[ by A2, RCOMP_1:1;
then A18: [.x0,x.] c= ].(x0 - r),(x0 + r).[ by A4, XXREAL_2:def 12;
(diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3;
then ((diff (f,].(x0 - r),(x0 + r).[)) . n) | ].(x0 - r),(x0 + r).[ is continuous by FDIFF_1:25;
then A19: ((diff (f,].(x0 - r),(x0 + r).[)) . n) | [.x0,x.] is continuous by A18, FCONT_1:16;
A20: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then f is_differentiable_on n + 1,].x0,x.[ by A3, A18, Th31, XBOOLE_1:1;
then consider c being Real such that
A21: c in ].x0,x.[ and
A22: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].x0,x.[)) . (n + 1)) . c) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A1, A16, A18, A17, A19, Th27;
take s = (c - x0) / (x - x0); :: thesis: ( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
A23: x - x0 > 0 by A16, XREAL_1:50;
then A24: x0 + (s * (x - x0)) = x0 + (c - x0) by XCMPLX_1:87
.= c ;
c in { p where p is Real : ( x0 < p & p < x0 + (x - x0) ) } by A21, RCOMP_1:def 2;
then A25: ex g being Real st
( g = c & x0 < g & g < x0 + (x - x0) ) ;
then 0 < c - x0 by XREAL_1:50;
then 0 / (x - x0) < (c - x0) / (x - x0) by A23, XREAL_1:74;
hence 0 < s ; :: thesis: ( s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) )
c - x0 < x - x0 by A25, XREAL_1:19;
then (c - x0) / (x - x0) < (x - x0) / (x - x0) by A23, XREAL_1:74;
hence s < 1 by A23, XCMPLX_1:60; :: thesis: f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !))
((diff (f,].x0,x.[)) . (n + 1)) . c = (((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) | ].x0,x.[) . c by A3, A18, A20, Th30, XBOOLE_1:1
.= ((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . c by A21, FUNCT_1:49 ;
hence f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) by A22, A24; :: thesis: verum

end;

end;

end;

hence ex s being Real st
( 0 < s & s < 1 & f . x = ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n) + (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ; :: thesis: verum