:: TAYLOR_1 semantic presentation

definition
let c1 be Integer;
func #Z c1 -> Function of REAL , REAL means :Def1: :: TAYLOR_1:def 1
for b1 being real number holds a2 . b1 = b1 #Z a1;
existence
ex b1 being Function of REAL , REAL st
for b2 being real number holds b1 . b2 = b2 #Z c1
proof end;
uniqueness
for b1, b2 being Function of REAL , REAL st ( for b3 being real number holds b1 . b3 = b3 #Z c1 ) & ( for b3 being real number holds b2 . b3 = b3 #Z c1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines #Z TAYLOR_1:def 1 :
for b1 being Integer
for b2 being Function of REAL , REAL holds
( b2 = #Z b1 iff for b3 being real number holds b2 . b3 = b3 #Z b1 );

theorem Th1: :: TAYLOR_1:1
for b1 being real number
for b2, b3 being natural number holds b1 #Z (b3 + b2) = (b1 #Z b3) * (b1 #Z b2)
proof end;

theorem Th2: :: TAYLOR_1:2
for b1 being natural number
for b2 being real number holds
( #Z b1 is_differentiable_in b2 & diff (#Z b1),b2 = b1 * (b2 #Z (b1 - 1)) )
proof end;

theorem Th3: :: TAYLOR_1:3
for b1 being natural number
for b2 being real number
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_in b2 holds
( (#Z b1) * b3 is_differentiable_in b2 & diff ((#Z b1) * b3),b2 = (b1 * ((b3 . b2) #Z (b1 - 1))) * (diff b3,b2) )
proof end;

Lemma4: for b1 being natural number
for b2 being real number holds (exp b2) #R b1 = exp (b1 * b2)
proof end;

theorem Th4: :: TAYLOR_1:4
for b1 being real number holds exp (- b1) = 1 / (exp b1)
proof end;

Lemma6: for b1 being Integer
for b2 being real number holds (exp b2) #R b1 = exp (b1 * b2)
proof end;

theorem Th5: :: TAYLOR_1:5
for b1 being Integer
for b2 being real number holds (exp b2) #R (1 / b1) = exp (b2 / b1)
proof end;

theorem Th6: :: TAYLOR_1:6
for b1 being real number
for b2, b3 being Integer holds (exp b1) #R (b2 / b3) = exp ((b2 / b3) * b1)
proof end;

Lemma9: for b1 being real number
for b2 being Rational holds (exp b1) #R b2 = exp (b2 * b1)
proof end;

theorem Th7: :: TAYLOR_1:7
for b1 being real number
for b2 being Rational holds (exp b1) #Q b2 = exp (b2 * b1)
proof end;

theorem Th8: :: TAYLOR_1:8
for b1, b2 being real number holds (exp b1) #R b2 = exp (b2 * b1)
proof end;

theorem Th9: :: TAYLOR_1:9
for b1 being real number holds
( (exp 1) #R b1 = exp b1 & (exp 1) to_power b1 = exp b1 & number_e to_power b1 = exp b1 & number_e #R b1 = exp b1 )
proof end;

theorem Th10: :: TAYLOR_1:10
for b1 being real number holds
( (exp . 1) #R b1 = exp . b1 & (exp . 1) to_power b1 = exp . b1 & number_e to_power b1 = exp . b1 & number_e #R b1 = exp . b1 )
proof end;

theorem Th11: :: TAYLOR_1:11
number_e >= 2
proof end;

then Lemma13: ( number_e > 1 & number_e > 0 )
by XREAL_1:2;

theorem Th12: :: TAYLOR_1:12
for b1 being real number holds log number_e ,(exp b1) = b1
proof end;

theorem Th13: :: TAYLOR_1:13
for b1 being real number holds log number_e ,(exp . b1) = b1
proof end;

theorem Th14: :: TAYLOR_1:14
for b1 being real number st b1 > 0 holds
exp (log number_e ,b1) = b1
proof end;

theorem Th15: :: TAYLOR_1:15
for b1 being real number st b1 > 0 holds
exp . (log number_e ,b1) = b1
proof end;

theorem Th16: :: TAYLOR_1:16
( exp is one-to-one & exp is_differentiable_on REAL & exp is_differentiable_on [#] REAL & ( for b1 being Real holds diff exp ,b1 = exp . b1 ) & ( for b1 being Real holds 0 < diff exp ,b1 ) & dom exp = REAL & dom exp = [#] REAL & rng exp = right_open_halfline 0 )
proof end;

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

theorem Th17: :: TAYLOR_1:17
( exp " is_differentiable_on dom (exp " ) & ( for b1 being real number st b1 in dom (exp " ) holds
diff (exp " ),b1 = 1 / b1 ) )
proof end;

registration
cluster right_open_halfline 0 -> non empty ;
coherence
not right_open_halfline 0 is empty
proof end;
end;

definition
let c1 be real number ;
func log_ c1 -> PartFunc of REAL , REAL means :Def2: :: TAYLOR_1:def 2
( dom a2 = right_open_halfline 0 & ( for b1 being Element of right_open_halfline 0 holds a2 . b1 = log a1,b1 ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = right_open_halfline 0 & ( for b2 being Element of right_open_halfline 0 holds b1 . b2 = log c1,b2 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b1 . b3 = log c1,b3 ) & dom b2 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b2 . b3 = log c1,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines log_ TAYLOR_1:def 2 :
for b1 being real number
for b2 being PartFunc of REAL , REAL holds
( b2 = log_ b1 iff ( dom b2 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b2 . b3 = log b1,b3 ) ) );

theorem Th18: :: TAYLOR_1:18
( log_ number_e = exp " & log_ number_e is one-to-one & dom (log_ number_e ) = right_open_halfline 0 & rng (log_ number_e ) = REAL & log_ number_e is_differentiable_on right_open_halfline 0 & ( for b1 being Real st b1 > 0 holds
log_ number_e is_differentiable_in b1 ) & ( for b1 being Element of right_open_halfline 0 holds diff (log_ number_e ),b1 = 1 / b1 ) & ( for b1 being Element of right_open_halfline 0 holds 0 < diff (log_ number_e ),b1 ) )
proof end;

theorem Th19: :: TAYLOR_1:19
for b1 being real number
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_in b1 holds
( exp * b2 is_differentiable_in b1 & diff (exp * b2),b1 = (exp . (b2 . b1)) * (diff b2,b1) )
proof end;

theorem Th20: :: TAYLOR_1:20
for b1 being real number
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_in b1 & b2 . b1 > 0 holds
( (log_ number_e ) * b2 is_differentiable_in b1 & diff ((log_ number_e ) * b2),b1 = (diff b2,b1) / (b2 . b1) )
proof end;

definition
let c1 be real number ;
func #R c1 -> PartFunc of REAL , REAL means :Def3: :: TAYLOR_1:def 3
( dom a2 = right_open_halfline 0 & ( for b1 being Element of right_open_halfline 0 holds a2 . b1 = b1 #R a1 ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = right_open_halfline 0 & ( for b2 being Element of right_open_halfline 0 holds b1 . b2 = b2 #R c1 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b1 . b3 = b3 #R c1 ) & dom b2 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b2 . b3 = b3 #R c1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines #R TAYLOR_1:def 3 :
for b1 being real number
for b2 being PartFunc of REAL , REAL holds
( b2 = #R b1 iff ( dom b2 = right_open_halfline 0 & ( for b3 being Element of right_open_halfline 0 holds b2 . b3 = b3 #R b1 ) ) );

theorem Th21: :: TAYLOR_1:21
for b1, b2 being real number st b1 > 0 holds
( #R b2 is_differentiable_in b1 & diff (#R b2),b1 = b2 * (b1 #R (b2 - 1)) )
proof end;

theorem Th22: :: TAYLOR_1:22
for b1, b2 being real number
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_in b1 & b3 . b1 > 0 holds
( (#R b2) * b3 is_differentiable_in b1 & diff ((#R b2) * b3),b1 = (b2 * ((b3 . b1) #R (b2 - 1))) * (diff b3,b1) )
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be Subset of REAL ;
func diff c1,c2 -> Functional_Sequence of REAL , REAL means :Def4: :: TAYLOR_1:def 4
( a3 . 0 = a1 | a2 & ( for b1 being natural number holds a3 . (b1 + 1) = (a3 . b1) `| a2 ) );
existence
ex b1 being Functional_Sequence of REAL , REAL st
( b1 . 0 = c1 | c2 & ( for b2 being natural number holds b1 . (b2 + 1) = (b1 . b2) `| c2 ) )
proof end;
uniqueness
for b1, b2 being Functional_Sequence of REAL , REAL st b1 . 0 = c1 | c2 & ( for b3 being natural number holds b1 . (b3 + 1) = (b1 . b3) `| c2 ) & b2 . 0 = c1 | c2 & ( for b3 being natural number holds b2 . (b3 + 1) = (b2 . b3) `| c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines diff TAYLOR_1:def 4 :
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being Functional_Sequence of REAL , REAL holds
( b3 = diff b1,b2 iff ( b3 . 0 = b1 | b2 & ( for b4 being natural number holds b3 . (b4 + 1) = (b3 . b4) `| b2 ) ) );

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be natural number ;
let c3 be Subset of REAL ;
pred c1 is_differentiable_on c2,c3 means :Def5: :: TAYLOR_1:def 5
for b1 being Nat st b1 <= a2 - 1 holds
(diff a1,a3) . b1 is_differentiable_on a3;
end;

:: deftheorem Def5 defines is_differentiable_on TAYLOR_1:def 5 :
for b1 being PartFunc of REAL , REAL
for b2 being natural number
for b3 being Subset of REAL holds
( b1 is_differentiable_on b2,b3 iff for b4 being Nat st b4 <= b2 - 1 holds
(diff b1,b3) . b4 is_differentiable_on b3 );

theorem Th23: :: TAYLOR_1:23
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being natural number st b1 is_differentiable_on b3,b2 holds
for b4 being natural number st b4 <= b3 holds
b1 is_differentiable_on b4,b2
proof end;

definition
let c1 be PartFunc of REAL , REAL ;
let c2 be Subset of REAL ;
let c3, c4 be real number ;
func Taylor c1,c2,c3,c4 -> Real_Sequence means :Def6: :: TAYLOR_1:def 6
for b1 being natural number holds a5 . b1 = ((((diff a1,a2) . b1) . a3) * ((a4 - a3) |^ b1)) / (b1 ! );
existence
ex b1 being Real_Sequence st
for b2 being natural number holds b1 . b2 = ((((diff c1,c2) . b2) . c3) * ((c4 - c3) |^ b2)) / (b2 ! )
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for b3 being natural number holds b1 . b3 = ((((diff c1,c2) . b3) . c3) * ((c4 - c3) |^ b3)) / (b3 ! ) ) & ( for b3 being natural number holds b2 . b3 = ((((diff c1,c2) . b3) . c3) * ((c4 - c3) |^ b3)) / (b3 ! ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines Taylor TAYLOR_1:def 6 :
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3, b4 being real number
for b5 being Real_Sequence holds
( b5 = Taylor b1,b2,b3,b4 iff for b6 being natural number holds b5 . b6 = ((((diff b1,b2) . b6) . b3) * ((b4 - b3) |^ b6)) / (b6 ! ) );

Lemma28: for b1 being Real ex b2 being PartFunc of REAL , REAL st
( dom b2 = REAL & ( for b3 being Real holds
( b2 . b3 = b1 - b3 & ( for b4 being Real holds
( b2 is_differentiable_in b4 & diff b2,b4 = - 1 ) ) ) ) )
proof end;

Lemma29: for b1 being Nat
for b2, b3 being Real ex b4 being PartFunc of REAL , REAL st
( dom b4 = REAL & ( for b5 being Real holds
( b4 . b5 = (b2 * ((b3 - b5) |^ (b1 + 1))) / ((b1 + 1) ! ) & ( for b6 being Real holds
( b4 is_differentiable_in b6 & diff b4,b6 = - ((b2 * ((b3 - b6) |^ b1)) / (b1 ! )) ) ) ) ) )
proof end;

Lemma30: for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL
for b4 being Real ex b5 being PartFunc of REAL , REAL st
( dom b5 = b3 & ( for b6 being Real st b6 in b3 holds
b5 . b6 = (b2 . b4) - ((Partial_Sums (Taylor b2,b3,b6,b4)) . b1) ) )
proof end;

theorem Th24: :: TAYLOR_1:24
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being Nat st b1 is_differentiable_on b3,b2 holds
for b4, b5 being Real st b4 < b5 & ].b4,b5.[ c= b2 holds
((diff b1,b2) . b3) | ].b4,b5.[ = (diff b1,].b4,b5.[) . b3
proof end;

Lemma32: for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being Nat st b1 is_differentiable_on b3,b2 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b2 & (diff b1,b2) . b3 is_continuous_on [.b4,b5.] & b1 is_differentiable_on b3 + 1,].b4,b5.[ holds
for b6 being PartFunc of REAL , REAL st dom b6 = b2 & ( for b7 being Real st b7 in b2 holds
b6 . b7 = (b1 . b5) - ((Partial_Sums (Taylor b1,b2,b7,b5)) . b3) ) holds
( b6 . b5 = 0 & b6 is_continuous_on [.b4,b5.] & b6 is_differentiable_on ].b4,b5.[ & ( for b7 being Real st b7 in ].b4,b5.[ holds
diff b6,b7 = - (((((diff b1,].b4,b5.[) . (b3 + 1)) . b7) * ((b5 - b7) |^ b3)) / (b3 ! )) ) )
proof end;

Lemma33: for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
ex b6 being PartFunc of REAL , REAL st
( dom b6 = b3 & ( for b7 being Real st b7 in b3 holds
b6 . b7 = (b2 . b5) - ((Partial_Sums (Taylor b2,b3,b7,b5)) . b1) ) & b6 . b5 = 0 & b6 is_continuous_on [.b4,b5.] & b6 is_differentiable_on ].b4,b5.[ & ( for b7 being Real st b7 in ].b4,b5.[ holds
diff b6,b7 = - (((((diff b2,].b4,b5.[) . (b1 + 1)) . b7) * ((b5 - b7) |^ b1)) / (b1 ! )) ) )
proof end;

theorem Th25: :: TAYLOR_1:25
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
for b6 being Real
for b7 being PartFunc of REAL , REAL st dom b7 = REAL & ( for b8 being Real holds b7 . b8 = ((b2 . b5) - ((Partial_Sums (Taylor b2,b3,b8,b5)) . b1)) - ((b6 * ((b5 - b8) |^ (b1 + 1))) / ((b1 + 1) ! )) ) & ((b2 . b5) - ((Partial_Sums (Taylor b2,b3,b4,b5)) . b1)) - ((b6 * ((b5 - b4) |^ (b1 + 1))) / ((b1 + 1) ! )) = 0 holds
( b7 is_differentiable_on ].b4,b5.[ & b7 . b4 = 0 & b7 . b5 = 0 & b7 is_continuous_on [.b4,b5.] & ( for b8 being Real st b8 in ].b4,b5.[ holds
diff b7,b8 = (- (((((diff b2,].b4,b5.[) . (b1 + 1)) . b8) * ((b5 - b8) |^ b1)) / (b1 ! ))) + ((b6 * ((b5 - b8) |^ b1)) / (b1 ! )) ) )
proof end;

theorem Th26: :: TAYLOR_1:26
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL
for b4, b5 being Real ex b6 being Function of REAL , REAL st
for b7 being Real holds b6 . b7 = ((b2 . b4) - ((Partial_Sums (Taylor b2,b3,b7,b4)) . b1)) - ((b5 * ((b4 - b7) |^ (b1 + 1))) / ((b1 + 1) ! ))
proof end;

theorem Th27: :: TAYLOR_1:27
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
ex b6 being Real st
( b6 in ].b4,b5.[ & b2 . b5 = ((Partial_Sums (Taylor b2,b3,b4,b5)) . b1) + (((((diff b2,].b4,b5.[) . (b1 + 1)) . b6) * ((b5 - b4) |^ (b1 + 1))) / ((b1 + 1) ! )) )
proof end;

Lemma37: for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being Nat st b1 is_differentiable_on b3,b2 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b2 & (diff b1,b2) . b3 is_continuous_on [.b4,b5.] & b1 is_differentiable_on b3 + 1,].b4,b5.[ holds
for b6 being PartFunc of REAL , REAL st dom b6 = b2 & ( for b7 being Real st b7 in b2 holds
b6 . b7 = (b1 . b4) - ((Partial_Sums (Taylor b1,b2,b7,b4)) . b3) ) holds
( b6 . b4 = 0 & b6 is_continuous_on [.b4,b5.] & b6 is_differentiable_on ].b4,b5.[ & ( for b7 being Real st b7 in ].b4,b5.[ holds
diff b6,b7 = - (((((diff b1,].b4,b5.[) . (b3 + 1)) . b7) * ((b4 - b7) |^ b3)) / (b3 ! )) ) )
proof end;

Lemma38: for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
ex b6 being PartFunc of REAL , REAL st
( dom b6 = b3 & ( for b7 being Real st b7 in b3 holds
b6 . b7 = (b2 . b4) - ((Partial_Sums (Taylor b2,b3,b7,b4)) . b1) ) & b6 . b4 = 0 & b6 is_continuous_on [.b4,b5.] & b6 is_differentiable_on ].b4,b5.[ & ( for b7 being Real st b7 in ].b4,b5.[ holds
diff b6,b7 = - (((((diff b2,].b4,b5.[) . (b1 + 1)) . b7) * ((b4 - b7) |^ b1)) / (b1 ! )) ) )
proof end;

theorem Th28: :: TAYLOR_1:28
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
for b6 being Real
for b7 being PartFunc of REAL , REAL st dom b7 = REAL & ( for b8 being Real holds b7 . b8 = ((b2 . b4) - ((Partial_Sums (Taylor b2,b3,b8,b4)) . b1)) - ((b6 * ((b4 - b8) |^ (b1 + 1))) / ((b1 + 1) ! )) ) & ((b2 . b4) - ((Partial_Sums (Taylor b2,b3,b5,b4)) . b1)) - ((b6 * ((b4 - b5) |^ (b1 + 1))) / ((b1 + 1) ! )) = 0 holds
( b7 is_differentiable_on ].b4,b5.[ & b7 . b5 = 0 & b7 . b4 = 0 & b7 is_continuous_on [.b4,b5.] & ( for b8 being Real st b8 in ].b4,b5.[ holds
diff b7,b8 = (- (((((diff b2,].b4,b5.[) . (b1 + 1)) . b8) * ((b4 - b8) |^ b1)) / (b1 ! ))) + ((b6 * ((b4 - b8) |^ b1)) / (b1 ! )) ) )
proof end;

theorem Th29: :: TAYLOR_1:29
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3 being Subset of REAL st b2 is_differentiable_on b1,b3 holds
for b4, b5 being Real st b4 < b5 & [.b4,b5.] c= b3 & (diff b2,b3) . b1 is_continuous_on [.b4,b5.] & b2 is_differentiable_on b1 + 1,].b4,b5.[ holds
ex b6 being Real st
( b6 in ].b4,b5.[ & b2 . b4 = ((Partial_Sums (Taylor b2,b3,b5,b4)) . b1) + (((((diff b2,].b4,b5.[) . (b1 + 1)) . b6) * ((b4 - b5) |^ (b1 + 1))) / ((b1 + 1) ! )) )
proof end;

theorem Th30: :: TAYLOR_1:30
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being open Subset of REAL st b3 c= b2 holds
for b4 being Nat st b1 is_differentiable_on b4,b2 holds
((diff b1,b2) . b4) | b3 = (diff b1,b3) . b4
proof end;

theorem Th31: :: TAYLOR_1:31
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being open Subset of REAL st b3 c= b2 holds
for b4 being natural number st b1 is_differentiable_on b4 + 1,b2 holds
b1 is_differentiable_on b4 + 1,b3
proof end;

theorem Th32: :: TAYLOR_1:32
for b1 being PartFunc of REAL , REAL
for b2 being Subset of REAL
for b3 being Real st b3 in b2 holds
for b4 being Nat holds b1 . b3 = (Partial_Sums (Taylor b1,b2,b3,b3)) . b4
proof end;

theorem Th33: :: TAYLOR_1:33
for b1 being Nat
for b2 being PartFunc of REAL , REAL
for b3, b4 being Real st 0 < b4 & b2 is_differentiable_on b1 + 1,].(b3 - b4),(b3 + b4).[ holds
for b5 being Real st b5 in ].(b3 - b4),(b3 + b4).[ holds
ex b6 being Real st
( 0 < b6 & b6 < 1 & b2 . b5 = ((Partial_Sums (Taylor b2,].(b3 - b4),(b3 + b4).[,b3,b5)) . b1) + (((((diff b2,].(b3 - b4),(b3 + b4).[) . (b1 + 1)) . (b3 + (b6 * (b5 - b3)))) * ((b5 - b3) |^ (b1 + 1))) / ((b1 + 1) ! )) )
proof end;