:: TAYLOR_1 semantic presentation

begin


definition
let q be Integer;
func #Z q ->  Function of REAL,REAL means :Def1: :: TAYLOR_1:def 1
 for x being real number holds it . x = x #Z q;
existence
 ex b1 being Function of REAL,REAL st
for x being real number holds b1 . x = x #Z q
proof
deffunc H1( Real) ->  Element of REAL = $1 #Z q;
consider f being Function of REAL,REAL such that
A1: for d being Element of REAL holds f . d = H1(d) from FUNCT_2:sch_4();
take  f ; ::_thesis: for x being real number holds f . x = x #Z q
let d be real number ; ::_thesis: f . d = d #Z q
 d is Real by XREAL_0:def_1;
hence  f . d = d #Z q by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of REAL,REAL st ( for x being real number holds b1 . x = x #Z q ) & ( for x being real number holds b2 . x = x #Z q ) holds
b1 = b2
proof
let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for x being real number holds f1 . x = x #Z q ) & ( for x being real number holds f2 . x = x #Z q ) implies f1 = f2 )
assume that
A2: for d being real number holds f1 . d = d #Z q and
A3: for d being real number holds f2 . d = d #Z q ; ::_thesis: f1 = f2
 for d being Element of REAL holds f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: f1 . d = f2 . d
thus f1 . d = d #Z q by A2
.= f2 . d by A3 ; ::_thesis: verum
end;
hence  f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines #Z TAYLOR_1:def_1_:_
 for q being Integer
