definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Subset of REAL ;
let c₃ be real number ;
func Maclaurin c₁,c₂,c₃ -> Real_Sequence equals :: TAYLOR_2:def 1
Taylor a₁,a₂,0,a₃;
coherence ;

end;

for b₁ being Nat
for b₂ being PartFunc of REAL , REAL
for b₃ being Real st 0 < b₃ & b₂ is_differentiable_on b₁ + 1,].(- b₃),b₃.[ holds
for b₄ being Real st b₄ in ].(- b₃),b₃.[ holds
ex b₅ being Real st
( 0 < b₅ & b₅ < 1 & b₂ . b₄ = ((Partial_Sums (Maclaurin b₂,].(- b₃),b₃.[,b₄)) . b₁) + (((((diff b₂,].(- b₃),b₃.[) . (b₁ + 1)) . (b₅ * b₄)) * (b₄ |^ (b₁ + 1))) / ((b₁ + 1) ! )) )

for b₁ being Nat
for b₂ being PartFunc of REAL , REAL
for b₃, b₄ being Real st 0 < b₄ & b₂ is_differentiable_on b₁ + 1,].(b₃ - b₄),(b₃ + b₄).[ holds
for b₅ being Real st b₅ in ].(b₃ - b₄),(b₃ + b₄).[ holds
ex b₆ being Real st
( 0 < b₆ & b₆ < 1 & abs ((b₂ . b₅) - ((Partial_Sums (Taylor b₂,].(b₃ - b₄),(b₃ + b₄).[,b₃,b₅)) . b₁)) = abs (((((diff b₂,].(b₃ - b₄),(b₃ + b₄).[) . (b₁ + 1)) . (b₃ + (b₆ * (b₅ - b₃)))) * ((b₅ - b₃) |^ (b₁ + 1))) / ((b₁ + 1) ! )) )

for b₁ being Nat
for b₂ being PartFunc of REAL , REAL
for b₃ being Real st 0 < b₃ & b₂ is_differentiable_on b₁ + 1,].(- b₃),b₃.[ holds
for b₄ being Real st b₄ in ].(- b₃),b₃.[ holds
ex b₅ being Real st
( 0 < b₅ & b₅ < 1 & abs ((b₂ . b₄) - ((Partial_Sums (Maclaurin b₂,].(- b₃),b₃.[,b₄)) . b₁)) = abs (((((diff b₂,].(- b₃),b₃.[) . (b₁ + 1)) . (b₅ * b₄)) * (b₄ |^ (b₁ + 1))) / ((b₁ + 1) ! )) )

for b₁ being Real holds
( exp `| ].(- b₁),b₁.[ = exp | ].(- b₁),b₁.[ & dom (exp | ].(- b₁),b₁.[) = ].(- b₁),b₁.[ )

for b₁ being Nat
for b₂ being Real holds (diff exp ,].(- b₂),b₂.[) . b₁ = exp | ].(- b₂),b₂.[

for b₁ being Nat
for b₂, b₃ being Real st b₃ in ].(- b₂),b₂.[ holds
((diff exp ,].(- b₂),b₂.[) . b₁) . b₃ = exp . b₃

for b₁ being Nat
for b₂, b₃ being Real st 0 < b₂ holds
(Maclaurin exp ,].(- b₂),b₂.[,b₃) . b₁ = (b₃ |^ b₁) / (b₁ ! )

for b₁ being Nat
for b₂, b₃, b₄ being Real st b₃ in ].(- b₂),b₂.[ & 0 < b₄ & b₄ < 1 holds
abs (((((diff exp ,].(- b₂),b₂.[) . (b₁ + 1)) . (b₄ * b₃)) * (b₃ |^ (b₁ + 1))) / ((b₁ + 1) ! )) <= ((abs (exp . (b₄ * b₃))) * ((abs b₃) |^ (b₁ + 1))) / ((b₁ + 1) ! )

for b₁ being Real
for b₂ being Nat holds exp is_differentiable_on b₂,].(- b₁),b₁.[

for b₁ being Real st 0 < b₁ holds
ex b₂, b₃ being Real st
( 0 <= b₂ & 0 <= b₃ & ( for b₄ being Nat
for b₅, b₆ being Real st b₅ in ].(- b₁),b₁.[ & 0 < b₆ & b₆ < 1 holds
abs (((((diff exp ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) <= (b₂ * (b₃ |^ b₄)) / (b₄ ! ) ) )

for b₁, b₂ being Real st b₁ >= 0 & b₂ >= 0 holds
for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅ being Nat st b₄ <= b₅ holds
(b₁ * (b₂ |^ b₅)) / (b₅ ! ) < b₃

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
for b₅, b₆ being Real st b₅ in ].(- b₁),b₁.[ & 0 < b₆ & b₆ < 1 holds
abs (((((diff exp ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) < b₂

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
for b₅ being real number st b₅ in ].(- b₁),b₁.[ holds
abs ((exp . b₅) - ((Partial_Sums (Maclaurin exp ,].(- b₁),b₁.[,b₅)) . b₄)) < b₂

for b₁ being Real holds b₁ ExpSeq is absolutely_summable

for b₁, b₂ being Real st 0 < b₁ holds
( Maclaurin exp ,].(- b₁),b₁.[,b₂ = b₂ ExpSeq & Maclaurin exp ,].(- b₁),b₁.[,b₂ is absolutely_summable & exp . b₂ = Sum (Maclaurin exp ,].(- b₁),b₁.[,b₂) )

for b₁ being PartFunc of REAL , REAL
for b₂ being Subset of REAL st b₁ is_differentiable_on b₂ holds
(- b₁) `| b₂ = - (b₁ `| b₂)

for b₁ being Nat
for b₂, b₃ being Real st b₂ > 0 holds
( (Maclaurin sin ,].(- b₂),b₂.[,b₃) . (2 * b₁) = 0 & (Maclaurin sin ,].(- b₂),b₂.[,b₃) . ((2 * b₁) + 1) = (((- 1) |^ b₁) * (b₃ |^ ((2 * b₁) + 1))) / (((2 * b₁) + 1) ! ) & (Maclaurin cos ,].(- b₂),b₂.[,b₃) . (2 * b₁) = (((- 1) |^ b₁) * (b₃ |^ (2 * b₁))) / ((2 * b₁) ! ) & (Maclaurin cos ,].(- b₂),b₂.[,b₃) . ((2 * b₁) + 1) = 0 )

for b₁ being Real
for b₂ being Nat holds
( sin is_differentiable_on b₂,].(- b₁),b₁.[ & cos is_differentiable_on b₂,].(- b₁),b₁.[ )

for b₁ being Real st b₁ > 0 holds
ex b₂, b₃ being Real st
( b₂ >= 0 & b₃ >= 0 & ( for b₄ being Nat
for b₅, b₆ being Real st b₅ in ].(- b₁),b₁.[ & 0 < b₆ & b₆ < 1 holds
( abs (((((diff sin ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) <= (b₂ * (b₃ |^ b₄)) / (b₄ ! ) & abs (((((diff cos ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) <= (b₂ * (b₃ |^ b₄)) / (b₄ ! ) ) ) )

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
for b₅, b₆ being Real st b₅ in ].(- b₁),b₁.[ & 0 < b₆ & b₆ < 1 holds
( abs (((((diff sin ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) < b₂ & abs (((((diff cos ,].(- b₁),b₁.[) . b₄) . (b₆ * b₅)) * (b₅ |^ b₄)) / (b₄ ! )) < b₂ )

for b₁, b₂ being Real st 0 < b₁ & 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
for b₅ being real number st b₅ in ].(- b₁),b₁.[ holds
( abs ((sin . b₅) - ((Partial_Sums (Maclaurin sin ,].(- b₁),b₁.[,b₅)) . b₄)) < b₂ & abs ((cos . b₅) - ((Partial_Sums (Maclaurin cos ,].(- b₁),b₁.[,b₅)) . b₄)) < b₂ )

for b₁, b₂ being Real
for b₃ being Nat st 0 < b₁ holds
( (Partial_Sums (Maclaurin sin ,].(- b₁),b₁.[,b₂)) . ((2 * b₃) + 1) = (Partial_Sums (b₂ P_sin )) . b₃ & (Partial_Sums (Maclaurin cos ,].(- b₁),b₁.[,b₂)) . ((2 * b₃) + 1) = (Partial_Sums (b₂ P_cos )) . b₃ )

for b₁, b₂ being Real
for b₃ being Nat st 0 < b₁ & b₃ > 0 holds
( (Partial_Sums (Maclaurin sin ,].(- b₁),b₁.[,b₂)) . (2 * b₃) = (Partial_Sums (b₂ P_sin )) . (b₃ - 1) & (Partial_Sums (Maclaurin cos ,].(- b₁),b₁.[,b₂)) . (2 * b₃) = (Partial_Sums (b₂ P_cos )) . b₃ )

for b₁, b₂ being Real
for b₃ being Nat st 0 < b₁ holds
(Partial_Sums (Maclaurin cos ,].(- b₁),b₁.[,b₂)) . (2 * b₃) = (Partial_Sums (b₂ P_cos )) . b₃

for b₁, b₂ being Real st b₁ > 0 holds
( Partial_Sums (Maclaurin sin ,].(- b₁),b₁.[,b₂) is convergent & sin . b₂ = Sum (Maclaurin sin ,].(- b₁),b₁.[,b₂) & Partial_Sums (Maclaurin cos ,].(- b₁),b₁.[,b₂) is convergent & cos . b₂ = Sum (Maclaurin cos ,].(- b₁),b₁.[,b₂) )