let n be Element of NAT ; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
let x0, r be Real; :: thesis:
assume that
A0: ].(x0 - r),(x0 + r).[ c= dom f and
A1: 0 < r and
A2: f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ ; :: thesis:
let x be Real; :: thesis:
assume A3: x in ].(x0 - r),(x0 + r).[ ; :: thesis:

now

per cases by XXREAL_0:1;

case A4: x < x0 ; :: thesis:

abs (x0 - x0) = 0 by ABSVALUE:7;
then x0 in ].(x0 - r),(x0 + r).[ by A1, RCOMP_1:8;
then A5: [.x,x0.] c= ].(x0 - r),(x0 + r).[ by A3, XXREAL_2:def 12;
A6: ].x,x0.[ c= [.x,x0.] by XXREAL_1:25;
A7: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A2, Th23, NAT_1:11;
n <= (n + 1) - 1 ;
then (diff f,].(x0 - r),(x0 + r).[) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A2, Def6;
then ( ].(x0 - r),(x0 + r).[ c= dom ((diff f,].(x0 - r),(x0 + r).[) . n) & ((diff f,].(x0 - r),(x0 + r).[) . n) | ].(x0 - r),(x0 + r).[ is continuous ) by FDIFF_1:33, FDIFF_1:def 7;
then A8: ((diff f,].(x0 - r),(x0 + r).[) . n) | [.x,x0.] is continuous by A5, FCONT_1:17;
f is_differentiable_on n + 1,].x,x0.[ by A2, A5, A6, Th31, XBOOLE_1:1;
then consider c being Real such that
A9: c in ].x,x0.[ and
A10: 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 A4, A5, A7, A8, Th29, A0;
A11: ((diff f,].x,x0.[) . (n + 1)) . c = (((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x,x0.[) . c by A2, A5, A6, Th30, XBOOLE_1:1
.= ((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . c by A9, FUNCT_1:72 ;
set t = x0 - x;
A12: x0 - x > 0 by A4, XREAL_1:52;
take s = (x0 - c) / (x0 - x); :: thesis:
c in { p where p is Real : ( x0 - (x0 - x) < p & p < x0 ) } by A9, RCOMP_1:def 2;
then A13: ex g being Real st
( g = c & x0 - (x0 - x) < g & g < x0 ) ;
then 0 < x0 - c by XREAL_1:52;
then 0 / (x0 - x) < (x0 - c) / (x0 - x) by A12, XREAL_1:76;
hence 0 < s ; :: thesis:
(x0 - (x0 - x)) + (x0 - x) < c + (x0 - x) by A13, XREAL_1:10;
then x0 - c < x0 - x by XREAL_1:21;
then (x0 - c) / (x0 - x) < (x0 - x) / (x0 - x) by A12, XREAL_1:76;
hence s < 1 by A12, XCMPLX_1:60; :: thesis:
x0 + (s * (x - x0)) = x0 - (((x0 - c) / (x0 - x)) * (x0 - x))
.= x0 - (x0 - c) by A12, XCMPLX_1:88
.= c ;
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 A10, A11; :: thesis:

end;

case A14: x = x0 ; :: thesis:

set s = 1 / 2;
take s = 1 / 2; :: thesis:
thus ( 0 < s & s < 1 ) ; :: thesis:
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 A3, A14, Th32
.= (f . x) + (((((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . (x0 + (s * (x - x0)))) * ((0 |^ n) * 0 )) / ((n + 1) ! )) by NEWTON:11
.= f . x ; :: thesis:

end;

case A15: x > x0 ; :: thesis:

abs (x0 - x0) = 0 by ABSVALUE:7;
then x0 in ].(x0 - r),(x0 + r).[ by A1, RCOMP_1:8;
then A16: [.x0,x.] c= ].(x0 - r),(x0 + r).[ by A3, XXREAL_2:def 12;
A17: ].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
A18: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A2, Th23, NAT_1:11;
n <= (n + 1) - 1 ;
then (diff f,].(x0 - r),(x0 + r).[) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A2, Def6;
then ( ].(x0 - r),(x0 + r).[ c= dom ((diff f,].(x0 - r),(x0 + r).[) . n) & ((diff f,].(x0 - r),(x0 + r).[) . n) | ].(x0 - r),(x0 + r).[ is continuous ) by FDIFF_1:33, FDIFF_1:def 7;
then A19: ((diff f,].(x0 - r),(x0 + r).[) . n) | [.x0,x.] is continuous by A16, FCONT_1:17;
f is_differentiable_on n + 1,].x0,x.[ by A2, A16, A17, Th31, XBOOLE_1:1;
then consider c being Real such that
A20: c in ].x0,x.[ and
A21: 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 A15, A16, A18, A19, Th27, A0;
A22: ((diff f,].x0,x.[) . (n + 1)) . c = (((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) | ].x0,x.[) . c by A2, A16, A17, Th30, XBOOLE_1:1
.= ((diff f,].(x0 - r),(x0 + r).[) . (n + 1)) . c by A20, FUNCT_1:72 ;
set t = x - x0;
A23: x - x0 > 0 by A15, XREAL_1:52;
take s = (c - x0) / (x - x0); :: thesis:
c in { p where p is Real : ( x0 < p & p < x0 + (x - x0) ) } by A20, RCOMP_1:def 2;
then A24: ex g being Real st
( g = c & x0 < g & g < x0 + (x - x0) ) ;
then 0 < c - x0 by XREAL_1:52;
then 0 / (x - x0) < (c - x0) / (x - x0) by A23, XREAL_1:76;
hence 0 < s ; :: thesis:
c - x0 < x - x0 by A24, XREAL_1:21;
then (c - x0) / (x - x0) < (x - x0) / (x - x0) by A23, XREAL_1:76;
hence s < 1 by A23, XCMPLX_1:60; :: thesis:
x0 + (s * (x - x0)) = x0 + (c - x0) by A23, XCMPLX_1:88
.= c ;
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 A21, A22; :: thesis:

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: