:: TAYLOR_1 semantic presentation

begin

definition
let q be ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) ;
func #Z q -> ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) means :: TAYLOR_1:def 1
 for x being ( ( real ) ( V22() real ext-real ) number ) holds it : ( ( ) ( V22() ) Element of COMPLEX : ( ( ) ( non empty V69() V80() V86() ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = x : ( ( real ) ( V22() real ext-real ) number ) #Z q : ( ( V22() ) ( V22() ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: TAYLOR_1:1
for x being ( ( real ) ( V22() real ext-real ) number )
for m, n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) holds x : ( ( real ) ( V22() real ext-real ) number ) #Z (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) + m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) set ) : ( ( ) ( V22() real ext-real ) set ) = (x : ( ( real ) ( V22() real ext-real ) number ) #Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( ) ( V22() real ext-real ) set ) * (x : ( ( real ) ( V22() real ext-real ) number ) #Z m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: TAYLOR_1:2
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat)
for x being ( ( real ) ( V22() real ext-real ) number ) holds
( #Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) is_differentiable_in x : ( ( real ) ( V22() real ext-real ) number ) & diff ((#Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) * (x : ( ( real ) ( V22() real ext-real ) number ) #Z (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ) ;

theorem :: TAYLOR_1:3
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat)
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
( (#Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & diff (((#Z n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) * ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #Z (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x0 : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

theorem :: TAYLOR_1:4
for x being ( ( real ) ( V22() real ext-real ) number ) holds exp_R (- x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( V22() ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) / (exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ;

theorem :: TAYLOR_1:5
for i being ( ( integer ) ( V22() real ext-real integer non irrational ) Integer)
for x being ( ( real ) ( V22() real ext-real ) number ) holds (exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) #R (1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) / i : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) ) : ( ( ) ( V22() real ext-real non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R (x : ( ( real ) ( V22() real ext-real ) number ) / i : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) ) : ( ( ) ( V22() real ext-real ) Element of COMPLEX : ( ( ) ( non empty V69() V80() V86() ) set ) ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: TAYLOR_1:6
for x being ( ( real ) ( V22() real ext-real ) number )
for m, n being ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) holds (exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) #R (m : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) / n : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) ) : ( ( ) ( V22() real ext-real non irrational ) Element of COMPLEX : ( ( ) ( non empty V69() V80() V86() ) set ) ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R ((m : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) / n : ( ( integer ) ( V22() real ext-real integer non irrational ) Integer) ) : ( ( ) ( V22() real ext-real non irrational ) Element of COMPLEX : ( ( ) ( non empty V69() V80() V86() ) set ) ) * x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: TAYLOR_1:7
for x being ( ( real ) ( V22() real ext-real ) number )
for q being ( ( non irrational ) ( V22() real ext-real non irrational ) Rational) holds (exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) #Q q : ( ( non irrational ) ( V22() real ext-real non irrational ) Rational) : ( ( ) ( V22() real ext-real ) set ) = exp_R (q : ( ( non irrational ) ( V22() real ext-real non irrational ) Rational) * x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: TAYLOR_1:8
for x, p being ( ( real ) ( V22() real ext-real ) number ) holds (exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) #R p : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R (p : ( ( real ) ( V22() real ext-real ) number ) * x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ;

theorem :: TAYLOR_1:9
for x being ( ( real ) ( V22() real ext-real ) number ) holds
( (exp_R 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) & (exp_R 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) to_power x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) & number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) to_power x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) & number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) set ) ) ;

theorem :: TAYLOR_1:10
for x being ( ( real ) ( V22() real ext-real ) number ) holds
( (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) & (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) to_power x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) & number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) to_power x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) & number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #R x : ( ( real ) ( V22() real ext-real ) number ) : ( ( real ) ( V22() real ext-real ) set ) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

theorem :: TAYLOR_1:11
number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) > 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: TAYLOR_1:12
for x being ( ( real ) ( V22() real ext-real ) number ) holds log (number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(exp_R x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) set ) ) : ( ( real ) ( V22() real ext-real ) set ) = x : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: TAYLOR_1:13
for x being ( ( real ) ( V22() real ext-real ) number ) holds log (number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = x : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: TAYLOR_1:14
for y being ( ( real ) ( V22() real ext-real ) number ) st y : ( ( real ) ( V22() real ext-real ) number ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
exp_R (log (number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,y : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) = y : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: TAYLOR_1:15
for y being ( ( real ) ( V22() real ext-real ) number ) st y : ( ( real ) ( V22() real ext-real ) number ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . (log (number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,y : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = y : ( ( real ) ( V22() real ext-real ) number ) ;

theorem :: TAYLOR_1:16
( exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is one-to-one & exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) & exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on [#] REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) : ( ( ) ( closed open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) holds diff (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < diff (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) & dom exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = [#] REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) : ( ( ) ( closed open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & dom exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = [#] REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) : ( ( ) ( closed open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & rng exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ;

registration
cluster exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) -> Function-like one-to-one quasi_total ;
end;

theorem :: TAYLOR_1:17
( exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) " : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on dom (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( real ) ( V22() real ext-real ) number ) st x : ( ( real ) ( V22() real ext-real ) number ) in dom (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
diff ((exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ") : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) / x : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ) ;

registration
cluster right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) -> non empty ;
end;

definition
let a be ( ( real ) ( V22() real ext-real ) number ) ;
func log_ a -> ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) means :: TAYLOR_1:def 2
( dom it : ( ( ) ( ) set ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for d being ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . d : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = log (a : ( ( ) ( ) set ) ,d : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( real ) ( V22() real ext-real ) set ) ) );
end;

definition
func ln -> ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) equals :: TAYLOR_1:def 3
 log_ number_e : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ;
end;

theorem :: TAYLOR_1:18
( ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) = exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) " : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) & ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is one-to-one & dom ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & rng ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) & ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) & ( for x being ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds diff (ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) / x : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) & ( for x being ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < diff (ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ) ;

theorem :: TAYLOR_1:19
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) holds
( exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & diff ((exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (exp_R : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like one-to-one non empty total quasi_total V33() V34() V35() continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x0 : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

theorem :: TAYLOR_1:20
for x0 being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & diff ((ln : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x0 : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

definition
let p be ( ( real ) ( V22() real ext-real ) number ) ;
func #R p -> ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) means :: TAYLOR_1:def 4
( dom it : ( ( ) ( ) set ) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for d being ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds it : ( ( ) ( ) set ) . d : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = d : ( ( ) ( V22() real ext-real ) Element of right_open_halfline 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) #R p : ( ( ) ( ) set ) : ( ( real ) ( V22() real ext-real ) set ) ) );
end;

theorem :: TAYLOR_1:21
for x, p being ( ( real ) ( V22() real ext-real ) number ) st x : ( ( real ) ( V22() real ext-real ) number ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( #R p : ( ( real ) ( V22() real ext-real ) number ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x : ( ( real ) ( V22() real ext-real ) number ) & diff ((#R p : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = p : ( ( real ) ( V22() real ext-real ) number ) * (x : ( ( real ) ( V22() real ext-real ) number ) #R (p : ( ( real ) ( V22() real ext-real ) number ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( real ) ( V22() real ext-real ) set ) : ( ( ) ( V22() real ext-real ) set ) ) ;

theorem :: TAYLOR_1:22
for x0, p being ( ( real ) ( V22() real ext-real ) number )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) > 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( (#R p : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_in x0 : ( ( real ) ( V22() real ext-real ) number ) & diff (((#R p : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) * f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (p : ( ( real ) ( V22() real ext-real ) number ) * ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x0 : ( ( real ) ( V22() real ext-real ) number ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) #R (p : ( ( real ) ( V22() real ext-real ) number ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x0 : ( ( real ) ( V22() real ext-real ) number ) )) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

begin

definition
let f be ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ;
let Z be ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ;
func diff (f,Z) -> ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) means :: TAYLOR_1:def 5
( it : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) . 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) = f : ( ( ) ( ) set ) | Z : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) & ( for i being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) holds it : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) . (i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) = (it : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) . i : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( ) ( ) set ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ) );
end;

definition
let f be ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ;
let n be ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ;
let Z be ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ;
pred f is_differentiable_on n,Z means :: TAYLOR_1:def 6
 for i being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( ) set ) - 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) holds
(diff (f : ( ( ) ( ) set ) ,Z : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ;
end;

theorem :: TAYLOR_1:23
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for m being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) st m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) <= n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on m : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ;

definition
let f be ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ;
let Z be ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ;
let a, b be ( ( real ) ( V22() real ext-real ) number ) ;
func Taylor (f,Z,a,b) -> ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) means :: TAYLOR_1:def 7
 for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) holds it : ( ( Function-like ) ( V1() V4(f : ( ( ) ( ) set ) ) V5(a : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) V5( RAT : ( ( ) ( non empty V69() V80() V81() V82() V83() V86() ) set ) ) Function-like V33() V34() V35() V36() ) Element of K19(K20(f : ( ( ) ( ) set ) ,a : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V5( RAT : ( ( ) ( non empty V69() V80() V81() V82() V83() V86() ) set ) ) V5( INT : ( ( ) ( non empty V69() V80() V81() V82() V83() V84() V86() ) set ) ) V33() V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) : ( ( ) ( V22() real ext-real non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((((diff (f : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . a : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((b : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) set ) - a : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real integer non irrational ) set ) |^ n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) ) : ( ( ) ( V22() real ext-real ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ;
end;

theorem :: TAYLOR_1:24
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st a : ( ( ) ( V22() real ext-real ) Real) < b : ( ( ) ( V22() real ext-real ) Real) & ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) = (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: TAYLOR_1:25
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st a : ( ( ) ( V22() real ext-real ) Real) < b : ( ( ) ( V22() real ext-real ) Real) & [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) & ((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
for l being ( ( ) ( V22() real ext-real ) Real)
for g being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st dom g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = [#] REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) : ( ( ) ( closed open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) holds g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((l : ( ( ) ( V22() real ext-real ) Real) * ((b : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) & ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((l : ( ( ) ( V22() real ext-real ) Real) * ((b : ( ( ) ( V22() real ext-real ) Real) - a : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . a : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (- (((((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((b : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) + ((l : ( ( ) ( V22() real ext-real ) Real) * ((b : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ) ;

theorem :: TAYLOR_1:26
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for b, l being ( ( ) ( V22() real ext-real ) Real) ex g being ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) st
for x being ( ( ) ( V22() real ext-real ) Real) holds g : ( ( Function-like quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Function of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) , REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((l : ( ( ) ( V22() real ext-real ) Real) * ((b : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ;

theorem :: TAYLOR_1:27
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st a : ( ( ) ( V22() real ext-real ) Real) < b : ( ( ) ( V22() real ext-real ) Real) & [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) & ((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
ex c being ( ( ) ( V22() real ext-real ) Real) st
( c : ( ( ) ( V22() real ext-real ) Real) in ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) + (((((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((b : ( ( ) ( V22() real ext-real ) Real) - a : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

theorem :: TAYLOR_1:28
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st a : ( ( ) ( V22() real ext-real ) Real) < b : ( ( ) ( V22() real ext-real ) Real) & [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) & ((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
for l being ( ( ) ( V22() real ext-real ) Real)
for g being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) st dom g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) = [#] REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) : ( ( ) ( closed open V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V22() real ext-real ) Real) holds g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . a : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ,a : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((l : ( ( ) ( V22() real ext-real ) Real) * ((a : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) & ((f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . a : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,b : ( ( ) ( V22() real ext-real ) Real) ,a : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) - ((l : ( ( ) ( V22() real ext-real ) Real) * ((a : ( ( ) ( V22() real ext-real ) Real) - b : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds
( g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . b : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . a : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) & g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & ( for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
diff (g : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (- (((((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((a : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) + ((l : ( ( ) ( V22() real ext-real ) Real) * ((a : ( ( ) ( V22() real ext-real ) Real) - x : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ) ;

theorem :: TAYLOR_1:29
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for a, b being ( ( ) ( V22() real ext-real ) Real) st a : ( ( ) ( V22() real ext-real ) Real) < b : ( ( ) ( V22() real ext-real ) Real) & [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) & ((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | [.a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .] : ( ( ) ( closed V80() V81() V82() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) is continuous & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
ex c being ( ( ) ( V22() real ext-real ) Real) st
( c : ( ( ) ( V22() real ext-real ) Real) in ].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . a : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,b : ( ( ) ( V22() real ext-real ) Real) ,a : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) + (((((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].a : ( ( ) ( V22() real ext-real ) Real) ,b : ( ( ) ( V22() real ext-real ) Real) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . c : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((a : ( ( ) ( V22() real ext-real ) Real) - b : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;

theorem :: TAYLOR_1:30
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for Z1 being ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z1 : ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) | Z1 : ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) = (diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z1 : ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: TAYLOR_1:31
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for Z1 being ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) st Z1 : ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for n being ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) st f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( natural ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational ) Nat) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,Z1 : ( ( open ) ( open V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ;

theorem :: TAYLOR_1:32
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for Z being ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) )
for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) holds
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) holds f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = (Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,Z : ( ( ) ( V80() V81() V82() ) Subset of ( ( ) ( ) set ) ) ,x : ( ( ) ( V22() real ext-real ) Real) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ;

theorem :: TAYLOR_1:33
for n being ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )
for f being ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,)
for x0, r being ( ( ) ( V22() real ext-real ) Real) st ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) c= dom f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) : ( ( ) ( V80() V81() V82() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) & 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < r : ( ( ) ( V22() real ext-real ) Real) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) is_differentiable_on n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ,].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
for x being ( ( ) ( V22() real ext-real ) Real) st x : ( ( ) ( V22() real ext-real ) Real) in ].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) holds
ex s being ( ( ) ( V22() real ext-real ) Real) st
( 0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V86() V97() V100() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) < s : ( ( ) ( V22() real ext-real ) Real) & s : ( ( ) ( V22() real ext-real ) Real) < 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) & f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) . x : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) = ((Partial_Sums (Taylor (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,x0 : ( ( ) ( V22() real ext-real ) Real) ,x : ( ( ) ( V22() real ext-real ) Real) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Real_Sequence) ) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like non empty total quasi_total V33() V34() V35() ) Element of K19(K20(NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) + (((((diff (f : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) PartFunc of ,) ,].(x0 : ( ( ) ( V22() real ext-real ) Real) - r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ,(x0 : ( ( ) ( V22() real ext-real ) Real) + r : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) .[ : ( ( ) ( open V80() V81() V82() V95() V96() V100() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( Function-like quasi_total ) ( V1() V4( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) V5( PFuncs (REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total quasi_total ) Functional_Sequence of ( ( ) ( functional non empty ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( Function-like ) ( V1() V4( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) V5( REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) Function-like V33() V34() V35() ) Element of K19(K20(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ,REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V33() V34() V35() ) set ) ) : ( ( ) ( ) set ) ) . (x0 : ( ( ) ( V22() real ext-real ) Real) + (s : ( ( ) ( V22() real ext-real ) Real) * (x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) * ((x : ( ( ) ( V22() real ext-real ) Real) - x0 : ( ( ) ( V22() real ext-real ) Real) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) |^ (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) / ((n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative integer non irrational V80() V81() V82() V83() V84() V85() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational V80() V81() V82() V83() V84() V85() V95() V97() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V80() V81() V82() V83() V84() V85() V86() V95() V97() ) Element of K19(REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( ) set ) ) ) !) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative integer non irrational ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty V69() V80() V81() V82() V86() V97() V98() V100() ) set ) ) ) ;