for b2 being Function of REAL,REAL holds
( b2 = #Z q iff for x being real number holds b2 . x = x #Z q );

theorem Th1: :: TAYLOR_1:1
for x being real number
for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m)
proof
let x be real number ; ::_thesis: for m, n being Nat holds x #Z (n + m) = (x #Z n) * (x #Z m)
let m, n be Nat; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
percases ( x <> 0 or x = 0 ) ;
suppose x <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
hence  x #Z (n + m) = (x #Z n) * (x #Z m) by PREPOWER:44; ::_thesis: verum
end;
supposeA1: x = 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
thus  x #Z (n + m) = (x #Z n) * (x #Z m) ::_thesis: verum
proof
A2: 0 #Z (n + m) = 0 |^ (abs (n + m)) by PREPOWER:def_3
.= 0 |^ (n + m) by ABSVALUE:def_1
.= (0 |^ n) * (0 |^ m) by NEWTON:8 ;
percases ( ( n = 0 & m = 0 ) or n <> 0 or m <> 0 ) ;
supposeA3: ( n = 0 & m = 0 ) ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
x #Z (0 + 0) = 1 * (x #Z 0)
.= (x #Z 0) * (x #Z 0) by PREPOWER:34 ;
hence  x #Z (n + m) = (x #Z n) * (x #Z m) by A3; ::_thesis: verum
end;
suppose n <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
then A4: 0 + 1 <= n by NAT_1:13;
A5: (0 #Z n) * (0 #Z m) = (0 |^ (abs n)) * (0 #Z m) by PREPOWER:def_3
.= (0 |^ n) * (0 #Z m) by ABSVALUE:def_1
.= 0 * (0 #Z m) by A4, NEWTON:11 ;
 0 #Z (n + m) = 0 * (0 |^ m) by A2, A4, NEWTON:11;
hence  x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A5; ::_thesis: verum
end;
suppose m <> 0 ; ::_thesis: x #Z (n + m) = (x #Z n) * (x #Z m)
then A6: 0 + 1 <= m by NAT_1:13;
A7: (0 #Z n) * (0 #Z m) = (0 |^ (abs m)) * (0 #Z n) by PREPOWER:def_3
.= (0 |^ m) * (0 #Z n) by ABSVALUE:def_1
.= 0 * (0 #Z n) by A6, NEWTON:11 ;
 0 #Z (n + m) = 0 * (0 |^ n) by A2, A6, NEWTON:11;
hence  x #Z (n + m) = (x #Z n) * (x #Z m) by A1, A7; ::_thesis: verum
end;
end;
end;
end;
end;
end;

theorem Th2: :: TAYLOR_1:2
for n being Nat
for x being real number holds
( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )
proof
let n be Nat; ::_thesis: for x being real number holds
( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )
let x be real number ; ::_thesis: ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) )
defpred S1[ Nat] means  for x being real number holds
( #Z $1 is_differentiable_in x & diff ((#Z $1),x) = $1 * (x #Z ($1 - 1)) );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
A2: now__::_thesis:_for_x_being_Real_st_x_in_REAL_holds_
(#Z_1)_._x_=_(1_*_x)_+_0
let x be Real; ::_thesis: ( x in REAL implies (#Z 1) . x = (1 * x) + 0 )
assume  x in REAL ; ::_thesis: (#Z 1) . x = (1 * x) + 0
thus (#Z 1) . x = x #Z 1 by Def1
.= (1 * x) + 0 by PREPOWER:35 ; ::_thesis: verum
end;
A3: [#] REAL is open Subset of REAL ;
A4: REAL c= dom (#Z 1) by FUNCT_2:def_1;
then A5: #Z 1 is_differentiable_on REAL by A2, A3, FDIFF_1:23;
A6: for x being real number holds
( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )
proof
let x be real number ; ::_thesis: ( #Z 1 is_differentiable_in x & diff ((#Z 1),x) = 1 )
A7: x is Real by XREAL_0:def_1;
hence  #Z 1 is_differentiable_in x by A3, A5, FDIFF_1:9; ::_thesis: diff ((#Z 1),x) = 1
thus  diff ((#Z 1),x) = ((#Z 1) `| REAL) . x by A5, A7, FDIFF_1:def_7
.= 1 by A2, A4, A3, A7, FDIFF_1:23 ; ::_thesis: verum
end;
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_k_=_0_&_S1[k_+_1]_)_or_(_k_<>_0_&_(_for_x_being_real_number_holds_
(_#Z_(k_+_1)_is_differentiable_in_x_&_diff_((#Z_(k_+_1)),x)_=_(k_+_1)_*_(x_#Z_((k_+_1)_-_1))_)_)_)_)
percases ( k = 0 or k <> 0 ) ;
caseA9: k = 0 ; ::_thesis: S1[k + 1]
thus  S1[k + 1] ::_thesis: verum
proof
let x be real number ; ::_thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )
thus  #Z (k + 1) is_differentiable_in x by A6, A9; ::_thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1))
thus  diff ((#Z (k + 1)),x) = 1 by A6, A9
.= (k + 1) * (x #Z ((k + 1) - 1)) by A9, PREPOWER:34 ; ::_thesis: verum
end;
end;
case k <> 0 ; ::_thesis: for x being real number holds
( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )
then  1 <= k by NAT_1:14;
then  1 - 1 <= k - 1 by XREAL_1:13;
then reconsider k1 = k - 1 as Element of NAT by INT_1:3;
let x be real number ; ::_thesis: ( #Z (k + 1) is_differentiable_in x & diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1)) )
A10: REAL = dom (#Z (k + 1)) by FUNCT_2:def_1;
A11: ( x is Real & #Z k is_differentiable_in x ) by A8, XREAL_0:def_1;
A12: for x being set st x in dom (#Z (k + 1)) holds
(#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)
proof
let x be set ; ::_thesis: ( x in dom (#Z (k + 1)) implies (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x) )
assume  x in dom (#Z (k + 1)) ; ::_thesis: (#Z (k + 1)) . x = ((#Z k) . x) * ((#Z 1) . x)
then reconsider x1 = x as Real ;
thus (#Z (k + 1)) . x = x1 #Z (k + 1) by Def1
.= (x1 #Z k) * (x1 #Z 1) by Th1
.= ((#Z k) . x) * (x1 #Z 1) by Def1
.= ((#Z k) . x) * ((#Z 1) . x) by Def1 ; ::_thesis: verum
end;
A13: #Z 1 is_differentiable_in x by A6;
A14: (dom (#Z k)) /\ (dom (#Z 1)) = ([#] REAL) /\ (dom (#Z 1)) by FUNCT_2:def_1
.= ([#] REAL) /\ REAL by FUNCT_2:def_1 ;
then  #Z (k + 1) = (#Z k) (#) (#Z 1) by A10, A12, VALUED_1:def_4;
hence  #Z (k + 1) is_differentiable_in x by A11, A13, FDIFF_1:16; ::_thesis: diff ((#Z (k + 1)),x) = (k + 1) * (x #Z ((k + 1) - 1))
thus  diff ((#Z (k + 1)),x) = diff (((#Z k) (#) (#Z 1)),x) by A14, A10, A12, VALUED_1:def_4
.= (((#Z k) . x) * (diff ((#Z 1),x))) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A11, A13, FDIFF_1:16
.= (((#Z k) . x) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by A6
.= ((x #Z k) * 1) + ((diff ((#Z k),x)) * ((#Z 1) . x)) by Def1
.= ((x #Z k) * 1) + ((diff ((#Z k),x)) * (x #Z 1)) by Def1
.= (x #Z k) + ((k * (x #Z k1)) * (x #Z 1)) by A8
.= (x #Z k) + (k * ((x #Z k1) * (x #Z 1)))
.= (x #Z k) + (k * (x #Z (k1 + 1))) by Th1
.= (k + 1) * (x #Z ((k + 1) - 1)) ; ::_thesis: verum
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A15: S1[ 0 ]
proof
let x be real number ; ::_thesis: ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) )
set f = #Z 0;
now__::_thesis:_for_y_being_set_st_y_in_{1}_holds_
y_in_rng_(#Z_0)
 dom (#Z 0) = REAL by FUNCT_2:def_1;
then consider x being set  such that
A16: x in dom (#Z 0) ;
reconsider x1 = x as Real by A16;
let y be set ; ::_thesis: ( y in {1} implies y in rng (#Z 0) )
assume A17: y in {1} ; ::_thesis: y in rng (#Z 0)
(#Z 0) . x = x1 #Z 0 by Def1
.= 1 by PREPOWER:34
.= y by A17, TARSKI:def_1 ;
hence  y in rng (#Z 0) by A16, FUNCT_1:def_3; ::_thesis: verum
end;
then A18: {1} c= rng (#Z 0) by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_rng_(#Z_0)_holds_
y_in_{1}
let y be set ; ::_thesis: ( y in rng (#Z 0) implies y in {1} )
assume  y in rng (#Z 0) ; ::_thesis: y in {1}
then consider x being set  such that
A19: x in dom (#Z 0) and
A20: y = (#Z 0) . x by FUNCT_1:def_3;
reconsider x = x as Real by A19;
(#Z 0) . x = x #Z 0 by Def1
.= 1 by PREPOWER:34 ;
hence  y in {1} by A20, TARSKI:def_1; ::_thesis: verum
end;
then  rng (#Z 0) c= {1} by TARSKI:def_3;
then A21: rng (#Z 0) = {1} by A18, XBOOLE_0:def_10;
A22: dom (#Z 0) = [#] REAL by FUNCT_2:def_1;
then A23: #Z 0 is_differentiable_on dom (#Z 0) by A21, FDIFF_1:11;
A24: x is Real by XREAL_0:def_1;
then  ((#Z 0) `| (dom (#Z 0))) . x = 0 by A21, A22, FDIFF_1:11;
hence  ( #Z 0 is_differentiable_in x & diff ((#Z 0),x) = 0 * (x #Z (0 - 1)) ) by A24, A23, A22, FDIFF_1:9, FDIFF_1:def_7; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A15, A1);
hence  ( #Z n is_differentiable_in x & diff ((#Z n),x) = n * (x #Z (n - 1)) ) ; ::_thesis: verum
end;

theorem :: TAYLOR_1:3
for n being Nat
for x0 being real number
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
proof
let n be Nat; ::_thesis: for x0 being real number
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 implies ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; ::_thesis: ( (#Z n) * f is_differentiable_in x0 & diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) )
A2: ( #Z n is_differentiable_in f . x0 & x0 is Real ) by Th2, XREAL_0:def_1;
hence  (#Z n) * f is_differentiable_in x0 by A1, FDIFF_2:13; ::_thesis: diff (((#Z n) * f),x0) = (n * ((f . x0) #Z (n - 1))) * (diff (f,x0))
thus  diff (((#Z n) * f),x0) = (diff ((#Z n),(f . x0))) * (diff (f,x0)) by A1, A2, FDIFF_2:13
.= (n * ((f . x0) #Z (n - 1))) * (diff (f,x0)) by Th2 ; ::_thesis: verum
end;

Lm1:  for n being Nat
for x being real number holds (exp_R x) #R n = exp_R (n * x)
proof
let n be Nat; ::_thesis: for x being real number holds (exp_R x) #R n = exp_R (n * x)
let x be real number ; ::_thesis: (exp_R x) #R n = exp_R (n * x)
reconsider x = x as Real by XREAL_0:def_1;
defpred S1[ Nat] means (exp_R x) #R $1 = exp_R ($1 * x);
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
thus (exp_R x) #R (k + 1) = ((exp_R x) #R k) * ((exp_R x) #R 1) by PREPOWER:75, SIN_COS:55
.= ((exp_R x) #R k) * (exp_R x) by PREPOWER:72, SIN_COS:55
.= exp_R ((k1 * x) + x) by A2, SIN_COS:50
.= exp_R ((k + 1) * x) ; ::_thesis: verum
end;
A3: S1[ 0 ] by PREPOWER:71, SIN_COS:51, SIN_COS:55;
 for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence  (exp_R x) #R n = exp_R (n * x) ; ::_thesis: verum
end;

theorem Th4: :: TAYLOR_1:4
for x being real number holds exp_R (- x) = 1 / (exp_R x)
proof
let x be real number ; ::_thesis: exp_R (- x) = 1 / (exp_R x)
reconsider x = x as Real by XREAL_0:def_1;
(exp_R (- x)) * (exp_R x) = exp_R ((- x) + x) by SIN_COS:50
.= 1 by SIN_COS:51 ;
hence  exp_R (- x) = 1 / (exp_R x) by XCMPLX_1:73; ::_thesis: verum
end;

Lm2:  for i being Integer
for x being real number holds (exp_R x) #R i = exp_R (i * x)
proof
let i be Integer; ::_thesis: for x being real number holds (exp_R x) #R i = exp_R (i * x)
let x be real number ; ::_thesis: (exp_R x) #R i = exp_R (i * x)
consider n being Element of NAT  such that
A1: ( i = n or i = - n ) by INT_1:2;
now__::_thesis:_(_(_i_=_n_&_(exp_R_x)_#R_i_=_exp_R_(i_*_x)_)_or_(_i_=_-_n_&_exp_R_(i_*_x)_=_(exp_R_x)_#R_i_)_)
percases ( i = n or i = - n ) by A1;
case i = n ; ::_thesis: (exp_R x) #R i = exp_R (i * x)
hence  (exp_R x) #R i = exp_R (i * x) by Lm1; ::_thesis: verum
end;
caseA2: i = - n ; ::_thesis: exp_R (i * x) = (exp_R x) #R i
hence  exp_R (i * x) = exp_R (- (n * x))
.= 1 / (exp_R (n * x)) by Th4
.= 1 / ((exp_R x) #R n) by Lm1
.= (exp_R x) #R i by A2, PREPOWER:76, SIN_COS:55 ;
::_thesis: verum
end;
end;
end;
hence  (exp_R x) #R i = exp_R (i * x) ; ::_thesis: verum
end;

theorem Th5: :: TAYLOR_1:5
for i being Integer
for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i)
proof
let i be Integer; ::_thesis: for x being real number holds (exp_R x) #R (1 / i) = exp_R (x / i)
let x be real number ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
set n = i;
percases ( i <> 0 or i = 0 ) ;
supposeA1: i <> 0 ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
then  exp_R x = exp_R ((x / i) * i) by XCMPLX_1:87
.= (exp_R (x / i)) #R i by Lm2 ;
hence (exp_R x) #R (1 / i) = (exp_R (x / i)) #R (i * (1 / i)) by PREPOWER:91, SIN_COS:55
.= (exp_R (x / i)) #R 1 by A1, XCMPLX_1:106
.= exp_R (x / i) by PREPOWER:72, SIN_COS:55 ;
::_thesis: verum
end;
supposeA2: i = 0 ; ::_thesis: (exp_R x) #R (1 / i) = exp_R (x / i)
(exp_R x) #R (1 / 0) = exp_R 0 by PREPOWER:71, SIN_COS:51, SIN_COS:55
.= exp_R (x / 0) by XCMPLX_1:49 ;
hence  (exp_R x) #R (1 / i) = exp_R (x / i) by A2; ::_thesis: verum
end;
end;
end;

theorem Th6: :: TAYLOR_1:6
for x being real number
for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x)
proof
let x be real number ; ::_thesis: for m, n being Integer holds (exp_R x) #R (m / n) = exp_R ((m / n) * x)
let m, n be Integer; ::_thesis: (exp_R x) #R (m / n) = exp_R ((m / n) * x)
thus  exp_R ((m / n) * x) = exp_R ((x / n) * m) by XCMPLX_1:75
.= (exp_R (x / n)) #R m by Lm2
.= ((exp_R x) #R (1 / n)) #R m by Th5
.= (exp_R x) #R ((1 / n) * m) by PREPOWER:91, SIN_COS:55
.= (exp_R x) #R ((m / n) * 1) by XCMPLX_1:75
.= (exp_R x) #R (m / n) ; ::_thesis: verum
end;

Lm3:  for x being real number
for q being Rational holds (exp_R x) #R q = exp_R (q * x)
proof
let x be real number ; ::_thesis: for q being Rational holds (exp_R x) #R q = exp_R (q * x)
let q be Rational; ::_thesis: (exp_R x) #R q = exp_R (q * x)
 ex m being Integer ex n being Element of NAT st
( n <> 0 & q = m / n ) by RAT_1:8;
hence  (exp_R x) #R q = exp_R (q * x) by Th6; ::_thesis: verum
end;

theorem Th7: :: TAYLOR_1:7
for x being real number
for q being Rational holds (exp_R x) #Q q = exp_R (q * x)
proof
let x be real number ; ::_thesis: for q being Rational holds (exp_R x) #Q q = exp_R (q * x)
let q be Rational; ::_thesis: (exp_R x) #Q q = exp_R (q * x)
thus (exp_R x) #Q q = (exp_R x) #R q by PREPOWER:74, SIN_COS:55
.= exp_R (q * x) by Lm3 ; ::_thesis: verum
end;

theorem Th8: :: TAYLOR_1:8
for x, p being real number holds (exp_R x) #R p = exp_R (p * x)
proof
let x, p be real number ; ::_thesis: (exp_R x) #R p = exp_R (p * x)
 exp_R x > 0 by SIN_COS:55;
then consider s being Rational_Sequence such that
A1: ( s is convergent & lim s = p ) and
 (exp_R x) #Q s is convergent and
A2: lim ((exp_R x) #Q s) = (exp_R x) #R p by PREPOWER:def_7;
A3: ( exp_R is_continuous_in x * p & rng (x (#) s) c= dom exp_R ) by FDIFF_1:24, SIN_COS:47, SIN_COS:65;
A4: now__::_thesis:_for_ii_being_set_st_ii_in_NAT_holds_
((exp_R_x)_#Q_s)_._ii_=_(exp_R_/*_(x_(#)_s))_._ii
let ii be set ; ::_thesis: ( ii in NAT implies ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii )
assume  ii in NAT ; ::_thesis: ((exp_R x) #Q s) . ii = (exp_R /* (x (#) s)) . ii
then reconsider i = ii as Element of NAT ;
A5: rng (x (#) s) c= dom exp_R by SIN_COS:47;
thus ((exp_R x) #Q s) . ii = (exp_R x) #Q (s . i) by PREPOWER:def_6
.= exp_R ((s . i) * x) by Th7
.= exp_R ((x (#) s) . i) by SEQ_1:9
.= exp_R . ((x (#) s) . i) by SIN_COS:def_23
.= (exp_R /* (x (#) s)) . ii by A5, FUNCT_2:108 ; ::_thesis: verum
end;
 ( x (#) s is convergent & lim (x (#) s) = x * p ) by A1, SEQ_2:7, SEQ_2:8;
then  lim (exp_R /* (x (#) s)) = exp_R . (x * p) by A3, FCONT_1:def_1
.= exp_R (p * x) by SIN_COS:def_23 ;
hence  (exp_R x) #R p = exp_R (p * x) by A2, A4, FUNCT_2:12; ::_thesis: verum
end;

theorem Th9: :: TAYLOR_1:9
for x being real number holds
( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
proof
let x be real number ; ::_thesis: ( (exp_R 1) #R x = exp_R x & (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
thus A1: exp_R x = exp_R (x * 1)
.= (exp_R 1) #R x by Th8 ; ::_thesis: ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x )
 exp_R 1 > 0 by SIN_COS:55;
hence  ( (exp_R 1) to_power x = exp_R x & number_e to_power x = exp_R x & number_e #R x = exp_R x ) by A1, IRRAT_1:def_7, POWER:def_2; ::_thesis: verum
end;

theorem :: TAYLOR_1:10
for x being real number holds
( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
proof
let x be real number ; ::_thesis: ( (exp_R . 1) #R x = exp_R . x & (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus (exp_R . 1) #R x = (exp_R 1) #R x by SIN_COS:def_23
.= exp_R x by Th9
.= exp_R . x by SIN_COS:def_23 ; ::_thesis: ( (exp_R . 1) to_power x = exp_R . x & number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus (exp_R . 1) to_power x = (exp_R 1) to_power x by SIN_COS:def_23
.= exp_R x by Th9
.= exp_R . x by SIN_COS:def_23 ; ::_thesis: ( number_e to_power x = exp_R . x & number_e #R x = exp_R . x )
thus number_e to_power x = exp_R x by Th9
.= exp_R . x by SIN_COS:def_23 ; ::_thesis: number_e #R x = exp_R . x
thus number_e #R x = exp_R x by Th9
.= exp_R . x by SIN_COS:def_23 ; ::_thesis: verum
end;

theorem :: TAYLOR_1:11
number_e > 2
proof
A1: number_e is irrational by IRRAT_1:41;
A2: for th, th1, th2, th3 being real number
for n being Element of NAT holds
( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
proof
let th, th1, th2, th3 be real number ; ::_thesis: for n being Element of NAT holds
( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
let n be Element of NAT ; ::_thesis: ( th |^ 0 = 1 & th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ 0 = (th GeoSeq) . 0 by PREPOWER:def_1
.= 1 by PREPOWER:3 ; ::_thesis: ( th |^ (2 * n) = (th |^ n) |^ 2 & th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus  th |^ (2 * n) = (th |^ n) |^ 2 by NEWTON:9; ::_thesis: ( th |^ 1 = th & th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A3: th |^ 1 = (th GeoSeq) . (0 + 1) by PREPOWER:def_1
.= ((th GeoSeq) . 0) * th by PREPOWER:3
.= 1 * th by PREPOWER:3
.= th ; ::_thesis: ( th |^ 2 = th * th & (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus th |^ 2 = th |^ (1 + 1)
.= th * th by A3, NEWTON:8 ; ::_thesis: ( (- 1) |^ (2 * n) = 1 & (- 1) |^ ((2 * n) + 1) = - 1 )
thus A4: (- 1) |^ (2 * n) = 1 |^ (2 * n) by POWER:1
.= 1 by NEWTON:10 ; ::_thesis: (- 1) |^ ((2 * n) + 1) = - 1
thus (- 1) |^ ((2 * n) + 1) = ((- 1) |^ (2 * n)) * (- 1) by NEWTON:6
.= - 1 by A4 ; ::_thesis: verum
end;
A5: for n being Element of NAT st 1 <= n holds
(Partial_Sums (1 rExpSeq)) . n >= 2
proof
defpred S1[ Integer] means (Partial_Sums (1 rExpSeq)) . $1 >= 2;
A6: for ni being Integer st 1 <= ni & S1[ni] holds
S1[ni + 1]
proof
let ni be Integer; ::_thesis: ( 1 <= ni & S1[ni] implies S1[ni + 1] )
assume  1 <= ni ; ::_thesis: ( not S1[ni] or S1[ni + 1] )
then reconsider n = ni as Element of NAT by INT_1:3;
A7: (Partial_Sums (1 rExpSeq)) . (n + 1) = ((Partial_Sums (1 rExpSeq)) . n) + ((1 rExpSeq) . (n + 1)) by SERIES_1:def_1
.= ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) by SIN_COS:def_5 ;
 ( 1 |^ (n + 1) > 0 & (n + 1) ! > 0 ) by PREPOWER:6;
then A8: ((Partial_Sums (1 rExpSeq)) . n) + ((1 |^ (n + 1)) / ((n + 1) !)) > (Partial_Sums (1 rExpSeq)) . n by XREAL_1:29, XREAL_1:139;
assume  (Partial_Sums (1 rExpSeq)) . ni >= 2 ; ::_thesis: S1[ni + 1]
hence  S1[ni + 1] by A7, A8, XXREAL_0:2; ::_thesis: verum
end;
(Partial_Sums (1 rExpSeq)) . 1 = ((Partial_Sums (1 rExpSeq)) . 0) + ((1 rExpSeq) . (0 + 1)) by SERIES_1:def_1
.= ((1 rExpSeq) . 0) + ((1 rExpSeq) . 1) by SERIES_1:def_1
.= ((1 rExpSeq) . 0) + ((1 |^ 1) / (1 !)) by SIN_COS:def_5
.= ((1 |^ 0) / (0 !)) + ((1 |^ 1) / (1 !)) by SIN_COS:def_5
.= 1 + ((1 |^ 1) / (1 !)) by A2, NEWTON:12
.= 1 + (1 / 1) by A2, NEWTON:13
.= 2 ;
then A9: S1[1] ;
 for n being Integer st 1 <= n holds
S1[n] from INT_1:sch_2(A9, A6);
hence  for n being Element of NAT st 1 <= n holds
(Partial_Sums (1 rExpSeq)) . n >= 2 ; ::_thesis: verum
end;
A10: for n being Element of NAT holds ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2
proof
let n be Element of NAT ; ::_thesis: ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2
 ((Partial_Sums (1 rExpSeq)) ^\ 1) . n = (Partial_Sums (1 rExpSeq)) . (n + 1) by NAT_1:def_3;
hence  ((Partial_Sums (1 rExpSeq)) ^\ 1) . n >= 2 by A5, NAT_1:11; ::_thesis: verum
end;
 1 rExpSeq is summable by SIN_COS:45;
then A11: Partial_Sums (1 rExpSeq) is convergent by SERIES_1:def_2;
 lim (Partial_Sums (1 rExpSeq)) = Sum (1 rExpSeq) by SERIES_1:def_3;
then  lim ((Partial_Sums (1 rExpSeq)) ^\ 1) = Sum (1 rExpSeq) by A11, SEQ_4:20;
then  Sum (1 rExpSeq) >= 2 by A10, A11, SIN_COS:38;
then  exp_R . 1 >= 2 by SIN_COS:def_22;
then  number_e >= 2 by IRRAT_1:def_7, SIN_COS:def_23;
then  ( number_e > 2 or number_e = 2 ) by XXREAL_0:1;
hence  number_e > 2 by A1; ::_thesis: verum
end;

then Lm4:  number_e > 1
by XXREAL_0:2;

theorem Th12: :: TAYLOR_1:12
for x being real number holds log (number_e,(exp_R x)) = x
proof
let x be real number ; ::_thesis: log (number_e,(exp_R x)) = x
 ( exp_R x > 0 & number_e to_power x = exp_R x ) by Th9, SIN_COS:55;
hence  log (number_e,(exp_R x)) = x by Lm4, POWER:def_3; ::_thesis: verum
end;

theorem Th13: :: TAYLOR_1:13
for x being real number holds log (number_e,(exp_R . x)) = x
proof
let x be real number ; ::_thesis: log (number_e,(exp_R . x)) = x
thus  log (number_e,(exp_R . x)) = log (number_e,(exp_R x)) by SIN_COS:def_23
.= x by Th12 ; ::_thesis: verum
end;

theorem Th14: :: TAYLOR_1:14
for y being real number st y > 0 holds
exp_R (log (number_e,y)) = y
proof
let y be real number ; ::_thesis: ( y > 0 implies exp_R (log (number_e,y)) = y )
assume  y > 0 ; ::_thesis: exp_R (log (number_e,y)) = y
then  number_e to_power (log (number_e,y)) = y by Lm4, POWER:def_3;
hence  exp_R (log (number_e,y)) = y by Th9; ::_thesis: verum
end;

theorem Th15: :: TAYLOR_1:15
for y being real number st y > 0 holds
exp_R . (log (number_e,y)) = y
proof
let y be real number ; ::_thesis: ( y > 0 implies exp_R . (log (number_e,y)) = y )
assume A1: y > 0 ; ::_thesis: exp_R . (log (number_e,y)) = y
thus exp_R . (log (number_e,y)) = exp_R (log (number_e,y)) by SIN_COS:def_23
.= y by A1, Th14 ; ::_thesis: verum
end;

theorem Th16: :: TAYLOR_1:16
( exp_R is one-to-one & exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
proof
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_exp_R_&_x2_in_dom_exp_R_&_exp_R_._x1_=_exp_R_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom exp_R & x2 in dom exp_R & exp_R . x1 = exp_R . x2 implies x1 = x2 )
assume that
A1: x1 in dom exp_R and
A2: x2 in dom exp_R and
A3: exp_R . x1 = exp_R . x2 ; ::_thesis: x1 = x2
reconsider p2 = x2 as Real by A2;
reconsider p1 = x1 as Real by A1;
thus x1 = log (number_e,(exp_R . p1)) by Th13
.= log (number_e,(exp_R . p2)) by A3
.= x2 by Th13 ; ::_thesis: verum
end;
hence  exp_R is one-to-one by FUNCT_1:def_4; ::_thesis: ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL & ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
thus  ( exp_R is_differentiable_on REAL & exp_R is_differentiable_on [#] REAL ) by SIN_COS:66; ::_thesis: ( ( for x being Real holds diff (exp_R,x) = exp_R . x ) & ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
thus  for x being Real holds diff (exp_R,x) = exp_R . x by SIN_COS:66; ::_thesis: ( ( for x being Real holds 0 < diff (exp_R,x) ) & dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
hereby  ::_thesis: ( dom exp_R = [#] REAL & dom exp_R = [#] REAL & rng exp_R = right_open_halfline 0 )
let x be Real; ::_thesis: diff (exp_R,x) > 0
 diff (exp_R,x) = exp_R . x by SIN_COS:66;
hence  diff (exp_R,x) > 0 by SIN_COS:54; ::_thesis: verum
end;
thus  ( dom exp_R = [#] REAL & dom exp_R = [#] REAL ) by SIN_COS:47; ::_thesis: rng exp_R = right_open_halfline 0
now__::_thesis:_for_y_being_set_st_y_in_rng_exp_R_holds_
y_in_right_open_halfline_0
let y be set ; ::_thesis: ( y in rng exp_R implies y in right_open_halfline 0 )
assume  y in rng exp_R ; ::_thesis: y in right_open_halfline 0
then consider x being set  such that
A4: x in dom exp_R and
A5: y = exp_R . x by FUNCT_1:def_3;
reconsider y1 = y as Real by A5;
reconsider x = x as Real by A4;
 exp_R . x > 0 by SIN_COS:54;
then  y1 in  {  g where g is Real : 0 < g  }  by A5;
hence  y in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
then A6: rng exp_R c= right_open_halfline 0 by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_right_open_halfline_0_holds_
y_in_rng_exp_R
let y be set ; ::_thesis: ( y in right_open_halfline 0 implies y in rng exp_R )
assume  y in right_open_halfline 0 ; ::_thesis: y in rng exp_R
then  y in  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then A7: ex g being Real st
( y = g & 0 < g ) ;
then reconsider y1 = y as Real ;
 y1 = exp_R . (log (number_e,y1)) by A7, Th15;
hence  y in rng exp_R by FUNCT_1:def_3, SIN_COS:47; ::_thesis: verum
end;
then  right_open_halfline 0 c= rng exp_R by TARSKI:def_3;
hence  rng exp_R = right_open_halfline 0 by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

registration
cluster exp_R  ->  one-to-one ;
coherence
 exp_R is one-to-one by Th16;
end;

theorem Th17: :: TAYLOR_1:17
( exp_R " is_differentiable_on dom (exp_R ") & ( for x being real number st x in dom (exp_R ") holds
diff ((exp_R "),x) = 1 / x ) )
proof
thus  exp_R " is_differentiable_on dom (exp_R ") by Th16, FDIFF_2:45; ::_thesis: for x being real number st x in dom (exp_R ") holds
diff ((exp_R "),x) = 1 / x
let x be real number ; ::_thesis: ( x in dom (exp_R ") implies diff ((exp_R "),x) = 1 / x )
assume A1: x in dom (exp_R ") ; ::_thesis: diff ((exp_R "),x) = 1 / x
A2: x in rng exp_R by A1, FUNCT_1:33;
diff (exp_R,((exp_R ") . x)) = exp_R . ((exp_R ") . x) by Th16
.= x by A2, FUNCT_1:35 ;
hence  diff ((exp_R "),x) = 1 / x by A1, Th16, FDIFF_2:45; ::_thesis: verum
end;

registration
cluster right_open_halfline 0 ->  non empty ;
coherence
 not right_open_halfline 0 is empty
proof
 1 in  {  g where g is Real : 0 < g  }  ;
hence  not right_open_halfline 0 is empty by XXREAL_1:230; ::_thesis: verum
end;
end;

definition
let a be real number ;
func log_ a ->  PartFunc of REAL,REAL means :Def2: :: TAYLOR_1:def 2
( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = log (a,d) ) );
existence
 ex b1 being PartFunc of REAL,REAL st
( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) )
proof
defpred S1[ set ] means $1 in right_open_halfline 0;
reconsider a = a as Real by XREAL_0:def_1;
deffunc H1( Real) ->  Element of REAL = log (a,$1);
consider f being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom f iff S1[d] ) and
A2: for d being Element of REAL st d in dom f holds
f /. d = H1(d) from PARTFUN2:sch_2();
take  f ; ::_thesis: ( dom f = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f . d = log (a,d) ) )
 for x being set st x in right_open_halfline 0 holds
x in dom f by A1;
then A3: right_open_halfline 0 c= dom f by TARSKI:def_3;
 for x being set st x in dom f holds
x in right_open_halfline 0 by A1;
then  dom f c= right_open_halfline 0 by TARSKI:def_3;
hence A4: dom f = right_open_halfline 0 by A3, XBOOLE_0:def_10; ::_thesis: for d being Element of right_open_halfline 0 holds f . d = log (a,d)
let d be Element of right_open_halfline 0; ::_thesis: f . d = log (a,d)
 f /. d = log (a,d) by A2, A4;
hence  f . d = log (a,d) by A4, PARTFUN1:def_6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = log (a,d) ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) holds
b1 = b2
proof
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = log (a,d) ) & dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = log (a,d) ) implies f1 = f2 )
assume that
A5: dom f1 = right_open_halfline 0 and
A6: for d being Element of right_open_halfline 0 holds f1 . d = log (a,d) and
A7: dom f2 = right_open_halfline 0 and
A8: for d being Element of right_open_halfline 0 holds f2 . d = log (a,d) ; ::_thesis: f1 = f2
 for d being Element of REAL st d in right_open_halfline 0 holds
f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies f1 . d = f2 . d )
assume A9: d in right_open_halfline 0 ; ::_thesis: f1 . d = f2 . d
thus f1 . d = log (a,d) by A6, A9
.= f2 . d by A8, A9 ; ::_thesis: verum
end;
hence  f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines log_ TAYLOR_1:def_2_:_
 for a being real number
for b2 being PartFunc of REAL,REAL holds
( b2 = log_ a iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = log (a,d) ) ) );

definition
func ln  ->  PartFunc of REAL,REAL equals :: TAYLOR_1:def 3
 log_ number_e;
correctness
coherence
log_ number_e is PartFunc of REAL,REAL;
;
end;

:: deftheorem  defines ln TAYLOR_1:def_3_:_
 ln = log_ number_e;

theorem Th18: :: TAYLOR_1:18
( ln = exp_R " & ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )
proof
A1: for d being Element of REAL st d in right_open_halfline 0 holds
(exp_R ") . d = ln . d
proof
let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies (exp_R ") . d = ln . d )
assume A2: d in right_open_halfline 0 ; ::_thesis: (exp_R ") . d = ln . d
 (exp_R ") . d = log (number_e,d)
proof
 d in  {  g where g is Real : 0 < g  }  by A2, XXREAL_1:230;
then  ex g being Real st
( g = d & g > 0 ) ;
then  d = exp_R . (log (number_e,d)) by Th15;
hence  (exp_R ") . d = log (number_e,d) by Th16, FUNCT_1:32; ::_thesis: verum
end;
hence  (exp_R ") . d = ln . d by A2, Def2; ::_thesis: verum
end;
A3: dom (exp_R ") = right_open_halfline 0 by Th16, FUNCT_1:33;
then  dom (exp_R ") = dom ln by Def2;
hence A4: ln = exp_R " by A3, A1, PARTFUN1:5; ::_thesis: ( ln is one-to-one & dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )
A5: for x being Real st x > 0 holds
ln is_differentiable_in x
proof
let x be Real; ::_thesis: ( x > 0 implies ln is_differentiable_in x )
assume  x > 0 ; ::_thesis: ln is_differentiable_in x
then  x in  {  g where g is Real : 0 < g  }  ;
then  x in right_open_halfline 0 by XXREAL_1:230;
hence  ln is_differentiable_in x by A3, A4, Th17, FDIFF_1:9; ::_thesis: verum
end;
A6: for x being Element of right_open_halfline 0 holds 0 < diff (ln,x)
proof
let x be Element of right_open_halfline 0; ::_thesis: 0 < diff (ln,x)
 x in right_open_halfline 0 ;
then  x in  {  g where g is Real : 0 < g  }  by XXREAL_1:230;
then A7: ex g being Real st
( x = g & 0 < g ) ;
 1 / x = x " by XCMPLX_1:215;
hence  0 < diff (ln,x) by A3, A4, A7, Th17; ::_thesis: verum
end;
thus  ln is one-to-one by A4, FUNCT_1:40; ::_thesis: ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) )
 dom ln = right_open_halfline 0 by Def2;
hence  ( dom ln = right_open_halfline 0 & rng ln = REAL & ln is_differentiable_on right_open_halfline 0 & ( for x being Real st x > 0 holds
ln is_differentiable_in x ) & ( for x being Element of right_open_halfline 0 holds diff (ln,x) = 1 / x ) & ( for x being Element of right_open_halfline 0 holds 0 < diff (ln,x) ) ) by A4, A5, A6, Th16, Th17, FUNCT_1:33; ::_thesis: verum
end;

theorem :: TAYLOR_1:19
for x0 being real number
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 implies ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; ::_thesis: ( exp_R * f is_differentiable_in x0 & diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0)) )
A2: ( x0 is Real & exp_R is_differentiable_in f . x0 ) by Th16, FDIFF_1:9, XREAL_0:def_1;
hence  exp_R * f is_differentiable_in x0 by A1, FDIFF_2:13; ::_thesis: diff ((exp_R * f),x0) = (exp_R . (f . x0)) * (diff (f,x0))
thus  diff ((exp_R * f),x0) = (diff (exp_R,(f . x0))) * (diff (f,x0)) by A1, A2, FDIFF_2:13
.= (exp_R . (f . x0)) * (diff (f,x0)) by Th16 ; ::_thesis: verum
end;

theorem :: TAYLOR_1:20
for x0 being real number
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
proof
let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) ) )
assume that
A1: f is_differentiable_in x0 and
A2: f . x0 > 0 ; ::_thesis: ( ln * f is_differentiable_in x0 & diff ((ln * f),x0) = (diff (f,x0)) / (f . x0) )
 f . x0 in  {  g where g is Real : 0 < g  }  by A2;
then A3: f . x0 in right_open_halfline 0 by XXREAL_1:230;
then A4: ln is_differentiable_in f . x0 by Th18, FDIFF_1:9;
A5: x0 is Real by XREAL_0:def_1;
hence  ln * f is_differentiable_in x0 by A1, A4, FDIFF_2:13; ::_thesis: diff ((ln * f),x0) = (diff (f,x0)) / (f . x0)
thus  diff ((ln * f),x0) = (diff (ln,(f . x0))) * (diff (f,x0)) by A1, A4, A5, FDIFF_2:13
.= (1 / (f . x0)) * (diff (f,x0)) by A3, Th18
.= ((diff (f,x0)) / (f . x0)) * 1 by XCMPLX_1:75
.= (diff (f,x0)) / (f . x0) ; ::_thesis: verum
end;

definition
let p be real number ;
func #R p ->  PartFunc of REAL,REAL means :Def4: :: TAYLOR_1:def 4
( dom it = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds it . d = d #R p ) );
existence
 ex b1 being PartFunc of REAL,REAL st
( dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) )
proof
defpred S1[ set ] means $1 in right_open_halfline 0;
reconsider p = p as Real by XREAL_0:def_1;
deffunc H1( Real) ->  Element of REAL = $1 #R p;
consider f being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom f iff S1[d] ) and
A2: for d being Element of REAL st d in dom f holds
f /. d = H1(d) from PARTFUN2:sch_2();
take  f ; ::_thesis: ( dom f = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f . d = d #R p ) )
 for x being set st x in right_open_halfline 0 holds
x in dom f by A1;
then A3: right_open_halfline 0 c= dom f by TARSKI:def_3;
 for x being set st x in dom f holds
x in right_open_halfline 0 by A1;
then  dom f c= right_open_halfline 0 by TARSKI:def_3;
hence A4: dom f = right_open_halfline 0 by A3, XBOOLE_0:def_10; ::_thesis: for d being Element of right_open_halfline 0 holds f . d = d #R p
let d be Element of right_open_halfline 0; ::_thesis: f . d = d #R p
 f /. d = d #R p by A2, A4;
hence  f . d = d #R p by A4, PARTFUN1:def_6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b1 . d = d #R p ) & dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) holds
b1 = b2
proof
let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f1 . d = d #R p ) & dom f2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds f2 . d = d #R p ) implies f1 = f2 )
assume that
A5: dom f1 = right_open_halfline 0 and
A6: for d being Element of right_open_halfline 0 holds f1 . d = d #R p and
A7: dom f2 = right_open_halfline 0 and
A8: for d being Element of right_open_halfline 0 holds f2 . d = d #R p ; ::_thesis: f1 = f2
 for d being Element of REAL st d in right_open_halfline 0 holds
f1 . d = f2 . d
proof
let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies f1 . d = f2 . d )
assume A9: d in right_open_halfline 0 ; ::_thesis: f1 . d = f2 . d
thus f1 . d = d #R p by A6, A9
.= f2 . d by A8, A9 ; ::_thesis: verum
end;
hence  f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines #R TAYLOR_1:def_4_:_
 for p being real number
for b2 being PartFunc of REAL,REAL holds
( b2 = #R p iff ( dom b2 = right_open_halfline 0 & ( for d being Element of right_open_halfline 0 holds b2 . d = d #R p ) ) );

theorem Th21: :: TAYLOR_1:21
for x, p being real number st x > 0 holds
( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) )
proof
let x, p be real number ; ::_thesis: ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) )
set f = #R p;
A1: p is Real by XREAL_0:def_1;
A2: for x being Real st 0 < x holds
( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) )
proof
let x be Real; ::_thesis: ( 0 < x implies ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) ) )
assume A3: x > 0 ; ::_thesis: ( exp_R * (p (#) ln) is_differentiable_in x & diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1)) )
A4: ln is_differentiable_in x by A3, Th18;
then A5: p (#) ln is_differentiable_in x by A1, FDIFF_1:15;
 x in  {  g where g is Real : 0 < g  }  by A3;
then A6: x in right_open_halfline 0 by XXREAL_1:230;
then A7: x in dom (p (#) ln) by Th18, VALUED_1:def_5;
A8: diff ((p (#) ln),x) = p * (diff (ln,x)) by A1, A4, FDIFF_1:15
.= p * (1 / x) by A6, Th18 ;
A9: exp_R is_differentiable_in (p (#) ln) . x by SIN_COS:65;
hence  exp_R * (p (#) ln) is_differentiable_in x by A5, FDIFF_2:13; ::_thesis: diff ((exp_R * (p (#) ln)),x) = p * (x #R (p - 1))
diff (exp_R,((p (#) ln) . x)) = exp_R . ((p (#) ln) . x) by Th16
.= exp_R . (p * (ln . x)) by A7, VALUED_1:def_5
.= exp_R . (p * (log (number_e,x))) by A6, Def2
.= exp_R . (log (number_e,(x to_power p))) by A3, Lm4, POWER:55
.= x to_power p by A3, Th15, POWER:34 ;
hence  diff ((exp_R * (p (#) ln)),x) = (x to_power p) * (p * (1 / x)) by A5, A9, A8, FDIFF_2:13
.= p * ((x to_power p) * (1 / x))
.= p * ((x to_power p) * (1 / (x to_power 1))) by POWER:25
.= p * ((x to_power p) * (x to_power (- 1))) by A3, POWER:28
.= p * (x to_power (p + (- 1))) by A3, POWER:27
.= p * (x #R (p - 1)) by A3, POWER:def_2 ;
::_thesis: verum
end;
 rng (p (#) ln) c= dom exp_R by Th16;
then A10: dom (exp_R * (p (#) ln)) = dom (p (#) ln) by RELAT_1:27
.= right_open_halfline 0 by Th18, VALUED_1:def_5 ;
A11: for d being Element of REAL st d in right_open_halfline 0 holds
(exp_R * (p (#) ln)) . d = (#R p) . d
proof
let d be Element of REAL ; ::_thesis: ( d in right_open_halfline 0 implies (exp_R * (p (#) ln)) . d = (#R p) . d )
assume A12: d in right_open_halfline 0 ; ::_thesis: (exp_R * (p (#) ln)) . d = (#R p) . d
A13: d in dom (p (#) ln) by A12, Th18, VALUED_1:def_5;
 d in  {  g where g is Real : 0 < g  }  by A12, XXREAL_1:230;
then A14: ex g being Real st
( g = d & g > 0 ) ;
thus (exp_R * (p (#) ln)) . d = (exp_R * (p (#) ln)) /. d by A10, A12, PARTFUN1:def_6
.= exp_R /. ((p (#) ln) /. d) by A10, A12, PARTFUN2:3
.= exp_R . ((p (#) ln) . d) by A13, PARTFUN1:def_6
.= exp_R . (p * (ln . d)) by A13, VALUED_1:def_5
.= exp_R . (p * (log (number_e,d))) by A12, Def2
.= exp_R . (log (number_e,(d to_power p))) by A14, Lm4, POWER:55
.= d to_power p by A14, Th15, POWER:34
.= d #R p by A14, POWER:def_2
.= (#R p) . d by A12, Def4 ; ::_thesis: verum
end;
 dom (#R p) = right_open_halfline 0 by Def4;
then  ( x is Real & exp_R * (p (#) ln) = #R p ) by A10, A11, PARTFUN1:5, XREAL_0:def_1;
hence  ( x > 0 implies ( #R p is_differentiable_in x & diff ((#R p),x) = p * (x #R (p - 1)) ) ) by A2; ::_thesis: verum
end;

theorem :: TAYLOR_1:22
for x0, p being real number
for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) )
proof
let x0, p be real number ; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_in x0 & f . x0 > 0 holds
( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) )
let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_in x0 & f . x0 > 0 implies ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) ) )
assume that
A1: f is_differentiable_in x0 and
A2: f . x0 > 0 ; ::_thesis: ( (#R p) * f is_differentiable_in x0 & diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) )
A3: x0 is Real by XREAL_0:def_1;
A4: #R p is_differentiable_in f . x0 by A2, Th21;
hence  (#R p) * f is_differentiable_in x0 by A1, A3, FDIFF_2:13; ::_thesis: diff (((#R p) * f),x0) = (p * ((f . x0) #R (p - 1))) * (diff (f,x0))
thus  diff (((#R p) * f),x0) = (diff ((#R p),(f . x0))) * (diff (f,x0)) by A1, A4, A3, FDIFF_2:13
.= (p * ((f . x0) #R (p - 1))) * (diff (f,x0)) by A2, Th21 ; ::_thesis: verum
end;

begin

definition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
func diff (f,Z) ->  Functional_Sequence of REAL,REAL means :Def5: :: TAYLOR_1:def 5
( it . 0 = f | Z & ( for i being Nat holds it . (i + 1) = (it . i) `| Z ) );
existence
 ex b1 being Functional_Sequence of REAL,REAL st
( b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) )
proof
reconsider fZ = f | Z as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
defpred S1[ set , set , set ] means  ex h being PartFunc of REAL,REAL st
( $2 = h & $3 = h `| Z );
A1: for n being Element of NAT
for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of PFuncs (REAL,REAL) ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
let x be Element of PFuncs (REAL,REAL); ::_thesis: ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y]
reconsider x9 = x as PartFunc of REAL,REAL by PARTFUN1:46;
reconsider y = x9 `| Z as Element of PFuncs (REAL,REAL) by PARTFUN1:45;
 ex h being PartFunc of REAL,REAL st
( x = h & y = h `| Z ) ;
hence  ex y being Element of PFuncs (REAL,REAL) st S1[n,x,y] ; ::_thesis: verum
end;
consider g being Function of NAT,(PFuncs (REAL,REAL)) such that
A2: ( g . 0 = fZ & ( for n being Element of NAT holds S1[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
reconsider g = g as Functional_Sequence of REAL,REAL ;
take  g ; ::_thesis: ( g . 0 = f | Z & ( for i being Nat holds g . (i + 1) = (g . i) `| Z ) )
thus  g . 0 = f | Z by A2; ::_thesis: for i being Nat holds g . (i + 1) = (g . i) `| Z
let i be Nat; ::_thesis: g . (i + 1) = (g . i) `| Z
 i is Element of NAT by ORDINAL1:def_12;
then  S1[i,g . i,g . (i + 1)] by A2;
hence  g . (i + 1) = (g . i) `| Z ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Functional_Sequence of REAL,REAL st b1 . 0 = f | Z & ( for i being Nat holds b1 . (i + 1) = (b1 . i) `| Z ) & b2 . 0 = f | Z & ( for i being Nat holds b2 . (i + 1) = (b2 . i) `| Z ) holds
b1 = b2
proof
let seq1, seq2 be Functional_Sequence of REAL,REAL; ::_thesis: ( seq1 . 0 = f | Z & ( for i being Nat holds seq1 . (i + 1) = (seq1 . i) `| Z ) & seq2 . 0 = f | Z & ( for i being Nat holds seq2 . (i + 1) = (seq2 . i) `| Z ) implies seq1 = seq2 )
assume that
A3: seq1 . 0 = f | Z and
A4: for n being Nat holds seq1 . (n + 1) = (seq1 . n) `| Z and
A5: seq2 . 0 = f | Z and
A6: for n being Nat holds seq2 . (n + 1) = (seq2 . n) `| Z ; ::_thesis: seq1 = seq2
defpred S1[ Element of NAT ] means seq1 . $1 = seq2 . $1;
A7: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; ::_thesis: S1[k + 1]
thus seq1 . (k + 1) = (seq1 . k) `| Z by A4
.= seq2 . (k + 1) by A6, A8 ; ::_thesis: verum
end;
A9: S1[ 0 ] by A3, A5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7);
hence  seq1 = seq2 by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines diff TAYLOR_1:def_5_:_
 for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b3 being Functional_Sequence of REAL,REAL holds
( b3 = diff (f,Z) iff ( b3 . 0 = f | Z & ( for i being Nat holds b3 . (i + 1) = (b3 . i) `| Z ) ) );

definition
let f be PartFunc of REAL,REAL;
let n be Nat;
let Z be Subset of REAL;
predf is_differentiable_on n,Z means :Def6: :: TAYLOR_1:def 6
 for i being Element of NAT st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z;
end;

:: deftheorem Def6 defines is_differentiable_on TAYLOR_1:def_6_:_
 for f being PartFunc of REAL,REAL
for n being Nat
for Z being Subset of REAL holds
( f is_differentiable_on n,Z iff for i being Element of NAT st i <= n - 1 holds
(diff (f,Z)) . i is_differentiable_on Z );

theorem Th23: :: TAYLOR_1:23
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
let Z be Subset of REAL; ::_thesis: for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z
let n be Nat; ::_thesis: ( f is_differentiable_on n,Z implies for m being Nat st m <= n holds
f is_differentiable_on m,Z )
assume A1: f is_differentiable_on n,Z ; ::_thesis: for m being Nat st m <= n holds
f is_differentiable_on m,Z
let m be Nat; ::_thesis: ( m <= n implies f is_differentiable_on m,Z )
assume A2: m <= n ; ::_thesis: f is_differentiable_on m,Z
now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_m_-_1_holds_
(diff_(f,Z))_._i_is_differentiable_on_Z
A3: m - 1 <= n - 1 by A2, XREAL_1:13;
let i be Element of NAT ; ::_thesis: ( i <= m - 1 implies (diff (f,Z)) . i is_differentiable_on Z )
assume  i <= m - 1 ; ::_thesis: (diff (f,Z)) . i is_differentiable_on Z
then  i <= n - 1 by A3, XXREAL_0:2;
hence  (diff (f,Z)) . i is_differentiable_on Z by A1, Def6; ::_thesis: verum
end;
hence  f is_differentiable_on m,Z by Def6; ::_thesis: verum
end;

definition
let f be PartFunc of REAL,REAL;
let Z be Subset of REAL;
let a, b be real number ;
func Taylor (f,Z,a,b) ->  Real_Sequence means :Def7: :: TAYLOR_1:def 7
 for n being Nat holds it . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !);
existence
 ex b1 being Real_Sequence st
for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
proof
deffunc H1( Element of NAT ) ->  Element of REAL = ((((diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 !);
consider seq being Real_Sequence such that
A1: for n being Element of NAT holds seq . n = H1(n) from SEQ_1:sch_1();
take  seq ; ::_thesis: for n being Nat holds seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
let n be Nat; ::_thesis: seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !)
 n is Element of NAT by ORDINAL1:def_12;
hence  seq . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds b2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) holds
b1 = b2
proof
deffunc H1( Nat) ->  Element of REAL = ((((diff (f,Z)) . $1) . a) * ((b - a) |^ $1)) / ($1 !);
let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Nat holds s1 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) & ( for n being Nat holds s2 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) ) implies s1 = s2 )
assume that
A2: for n being Nat holds s1 . n = H1(n) and
A3: for n being Nat holds s2 . n = H1(n) ; ::_thesis: s1 = s2
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
s1_._x_=_s2_._x
let x be set ; ::_thesis: ( x in NAT implies s1 . x = s2 . x )
assume  x in NAT ; ::_thesis: s1 . x = s2 . x
then reconsider n = x as Element of NAT ;
thus s1 . x = H1(n) by A2
.= s2 . x by A3 ; ::_thesis: verum
end;
hence  s1 = s2 by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines Taylor TAYLOR_1:def_7_:_
 for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for a, b being real number
for b5 being Real_Sequence holds
( b5 = Taylor (f,Z,a,b) iff for n being Nat holds b5 . n = ((((diff (f,Z)) . n) . a) * ((b - a) |^ n)) / (n !) );

Lm5:  for b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
proof
defpred S1[ set ] means $1 in REAL ;
let b be Real; ::_thesis: ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
deffunc H1( Real) ->  Element of REAL = b - $1;
consider g being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S1[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H1(d) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) )
 for x being set st x in REAL holds
x in dom g by A1;
then A3: REAL c= dom g by TARSKI:def_3;
then A4: dom g = [#] REAL by XBOOLE_0:def_10;
A5: for d being Element of REAL holds g . d = b - d
proof
let d be Element of REAL ; ::_thesis: g . d = b - d
 g /. d = b - d by A2, A4;
hence  g . d = b - d by A4, PARTFUN1:def_6; ::_thesis: verum
end;
A6: for d being Real st d in REAL holds
g . d = ((- 1) * d) + b
proof
let d be Real; ::_thesis: ( d in REAL implies g . d = ((- 1) * d) + b )
assume  d in REAL ; ::_thesis: g . d = ((- 1) * d) + b
thus g . d = b - d by A5
.= ((- 1) * d) + b ; ::_thesis: verum
end;
then A7: g is_differentiable_on dom g by A4, FDIFF_1:23;
 for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 )
proof
let d be Real; ::_thesis: ( g is_differentiable_in d & diff (g,d) = - 1 )
thus  g is_differentiable_in d by A4, A7, FDIFF_1:9; ::_thesis: diff (g,d) = - 1
thus  diff (g,d) = (g `| (dom g)) . d by A4, A7, FDIFF_1:def_7
.= - 1 by A4, A6, FDIFF_1:23 ; ::_thesis: verum
end;
hence  ( dom g = [#] REAL & ( for x being Real holds
( g . x = b - x & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) by A3, A5, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm6:  for n being Element of NAT
for l, b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) )
proof
defpred S1[ set ] means $1 in REAL ;
let n be Element of NAT ; ::_thesis: for l, b being Real ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) )
let l, b be Real; ::_thesis: ex g being PartFunc of REAL,REAL st
( dom g = [#] REAL & ( for x being Real holds
( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) )
deffunc H1( Real) ->  Element of REAL = (l * ((b - $1) |^ (n + 1))) / ((n + 1) !);
consider g being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S1[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H1(d) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds
( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) )
consider f being PartFunc of REAL,REAL such that
A3: dom f = [#] REAL and
A4: for x being Real holds f . x = b - x and
A5: for x being Real holds
( f is_differentiable_in x & diff (f,x) = - 1 ) by Lm5;
 ( dom (#Z (n + 1)) = REAL & rng f c= REAL ) by FUNCT_2:def_1;
then A6: dom ((#Z (n + 1)) * f) = dom f by RELAT_1:27;
 for x being set st x in REAL holds
x in dom g by A1;
then A7: REAL c= dom g by TARSKI:def_3;
then A8: dom g = [#] REAL by XBOOLE_0:def_10;
A9: for d being Element of REAL holds g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)
proof
let d be Element of REAL ; ::_thesis: g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !)
 g /. d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A2, A8;
hence  g . d = (l * ((b - d) |^ (n + 1))) / ((n + 1) !) by A8, PARTFUN1:def_6; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_Element_of_REAL_st_x_in_dom_((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f))_holds_
((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f))_._x_=_g_._x
let x be Element of REAL ; ::_thesis: ( x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) implies ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x )
assume  x in dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) ; ::_thesis: ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = g . x
hence ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) . x = (l / ((n + 1) !)) * (((#Z (n + 1)) * f) . x) by VALUED_1:def_5
.= (l / ((n + 1) !)) * (((#Z (n + 1)) * f) /. x) by A3, A6, PARTFUN1:def_6
.= (l / ((n + 1) !)) * ((#Z (n + 1)) /. (f /. x)) by A3, A6, PARTFUN2:3
.= (l / ((n + 1) !)) * ((#Z (n + 1)) . (f . x)) by A3, PARTFUN1:def_6
.= (l / ((n + 1) !)) * ((f . x) #Z (n + 1)) by Def1
.= (l / ((n + 1) !)) * ((f . x) |^ (n + 1)) by PREPOWER:36
.= (l / ((n + 1) !)) * ((b - x) |^ (n + 1)) by A4
.= (l * ((b - x) |^ (n + 1))) / ((n + 1) !) by XCMPLX_1:74
.= g . x by A9 ;
::_thesis: verum
end;
A11: for x being Real holds
( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )
proof
let x be Real; ::_thesis: ( (#Z (n + 1)) * f is_differentiable_in x & diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n)) )
A12: ( f is_differentiable_in x & #Z (n + 1) is_differentiable_in f . x ) by A5, Th2;
hence  (#Z (n + 1)) * f is_differentiable_in x by FDIFF_2:13; ::_thesis: diff (((#Z (n + 1)) * f),x) = - ((n + 1) * ((b - x) #Z n))
 diff ((#Z (n + 1)),(f . x)) = (n + 1) * ((f . x) #Z ((n + 1) - 1)) by Th2;
hence  diff (((#Z (n + 1)) * f),x) = ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (diff (f,x)) by A12, FDIFF_2:13
.= ((n + 1) * ((f . x) #Z ((n + 1) - 1))) * (- 1) by A5
.= ((n + 1) * ((b - x) #Z ((n + 1) - 1))) * (- 1) by A4
.= - ((n + 1) * ((b - x) #Z n)) ;
::_thesis: verum
end;
A13: now__::_thesis:_for_x_being_Real_holds_
(_(l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f)_is_differentiable_in_x_&_diff_(((l_/_((n_+_1)_!))_(#)_((#Z_(n_+_1))_*_f)),x)_=_-_((l_*_((b_-_x)_|^_n))_/_(n_!))_)
let x be Real; ::_thesis: ( (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x & diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !)) )
A14: (n + 1) / ((n + 1) !) = (1 * (n + 1)) / ((n !) * (n + 1)) by NEWTON:15
.= 1 / (n !) by XCMPLX_1:91 ;
A15: (#Z (n + 1)) * f is_differentiable_in x by A11;
hence  (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) is_differentiable_in x by FDIFF_1:15; ::_thesis: diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = - ((l * ((b - x) |^ n)) / (n !))
thus  diff (((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)),x) = (l / ((n + 1) !)) * (diff (((#Z (n + 1)) * f),x)) by A15, FDIFF_1:15
.= ((diff (((#Z (n + 1)) * f),x)) / ((n + 1) !)) * l by XCMPLX_1:75
.= l * ((- ((n + 1) * ((b - x) #Z n))) / ((n + 1) !)) by A11
.= l * ((- ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)) by PREPOWER:36
.= (l * (- ((n + 1) * ((b - x) |^ n)))) / ((n + 1) !) by XCMPLX_1:74
.= ((- l) * ((n + 1) * ((b - x) |^ n))) / ((n + 1) !)
.= (- l) * (((n + 1) * ((b - x) |^ n)) / ((n + 1) !)) by XCMPLX_1:74
.= (- l) * (((b - x) |^ n) * ((n + 1) / ((n + 1) !))) by XCMPLX_1:74
.= (- l) * (((b - x) |^ n) / (n !)) by A14, XCMPLX_1:99
.= - (l * (((b - x) |^ n) / (n !)))
.= - ((l * ((b - x) |^ n)) / (n !)) by XCMPLX_1:74 ; ::_thesis: verum
end;
 dom ((l / ((n + 1) !)) (#) ((#Z (n + 1)) * f)) = dom g by A8, A3, A6, VALUED_1:def_5;
then  (l / ((n + 1) !)) (#) ((#Z (n + 1)) * f) = g by A10, PARTFUN1:5;
hence  ( dom g = [#] REAL & ( for x being Real holds
( g . x = (l * ((b - x) |^ (n + 1))) / ((n + 1) !) & ( for x being Real holds
( g is_differentiable_in x & diff (g,x) = - ((l * ((b - x) |^ n)) / (n !)) ) ) ) ) ) by A7, A9, A13, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm7:  for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b being Real ex 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) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b being Real ex 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) ) )
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for b being Real ex 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) ) )
let Z be Subset of REAL; ::_thesis: for b being Real ex 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) ) )
let b be Real; ::_thesis: ex 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) ) )
defpred S1[ set ] means $1 in Z;
deffunc H1( Real) ->  Element of REAL = (f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n);
consider g being PartFunc of REAL,REAL such that
A1: for d being Element of REAL holds
( d in dom g iff S1[d] ) and
A2: for d being Element of REAL st d in dom g holds
g /. d = H1(d) from PARTFUN2:sch_2();
take  g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) )
 for x being set st x in dom g holds
x in Z by A1;
then A3: dom g c= Z by TARSKI:def_3;
 for x being set st x in Z holds
x in dom g by A1;
then A4: Z c= dom g by TARSKI:def_3;
 for d being Real st d in Z holds
g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
proof
let d be Real; ::_thesis: ( d in Z implies g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) )
assume A5: d in Z ; ::_thesis: g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n)
 g /. d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) by A2, A4, A5;
hence  g . d = (f . b) - ((Partial_Sums (Taylor (f,Z,d,b))) . n) by A4, A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence  ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th24: :: TAYLOR_1:24
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
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 holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
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 holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n
let Z be Subset of REAL; ::_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 holds
((diff (f,Z)) . n) | ].a,b.[ = (diff (f,].a,b.[)) . n
defpred S1[ Element of NAT ] means ( f is_differentiable_on $1,Z implies for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . $1) | ].a,b.[ = (diff (f,].a,b.[)) . $1 );
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
assume A3: f is_differentiable_on k + 1,Z ; ::_thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1)
let a, b be Real; ::_thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1) )
assume that
A4: a < b and
A5: ].a,b.[ c= Z ; ::_thesis: ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (diff (f,].a,b.[)) . (k + 1)
 k <= (k + 1) - 1 ;
then A6: (diff (f,Z)) . k is_differentiable_on Z by A3, Def6;
then A7: (diff (f,Z)) . k is_differentiable_on ].a,b.[ by A5, FDIFF_1:26;
then A8: dom (((diff (f,Z)) . k) `| ].a,b.[) = ].a,b.[ by FDIFF_1:def_7;
A9: dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) = (dom (((diff (f,Z)) . k) `| Z)) /\ ].a,b.[ by RELAT_1:61
.= Z /\ ].a,b.[ by A6, FDIFF_1:def_7
.= ].a,b.[ by A5, XBOOLE_1:28 ;
A10: now__::_thesis:_for_x_being_Real_st_x_in_dom_((((diff_(f,Z))_._k)_`|_Z)_|_].a,b.[)_holds_
((((diff_(f,Z))_._k)_`|_Z)_|_].a,b.[)_._x_=_(((diff_(f,Z))_._k)_`|_].a,b.[)_._x
let x be Real; ::_thesis: ( x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) implies ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x )
assume A11: x in dom ((((diff (f,Z)) . k) `| Z) | ].a,b.[) ; ::_thesis: ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| ].a,b.[) . x
thus ((((diff (f,Z)) . k) `| Z) | ].a,b.[) . x = (((diff (f,Z)) . k) `| Z) . x by A9, A11, FUNCT_1:49
.= diff (((diff (f,Z)) . k),x) by A5, A6, A9, A11, FDIFF_1:def_7
.= (((diff (f,Z)) . k) `| ].a,b.[) . x by A7, A9, A11, FDIFF_1:def_7 ; ::_thesis: verum
end;
thus ((diff (f,Z)) . (k + 1)) | ].a,b.[ = (((diff (f,Z)) . k) `| Z) | ].a,b.[ by Def5
.= ((diff (f,Z)) . k) `| ].a,b.[ by A9, A8, A10, PARTFUN1:5
.= (((diff (f,Z)) . k) | ].a,b.[) `| ].a,b.[ by A7, FDIFF_2:16
.= ((diff (f,].a,b.[)) . k) `| ].a,b.[ by A2, A3, A4, A5, Th23, NAT_1:11
.= (diff (f,].a,b.[)) . (k + 1) by Def5 ; ::_thesis: verum
end;
A12: S1[ 0 ]
proof
assume  f is_differentiable_on 0 ,Z ; ::_thesis: for a, b being Real st a < b & ].a,b.[ c= Z holds
((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0
let a, b be Real; ::_thesis: ( a < b & ].a,b.[ c= Z implies ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0 )
assume that
 a < b and
A13: ].a,b.[ c= Z ; ::_thesis: ((diff (f,Z)) . 0) | ].a,b.[ = (diff (f,].a,b.[)) . 0
thus ((diff (f,Z)) . 0) | ].a,b.[ = (f | Z) | ].a,b.[ by Def5
.= f | ].a,b.[ by A13, FUNCT_1:51
.= (diff (f,].a,b.[)) . 0 by Def5 ; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A1); ::_thesis: verum
end;

Lm8:  for f being PartFunc of REAL,REAL
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 . 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 !)) ) )
proof
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 . 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 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 . 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 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 . 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 S1[ 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 . 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: S1[ 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;
 0 <= (0 + 1) - 1 ;
then  (diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A6, Def6;
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_set_st_xx_in_dom_(g_|_[.a,b.])_holds_
(g_|_[.a,b.])_._xx_=_((y_*_f)_|_[.a,b.])_._xx
let xx be set ; ::_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_set_st_xx_in_dom_(g_|_].a,b.[)_holds_
(g_|_].a,b.[)_._xx_=_((y_*_f)_|_].a,b.[)_._xx
let xx be set ; ::_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 Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A41: S1[k] ; ::_thesis: S1[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) !)) ) )
 k <= (k + 1) - 1 ;
then  (diff (f,Z)) . k is_differentiable_on Z by A42, Def6;
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)_!))_)_)
 k <= (k + 1) - 1 ;
then A55: (diff (f,Z)) . k is_differentiable_on Z by A42, Def6;
 k <= ((k + 1) + 1) - 1 by NAT_1:11;
then A56: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A46, Def6;
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_Real_st_x_in_Z_holds_
gk1_._x_=_(gk_-_(((diff_(f,Z))_._(k_+_1))_(#)_h))_._x
let x be 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_set_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 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 . 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;
 k + 1 <= ((k + 1) + 1) - 1 ;
then A76: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A46, Def6;
 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 Element of NAT holds S1[k] from NAT_1:sch_1(A2, 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 . 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
end;

Lm9:  for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 !)) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 & f is_differentiable_on n,Z implies 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
ex 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) ) & 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 & f is_differentiable_on n,Z ) ; ::_thesis: 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
ex 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) ) & 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 a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex 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) ) & 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 A2: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex 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) ) & 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 !)) ) )
consider g being PartFunc of REAL,REAL such that
A3: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) ) by Lm7;
take  g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & 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 !)) ) )
thus  ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n) ) & 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 !)) ) ) by A1, A2, A3, Lm8; ::_thesis: verum
end;

theorem Th25: :: TAYLOR_1:25
for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) ) )
assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies for l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) ) )
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: for l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
let l be Real; ::_thesis: for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
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: ( dom g = [#] REAL & ( for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 implies ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) ) )
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: ( g is_differentiable_on ].a,b.[ & g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
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 set st x in dom (h - p) holds
(h - p) . x = g . x
proof
let x be set ; ::_thesis: ( x in dom (h - p) implies (h - p) . x = g . x )
assume A20: x in dom (h - p) ; ::_thesis: (h - p) . x = g . x
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: verum
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: ( x in ].a,b.[ implies ( 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 !)) ) )
assume A26: x in ].a,b.[ ; ::_thesis: ( 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 !)) )
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: diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !))
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: verum
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: ( g . a = 0 & g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
thus  g . a = 0 by A16, A17; ::_thesis: ( g . b = 0 & g | [.a,b.] is continuous & ( 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 !)) ) )
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: ( g | [.a,b.] is continuous & ( 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 !)) ) )
(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: 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 !))
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: verum
proof
let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !)) )
assume A32: x in ].a,b.[ ; ::_thesis: diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((b - x) |^ n)) / (n !))) + ((l * ((b - x) |^ n)) / (n !))
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: verum
end;
end;

theorem Th26: :: TAYLOR_1:26
for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b, l being Real ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for b, l being Real ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for b, l being Real ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
let Z be Subset of REAL; ::_thesis: for b, l being Real ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
let b, l be Real; ::_thesis: ex g being Function of REAL,REAL st
for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
deffunc H1( Real) ->  Element of REAL = ((f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n)) - ((l * ((b - $1) |^ (n + 1))) / ((n + 1) !));
consider g being Function of REAL,REAL such that
A1: for d being Element of REAL holds g . d = H1(d) from FUNCT_2:sch_4();
take  g ; ::_thesis: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !))
thus  for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) by A1; ::_thesis: verum
end;

theorem Th27: :: TAYLOR_1:27
for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies 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
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) )
assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: 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
ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) )
assume that
A2: a < b and
A3: ( [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) )
 b - a <> 0 by A2;
then A4: (b - a) |^ (n + 1) <> 0 by CARD_4:3;
deffunc H1( Real) ->  Element of REAL = (f . b) - ((Partial_Sums (Taylor (f,Z,$1,b))) . n);
reconsider l = H1(a) / (((b - a) |^ (n + 1)) / ((n + 1) !)) as Real ;
consider g being Function of REAL,REAL such that
A5: for x being Real holds g . x = ((f . b) - ((Partial_Sums (Taylor (f,Z,x,b))) . n)) - ((l * ((b - x) |^ (n + 1))) / ((n + 1) !)) by Th26;
A6: ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - ((l * ((b - a) |^ (n + 1))) / ((n + 1) !)) = H1(a) - ((H1(a) / (((b - a) |^ (n + 1)) / ((n + 1) !))) * (((b - a) |^ (n + 1)) / ((n + 1) !))) by XCMPLX_1:74
.= H1(a) - H1(a) by A4, XCMPLX_1:50, XCMPLX_1:87
.= 0 ;
then A7: g . a = 0 by A5;
A8: dom g = REAL by FUNCT_2:def_1;
then A9: g | [.a,b.] is continuous by A1, A2, A3, A5, A6, Th25;
 ( g is_differentiable_on ].a,b.[ & g . b = 0 ) by A1, A2, A3, A5, A6, A8, Th25;
then consider c being Real such that
A10: c in ].a,b.[ and
A11: diff (g,c) = 0 by A2, A8, A7, A9, ROLLE:1;
 c in  {  r where r is Real : ( a < r & r < b )  }  by A10, RCOMP_1:def_2;
then  ex r being Real st
( c = r & a < r & r < b ) ;
then  b - c <> 0 ;
then A12: (b - c) |^ n <> 0 by CARD_4:3;
 dom g = REAL by FUNCT_2:def_1;
then  (- (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n !))) + ((l * ((b - c) |^ n)) / (n !)) = 0 by A1, A2, A3, A5, A6, A10, A11, Th25;
then  ((((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / (n !)) * (n !)) - (((l * ((b - c) |^ n)) / (n !)) * (n !)) = 0 ;
then  ((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (((l * ((b - c) |^ n)) / (n !)) * (n !)) = 0 by XCMPLX_1:87;
then  (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) - (l * ((b - c) |^ n))) / ((b - c) |^ n) = 0 / ((b - c) |^ n) by XCMPLX_1:87;
then  (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - c) |^ n)) / ((b - c) |^ n)) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by XCMPLX_1:120;
then  (((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((b - c) |^ n)) / ((b - c) |^ n)) = 0 by A12, XCMPLX_1:89;
then  ((f . b) - ((Partial_Sums (Taylor (f,Z,a,b))) . n)) - (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) = 0 by A6, A12, XCMPLX_1:89;
then  f . b = (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (Taylor (f,Z,a,b))) . n) ;
hence  ex c being Real st
( c in ].a,b.[ & f . b = ((Partial_Sums (Taylor (f,Z,a,b))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((b - a) |^ (n + 1))) / ((n + 1) !)) ) by A10; ::_thesis: verum
end;

Lm10:  for f being PartFunc of REAL,REAL
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 !)) ) )
proof
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 A1: 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 S1[ 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 !)) ) ) );
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
assume A4: 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
A5: a < b and
A6: [.a,b.] c= Z and
A7: ((diff (f,Z)) . (k + 1)) | [.a,b.] is continuous and
A8: 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) !)) ) )
 k <= (k + 1) - 1 ;
then  (diff (f,Z)) . k is_differentiable_on Z by A4, Def6;
then  ((diff (f,Z)) . k) | Z is continuous by FDIFF_1:25;
then A9: ((diff (f,Z)) . k) | [.a,b.] is continuous by A6, FCONT_1:16;
A10: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A11: ].a,b.[ c= Z by A6, XBOOLE_1:1;
consider gk being PartFunc of REAL,REAL such that
A12: dom gk = Z and
A13: for x being Real st x in Z holds
gk . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . k) by Lm7;
A14: f is_differentiable_on k + 1,].a,b.[ by A8, Th23, NAT_1:11;
then A15: gk is_differentiable_on ].a,b.[ by A3, A4, A5, A6, A9, A12, A13, Th23, NAT_1:11;
A16: gk | [.a,b.] is continuous by A3, A4, A5, A6, A9, A14, A12, A13, 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_._a)_-_((Partial_Sums_(Taylor_(f,Z,x,a)))_._(k_+_1))_)_holds_
(_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)_!))_)_)
 k <= (k + 1) - 1 ;
then A17: (diff (f,Z)) . k is_differentiable_on Z by A4, Def6;
 k <= ((k + 1) + 1) - 1 by NAT_1:11;
then A18: (diff (f,].a,b.[)) . k is_differentiable_on ].a,b.[ by A8, Def6;
A19: (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 . 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
A20: dom gk1 = Z and
A21: 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) !)) ) )
A22: a in [.a,b.] by A5, XXREAL_1:1;
then gk1 . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . (k + 1)) by A6, A21
.= (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 A6, A13, A22
.= 0 - ((Taylor (f,Z,a,a)) . (k + 1)) by A3, A4, A5, A6, A9, A14, A12, A13, Th23, NAT_1:11
.= 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:6
.= 0 ;
hence  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) !)) ) )
consider h being PartFunc of REAL,REAL such that
A23: dom h = [#] REAL and
A24: for x being Real holds h . x = (1 * ((a - x) |^ (k + 1))) / ((k + 1) !) and
A25: for x being Real holds
( h is_differentiable_in x & diff (h,x) = - ((1 * ((a - x) |^ k)) / (k !)) ) by Lm6;
A26: dom (((diff (f,Z)) . (k + 1)) (#) h) = (dom ((diff (f,Z)) . (k + 1))) /\ (dom h) by VALUED_1:def_4
.= Z /\ REAL by A23, A19, A17, FDIFF_1:def_7
.= Z by XBOOLE_1:28 ;
A27: dom (gk - (((diff (f,Z)) . (k + 1)) (#) h)) = (dom gk) /\ (dom (((diff (f,Z)) . (k + 1)) (#) h)) by VALUED_1:12
.= Z by A12, A26 ;
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);
 for x being Real st x in REAL holds
h is_differentiable_in x by A25;
then  h is_differentiable_on REAL by A23, FDIFF_1:9;
then  h | REAL is continuous by FDIFF_1:25;
then A28: h | [.a,b.] is continuous by FCONT_1:16;
now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_
gk1_._x_=_(gk_-_(((diff_(f,Z))_._(k_+_1))_(#)_h))_._x
let x be Real; ::_thesis: ( x in Z implies gk1 . x = (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x )
assume A29: 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 A21, A29
.= (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 A13, A29
.= (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:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A27, A29, VALUED_1:13 ; ::_thesis: verum
end;
then A30: gk1 = gk - (((diff (f,Z)) . (k + 1)) (#) h) by A20, A27, PARTFUN1:5;
 [.a,b.] c= dom ((diff (f,Z)) . (k + 1)) by A6, A19, A17, FDIFF_1:def_7;
then  (((diff (f,Z)) . (k + 1)) (#) h) | ([.a,b.] /\ [.a,b.]) is continuous by A7, A23, A28, FCONT_1:19;
hence  gk1 | [.a,b.] is continuous by A6, A12, A16, A26, A30, FCONT_1:19; ::_thesis: verum
end;
A31: (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);
A32: 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 A23, A31, A18, FDIFF_1:def_7
.= ].a,b.[ by XBOOLE_1:28 ;
A33: dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = Z /\ (dom (((diff (f,].a,b.[)) . (k + 1)) (#) h)) by A12, VALUED_1:12
.= ].a,b.[ by A6, A10, A32, XBOOLE_1:1, XBOOLE_1:28 ;
A34: 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 A35: 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 A33, A35, 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 A4, A5, A6, A10, Th24, XBOOLE_1:1
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A35, 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 A11, A27, A35, VALUED_1:13 ; ::_thesis: verum
end;
A36: now__::_thesis:_for_xx_being_set_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 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 A37: 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 A37;
thus gk1 . xx = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . (k + 1)) by A11, A21, A33, A37
.= (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 A11, A13, A33, A37
.= (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:74
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) . x) * (h . x)) by A24
.= (gk . x) - ((((diff (f,Z)) . (k + 1)) (#) h) . x) by VALUED_1:5
.= (gk - (((diff (f,Z)) . (k + 1)) (#) h)) . x by A11, A27, A33, A37, VALUED_1:13
.= (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) . xx by A33, A34, A37 ; ::_thesis: verum
end;
 k + 1 <= ((k + 1) + 1) - 1 ;
then A38: (diff (f,].a,b.[)) . (k + 1) is_differentiable_on ].a,b.[ by A8, Def6;
 for x being Real st x in ].a,b.[ holds
h is_differentiable_in x by A25;
then A39: h is_differentiable_on ].a,b.[ by A23, FDIFF_1:9;
then A40: ((diff (f,].a,b.[)) . (k + 1)) (#) h is_differentiable_on ].a,b.[ by A32, A38, FDIFF_1:21;
then A41: gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h) is_differentiable_on ].a,b.[ by A15, A33, FDIFF_1:19;
 dom (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) = (dom gk1) /\ ].a,b.[ by A6, A10, A20, A33, XBOOLE_1:1, XBOOLE_1:28;
then A42: (gk1 | ].a,b.[) | ].a,b.[ = (gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[ by A36, 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 A41, FDIFF_1:def_6;
hence A43: gk1 is_differentiable_on ].a,b.[ by A11, A20, 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) * ((a - 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)_*_((a_-_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) * ((a - x) |^ (k + 1))) / ((k + 1) !)) )
assume A44: 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 A43, A44, FDIFF_1:def_7
.= ((gk1 | ].a,b.[) `| ].a,b.[) . x by A43, FDIFF_2:16
.= (((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) | ].a,b.[) `| ].a,b.[) . x by A42, FUNCT_1:51
.= ((gk - (((diff (f,].a,b.[)) . (k + 1)) (#) h)) `| ].a,b.[) . x by A41, FDIFF_2:16
.= (diff (gk,x)) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A15, A33, A40, A44, FDIFF_1:19
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (diff ((((diff (f,].a,b.[)) . (k + 1)) (#) h),x)) by A3, A4, A5, A6, A9, A14, A12, A13, A44, Th23, NAT_1:11
.= (- (((((diff (f,].a,b.[)) . (k + 1)) . x) * ((a - x) |^ k)) / (k !))) - (((((diff (f,].a,b.[)) . (k + 1)) (#) h) `| ].a,b.[) . x) by A40, A44, FDIFF_1:def_7
.= (- (((((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 A32, A38, A39, A44, FDIFF_1:21
.= ((- (((((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 A24
.= ((- (((((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 A25
.= ((- (((((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:74
.= - ((((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 A38, A44, FDIFF_1:def_7
.= - ((((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: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) * ((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;
A45: S1[ 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
A46: a < b and
A47: [.a,b.] c= Z and
A48: ((diff (f,Z)) . 0) | [.a,b.] is continuous and
A49: 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 !)) ) )
A50: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
then A51: ].a,b.[ c= Z by A47, 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 . 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
A52: dom g = Z and
A53: 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 !)) ) )
A54: a in [.a,b.] by A46, XXREAL_1:1;
hence g . a = (f . a) - ((Partial_Sums (Taylor (f,Z,a,a))) . 0) by A47, A53
.= (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 A47, A54, FUNCT_1:49
.= (f . a) - ((f . a) * 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) * ((a - x) |^ 0)) / (0 !)) ) )
consider y being PartFunc of REAL,REAL such that
A55: dom y = [#] REAL and
A56: for x being Real holds y . x = (f . a) - x and
A57: for x being Real holds
( y is_differentiable_in x & diff (y,x) = - 1 ) by Lm5;
 rng f c= REAL ;
then A58: dom (y * f) = dom f by A55, RELAT_1:27;
 for x being Real st x in REAL holds
y is_differentiable_in x by A57;
then  y is_differentiable_on REAL by A55, FDIFF_1:9;
then  y | REAL is continuous by FDIFF_1:25;
then A59: y | (f .: [.a,b.]) is continuous by FCONT_1:16;
 rng f c= dom y by A55;
then A60: dom (y * f) = dom f by RELAT_1:27;
A61: [.a,b.] c= dom f by A1, A47, XBOOLE_1:1;
then A62: ].a,b.[ c= dom f by A50, XBOOLE_1:1;
 0 <= (0 + 1) - 1 ;
then  (diff (f,].a,b.[)) . 0 is_differentiable_on ].a,b.[ by A49, Def6;
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 A63: f is_differentiable_on ].a,b.[ by A62, FDIFF_1:def_6;
A64: 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
A65: (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 A63, 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) * ((a - x) |^ 0)) / (0 !)) ) )
assume A66: 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 !)) )
A67: f is_differentiable_in x by A63, A66, FDIFF_1:9;
A68: y is_differentiable_in f . x by A57;
hence  y * f is_differentiable_in x by A67, FDIFF_2:13; ::_thesis: diff ((y * f),x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !))
A69: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus  diff ((y * f),x) = (diff (y,(f . x))) * (diff (f,x)) by A68, A67, FDIFF_2:13
.= (diff (y,(f . x))) * ((f `| ].a,b.[) . x) by A63, A66, FDIFF_1:def_7
.= (- 1) * (((diff (f,].a,b.[)) . (0 + 1)) . x) by A57, A65
.= - ((((diff (f,].a,b.[)) . (0 + 1)) . x) * (((a - x) |^ 0) / (0 !))) by A69
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - 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 A70: y * f is_differentiable_on ].a,b.[ by A62, A60, FDIFF_1:9;
A71: dom ((y * f) | [.a,b.]) = (dom (y * f)) /\ [.a,b.] by RELAT_1:61
.= [.a,b.] by A1, A47, A58, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ [.a,b.] by A47, XBOOLE_1:28
.= dom (g | [.a,b.]) by A52, RELAT_1:61 ;
A72: now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_[.a,b.])_holds_
(g_|_[.a,b.])_._xx_=_((y_*_f)_|_[.a,b.])_._xx
let xx be set ; ::_thesis: ( xx in dom (g | [.a,b.]) implies (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx )
assume A73: xx in dom (g | [.a,b.]) ; ::_thesis: (g | [.a,b.]) . xx = ((y * f) | [.a,b.]) . xx
reconsider x = xx as Real by A73;
 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 A74: x in [.a,b.] by A73;
thus (g | [.a,b.]) . xx = g . x by A73, FUNCT_1:47
.= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A47, A53, A74
.= (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 A47, A74, FUNCT_1:49
.= (f . a) - ((f . x) * 1) by NEWTON:4, NEWTON:12
.= y . (f . x) by A56
.= (y * f) . x by A61, A74, FUNCT_1:13
.= ((y * f) | [.a,b.]) . xx by A71, A73, FUNCT_1:47 ; ::_thesis: verum
end;
 (f | Z) | [.a,b.] is continuous by A48, Def5;
then  ((f | Z) | [.a,b.]) | [.a,b.] is continuous by FCONT_1:15;
then  (f | [.a,b.]) | [.a,b.] is continuous by A47, FUNCT_1:51;
then  f | [.a,b.] is continuous by FCONT_1:15;
then  (y * f) | [.a,b.] is continuous by A59, FCONT_1:25;
hence  g | [.a,b.] is continuous by A71, A72, 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) * ((a - x) |^ 0)) / (0 !)) ) )
A75: dom ((y * f) | ].a,b.[) = (dom (y * f)) /\ ].a,b.[ by RELAT_1:61
.= ].a,b.[ by A50, A61, A60, XBOOLE_1:1, XBOOLE_1:28
.= Z /\ ].a,b.[ by A47, A50, XBOOLE_1:1, XBOOLE_1:28
.= dom (g | ].a,b.[) by A52, RELAT_1:61 ;
now__::_thesis:_for_xx_being_set_st_xx_in_dom_(g_|_].a,b.[)_holds_
(g_|_].a,b.[)_._xx_=_((y_*_f)_|_].a,b.[)_._xx
let xx be set ; ::_thesis: ( xx in dom (g | ].a,b.[) implies (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx )
assume A76: xx in dom (g | ].a,b.[) ; ::_thesis: (g | ].a,b.[) . xx = ((y * f) | ].a,b.[) . xx
reconsider x = xx as Real by A76;
 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 A77: x in ].a,b.[ by A76;
A78: ((a - x) |^ 0) / (0 !) = 1 by NEWTON:4, NEWTON:12;
thus (g | ].a,b.[) . xx = g . x by A76, FUNCT_1:47
.= (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . 0) by A53, A51, A77
.= (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 A51, A77, FUNCT_1:49
.= (f . a) - ((f . x) * (((a - x) |^ 0) / (0 !))) by XCMPLX_1:74
.= y . (f . x) by A56, A78
.= (y * f) . x by A62, A77, FUNCT_1:13
.= ((y * f) | ].a,b.[) . xx by A75, A76, FUNCT_1:47 ; ::_thesis: verum
end;
then A79: g | ].a,b.[ = (y * f) | ].a,b.[ by A75, FUNCT_1:2;
then  g | ].a,b.[ is_differentiable_on ].a,b.[ by A70, 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 A80: g is_differentiable_on ].a,b.[ by A52, A51, 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) * ((a - 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)_*_((a_-_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) * ((a - x) |^ 0)) / (0 !)) ) )
assume A81: 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 A80, A81, FDIFF_1:9; ::_thesis: diff (g,x) = - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !))
thus  diff (g,x) = (g `| ].a,b.[) . x by A80, A81, FDIFF_1:def_7
.= ((g | ].a,b.[) `| ].a,b.[) . x by A80, FDIFF_2:16
.= ((y * f) `| ].a,b.[) . x by A79, A70, FDIFF_2:16
.= diff ((y * f),x) by A70, A81, FDIFF_1:def_7
.= - (((((diff (f,].a,b.[)) . (0 + 1)) . x) * ((a - x) |^ 0)) / (0 !)) by A64, A81 ; ::_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;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A45, A2);
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
end;

Lm11:  for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 !)) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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
ex 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) ) & 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 & f is_differentiable_on n,Z implies 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
ex 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) ) & 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 A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: 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
ex 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) ) & 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 a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex 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) ) & 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 A2: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex 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) ) & 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 !)) ) )
consider g being PartFunc of REAL,REAL such that
A3: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) ) by Lm7;
take  g ; ::_thesis: ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & 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 !)) ) )
thus  ( dom g = Z & ( for x being Real st x in Z holds
g . x = (f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) ) & 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 !)) ) ) by A1, A2, A3, Lm10; ::_thesis: verum
end;

theorem Th28: :: TAYLOR_1:28
for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) )
assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: 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 l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies for l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) )
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: for l being Real
for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
let l be Real; ::_thesis: for g being PartFunc of REAL,REAL st dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 holds
( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
consider p being PartFunc of REAL,REAL such that
A5: dom p = [#] REAL and
A6: for x being Real holds p . x = (l * ((a - x) |^ (n + 1))) / ((n + 1) !) and
A7: for x being Real holds
( p is_differentiable_in x & diff (p,x) = - ((l * ((a - 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 . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n) and
A10: h . a = 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) * ((a - x) |^ n)) / (n !)) by A1, A2, A3, A4, Lm11;
A14: [.a,b.] c= (dom h) /\ (dom p) by A3, A8, A5, XBOOLE_1:19;
let g be PartFunc of REAL,REAL; ::_thesis: ( dom g = [#] REAL & ( for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) ) & ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 implies ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) ) )
assume that
A15: dom g = [#] REAL and
A16: for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) and
A17: ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = 0 ; ::_thesis: ( g is_differentiable_on ].a,b.[ & g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
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 set st x in dom (h - p) holds
(h - p) . x = g . x
proof
let x be set ; ::_thesis: ( x in dom (h - p) implies (h - p) . x = g . x )
assume A20: x in dom (h - p) ; ::_thesis: (h - p) . x = g . x
reconsider xx = x as Real by A20;
thus (h - p) . x = (h . xx) - (p . xx) by A20, VALUED_1:13
.= ((f . a) - ((Partial_Sums (Taylor (f,Z,xx,a))) . n)) - (p . xx) by A9, A18, A20
.= ((f . a) - ((Partial_Sums (Taylor (f,Z,xx,a))) . n)) - ((l * ((a - xx) |^ (n + 1))) / ((n + 1) !)) by A6
.= g . x by A16 ; ::_thesis: verum
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) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) )
proof
let x be Real; ::_thesis: ( x in ].a,b.[ implies ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
assume A26: x in ].a,b.[ ; ::_thesis: ( h - p is_differentiable_in x & diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) )
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: diff ((h - p),x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !))
thus  diff ((h - p),x) = (diff (h,x)) - (diff (p,x)) by A27, A28, FDIFF_1:14
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) - (diff (p,x)) by A13, A26
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) - (- ((l * ((a - x) |^ n)) / (n !))) by A7
.= (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ; ::_thesis: verum
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: ( g . b = 0 & g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
thus  g . b = 0 by A16, A17; ::_thesis: ( g . a = 0 & g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
A31: a in [.a,b.] by A2, XXREAL_1:1;
then g . a = (h - p) . a by A3, A18, A19
.= (h . a) - (p . a) by A3, A18, A31, VALUED_1:13
.= 0 - ((l * ((a - a) |^ (n + 1))) / ((n + 1) !)) by A10, A6
.= 0 - ((l * ((0 |^ n) * 0)) / ((n + 1) !)) by NEWTON:6
.= 0 ;
hence  g . a = 0 ; ::_thesis: ( g | [.a,b.] is continuous & ( for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ) )
(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: for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !))
thus  for x being Real st x in ].a,b.[ holds
diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) ::_thesis: verum
proof
let x be Real; ::_thesis: ( x in ].a,b.[ implies diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) )
assume A32: x in ].a,b.[ ; ::_thesis: diff (g,x) = (- (((((diff (f,].a,b.[)) . (n + 1)) . x) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !))
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) * ((a - x) |^ n)) / (n !))) + ((l * ((a - x) |^ n)) / (n !)) by A25, A32 ; ::_thesis: verum
end;
end;

theorem Th29: :: TAYLOR_1:29
for n being Element of NAT
for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
proof
let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st Z c= dom f & 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
ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let Z be Subset of REAL; ::_thesis: ( Z c= dom f & f is_differentiable_on n,Z implies 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
ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) )
assume A1: ( Z c= dom f & f is_differentiable_on n,Z ) ; ::_thesis: 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
ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let a, b be Real; ::_thesis: ( a < b & [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ implies ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) )
assume that
A2: a < b and
A3: ( [.a,b.] c= Z & ((diff (f,Z)) . n) | [.a,b.] is continuous & f is_differentiable_on n + 1,].a,b.[ ) ; ::_thesis: ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
 a - b <> 0 by A2;
then A4: (a - b) |^ (n + 1) <> 0 by CARD_4:3;
deffunc H1( Real) ->  Element of REAL = (f . a) - ((Partial_Sums (Taylor (f,Z,$1,a))) . n);
reconsider l = H1(b) / (((a - b) |^ (n + 1)) / ((n + 1) !)) as Real ;
consider g being Function of REAL,REAL such that
A5: for x being Real holds g . x = ((f . a) - ((Partial_Sums (Taylor (f,Z,x,a))) . n)) - ((l * ((a - x) |^ (n + 1))) / ((n + 1) !)) by Th26;
A6: ((f . a) - ((Partial_Sums (Taylor (f,Z,b,a))) . n)) - ((l * ((a - b) |^ (n + 1))) / ((n + 1) !)) = H1(b) - ((H1(b) / (((a - b) |^ (n + 1)) / ((n + 1) !))) * (((a - b) |^ (n + 1)) / ((n + 1) !))) by XCMPLX_1:74
.= H1(b) - H1(b) by A4, XCMPLX_1:50, XCMPLX_1:87
.= 0 ;
then A7: g . b = 0 by A5;
A8: dom g = REAL by FUNCT_2:def_1;
then A9: g | [.a,b.] is continuous by A1, A2, A3, A5, A6, Th28;
 ( g is_differentiable_on ].a,b.[ & g . a = 0 ) by A1, A2, A3, A5, A6, A8, Th28;
then consider c being Real such that
A10: c in ].a,b.[ and
A11: diff (g,c) = 0 by A2, A8, A7, A9, ROLLE:1;
 c in  {  r where r is Real : ( a < r & r < b )  }  by A10, RCOMP_1:def_2;
then  ex r being Real st
( c = r & a < r & r < b ) ;
then  a - c <> 0 ;
then A12: (a - c) |^ n <> 0 by CARD_4:3;
 dom g = REAL by FUNCT_2:def_1;
then  (- (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n !))) + ((l * ((a - c) |^ n)) / (n !)) = 0 by A1, A2, A3, A5, A6, A10, A11, Th28;
then  ((((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / (n !)) * (n !)) - (((l * ((a - c) |^ n)) / (n !)) * (n !)) = 0 ;
then  ((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (((l * ((a - c) |^ n)) / (n !)) * (n !)) = 0 by XCMPLX_1:87;
then  (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) - (l * ((a - c) |^ n))) / ((a - c) |^ n) = 0 / ((a - c) |^ n) by XCMPLX_1:87;
then  (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - c) |^ n)) / ((a - c) |^ n)) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by XCMPLX_1:120;
then  (((diff (f,].a,b.[)) . (n + 1)) . c) - ((l * ((a - c) |^ n)) / ((a - c) |^ n)) = 0 by A12, XCMPLX_1:89;
then  ((diff (f,].a,b.[)) . (n + 1)) . c = l by A12, XCMPLX_1:89;
then  f . a = (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) + ((Partial_Sums (Taylor (f,Z,b,a))) . n) by A6;
hence  ex c being Real st
( c in ].a,b.[ & f . a = ((Partial_Sums (Taylor (f,Z,b,a))) . n) + (((((diff (f,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) by A10; ::_thesis: verum
end;

theorem Th30: :: TAYLOR_1:30
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Element of NAT st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Element of NAT st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
let Z be Subset of REAL; ::_thesis: for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Element of NAT st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
let Z1 be open Subset of REAL; ::_thesis: ( Z1 c= Z implies for n being Element of NAT st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n )
assume A1: Z1 c= Z ; ::_thesis: for n being Element of NAT st f is_differentiable_on n,Z holds
((diff (f,Z)) . n) | Z1 = (diff (f,Z1)) . n
defpred S1[ Element of NAT ] means ( f is_differentiable_on $1,Z implies ((diff (f,Z)) . $1) | Z1 = (diff (f,Z1)) . $1 );
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
assume A4: f is_differentiable_on k + 1,Z ; ::_thesis: ((diff (f,Z)) . (k + 1)) | Z1 = (diff (f,Z1)) . (k + 1)
 k <= (k + 1) - 1 ;
then A5: (diff (f,Z)) . k is_differentiable_on Z by A4, Def6;
then A6: (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26;
then A7: dom (((diff (f,Z)) . k) `| Z1) = Z1 by FDIFF_1:def_7;
A8: dom ((((diff (f,Z)) . k) `| Z) | Z1) = (dom (((diff (f,Z)) . k) `| Z)) /\ Z1 by RELAT_1:61
.= Z /\ Z1 by A5, FDIFF_1:def_7
.= Z1 by A1, XBOOLE_1:28 ;
A9: now__::_thesis:_for_x_being_Real_st_x_in_dom_((((diff_(f,Z))_._k)_`|_Z)_|_Z1)_holds_
((((diff_(f,Z))_._k)_`|_Z)_|_Z1)_._x_=_(((diff_(f,Z))_._k)_`|_Z1)_._x
let x be Real; ::_thesis: ( x in dom ((((diff (f,Z)) . k) `| Z) | Z1) implies ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x )
assume A10: x in dom ((((diff (f,Z)) . k) `| Z) | Z1) ; ::_thesis: ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z1) . x
thus ((((diff (f,Z)) . k) `| Z) | Z1) . x = (((diff (f,Z)) . k) `| Z) . x by A8, A10, FUNCT_1:49
.= diff (((diff (f,Z)) . k),x) by A1, A5, A8, A10, FDIFF_1:def_7
.= (((diff (f,Z)) . k) `| Z1) . x by A6, A8, A10, FDIFF_1:def_7 ; ::_thesis: verum
end;
thus ((diff (f,Z)) . (k + 1)) | Z1 = (((diff (f,Z)) . k) `| Z) | Z1 by Def5
.= ((diff (f,Z)) . k) `| Z1 by A8, A7, A9, PARTFUN1:5
.= ((diff (f,Z1)) . k) `| Z1 by A3, A4, A6, Th23, FDIFF_2:16, NAT_1:11
.= (diff (f,Z1)) . (k + 1) by Def5 ; ::_thesis: verum
end;
A11: S1[ 0 ]
proof
assume  f is_differentiable_on 0 ,Z ; ::_thesis: ((diff (f,Z)) . 0) | Z1 = (diff (f,Z1)) . 0
thus ((diff (f,Z)) . 0) | Z1 = (f | Z) | Z1 by Def5
.= f | Z1 by A1, FUNCT_1:51
.= (diff (f,Z1)) . 0 by Def5 ; ::_thesis: verum
end;
thus  for k being Element of NAT holds S1[k] from NAT_1:sch_1(A11, A2); ::_thesis: verum
end;

theorem Th31: :: TAYLOR_1:31
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z be Subset of REAL; ::_thesis: for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z1 be open Subset of REAL; ::_thesis: ( Z1 c= Z implies for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1 )
assume A1: Z1 c= Z ; ::_thesis: for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let n be Nat; ::_thesis: ( f is_differentiable_on n + 1,Z implies f is_differentiable_on n + 1,Z1 )
assume A2: f is_differentiable_on n + 1,Z ; ::_thesis: f is_differentiable_on n + 1,Z1
now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_(n_+_1)_-_1_holds_
(diff_(f,Z1))_._k_is_differentiable_on_Z1
let k be Element of NAT ; ::_thesis: ( k <= (n + 1) - 1 implies (diff (f,Z1)) . k is_differentiable_on Z1 )
assume A3: k <= (n + 1) - 1 ; ::_thesis: (diff (f,Z1)) . k is_differentiable_on Z1
 (diff (f,Z)) . k is_differentiable_on Z by A2, A3, Def6;
then  (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26;
then A4: ((diff (f,Z)) . k) | Z1 is_differentiable_on Z1 by FDIFF_2:16;
 n <= n + 1 by NAT_1:11;
then  k <= n + 1 by A3, XXREAL_0:2;
hence  (diff (f,Z1)) . k is_differentiable_on Z1 by A1, A2, A4, Th23, Th30; ::_thesis: verum
end;
hence  f is_differentiable_on n + 1,Z1 by Def6; ::_thesis: verum
end;

theorem Th32: :: TAYLOR_1:32
for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x being Real st x in Z holds
for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n
proof
let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL
for x being Real st x in Z holds
for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n
let Z be Subset of REAL; ::_thesis: for x being Real st x in Z holds
for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n
let x be Real; ::_thesis: ( x in Z implies for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n )
assume A1: x in Z ; ::_thesis: for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n
defpred S1[ Element of NAT ] means f . x = (Partial_Sums (Taylor (f,Z,x,x))) . $1;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
thus (Partial_Sums (Taylor (f,Z,x,x))) . (k + 1) = ((Partial_Sums (Taylor (f,Z,x,x))) . k) + ((Taylor (f,Z,x,x)) . (k + 1)) by SERIES_1:def_1
.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((x - x) |^ (k + 1))) / ((k + 1) !)) by A3, Def7
.= (f . x) + (((((diff (f,Z)) . (k + 1)) . x) * ((0 |^ k) * 0)) / ((k + 1) !)) by NEWTON:6
.= f . x ; ::_thesis: verum
end;
(Partial_Sums (Taylor (f,Z,x,x))) . 0 = (Taylor (f,Z,x,x)) . 0 by SERIES_1:def_1
.= ((((diff (f,Z)) . 0) . x) * ((x - x) |^ 0)) / (0 !) by Def7
.= (((f | Z) . x) * ((x - x) |^ 0)) / (0 !) by Def5
.= (((f | Z) . x) * 1) / 1 by NEWTON:4, NEWTON:12
.= f . x by A1, FUNCT_1:49 ;
then A4: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2);
hence  for n being Element of NAT holds f . x = (Partial_Sums (Taylor (f,Z,x,x))) . n ; ::_thesis: verum
end;

theorem :: TAYLOR_1:33
for n being Element of NAT
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) !)) )
proof
let n be Element of 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_Element_of_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)_!))_)_)_or_(_x_=_x0_&_ex_s_being_Element_of_REAL_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_Element_of_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)_!))_)_)_)
percases ( x < x0 or x = x0 or x > x0 ) by XXREAL_0:1;
caseA5: x < x0 ; ::_thesis: ex s being Element of 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) !)) )
 abs (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;
 n <= (n + 1) - 1 ;
then  (diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3, Def6;
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;
caseA15: x = x0 ; ::_thesis: ex s being Element of REAL 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;
caseA16: x > x0 ; ::_thesis: ex s being Element of 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) !)) )
set t = x - x0;
A17: f is_differentiable_on n,].(x0 - r),(x0 + r).[ by A3, Th23, NAT_1:11;
 abs (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;
 n <= (n + 1) - 1 ;
then  (diff (f,].(x0 - r),(x0 + r).[)) . n is_differentiable_on ].(x0 - r),(x0 + r).[ by A3, Def6;
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
end;