begin
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ex
r,
r1 being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r1 : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
r1 : ( ( ) (
V11()
real ext-real )
Real)
<= f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0,
r being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) holds
( (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
r : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) implies
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) & (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
r : ( ( ) (
V11()
real ext-real )
Real)
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) implies
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) & (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
r : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) implies
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) & (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
r : ( ( ) (
V11()
real ext-real )
Real)
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) implies
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
non-decreasing &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
non-increasing & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
increasing &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
decreasing & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
non-increasing &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
non-decreasing & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
decreasing &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
increasing & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below & not
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
(dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
(dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_left_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_right_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim_left (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
= lim_right (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim_left (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim_right (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_left_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_right_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim_left (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
= lim_right (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim_left (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim_right (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0,
r being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) holds
(
r : ( ( ) (
V11()
real ext-real )
Real)
(#) f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(r : ( ( ) ( V11() real ext-real ) Real) (#) f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= r : ( ( ) (
V11()
real ext-real )
Real)
* (lim (f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
+ (lim (f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
- f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
- (lim (f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
" {0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V69() V70() V71() V72() V73() V74() V85() V86() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V69() V70() V71() V72() V73() V74() V75() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) } : ( ( ) (
V69()
V70()
V71()
V72()
V73()
V74() )
set ) : ( ( ) ( )
set )
= {} : ( ( ) ( )
set ) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
" : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g1 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g2 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
" : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
* (lim (f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
/ f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= (lim (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real)
/ (lim (f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ,x0 : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom (f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
| (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim (
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) & ( (
(dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) &
(dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) or (
(dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) &
(dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2,
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim (
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) &
].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= ((dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) set ) /\ (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( ) set ) ) : ( ( ) ( )
set )
/\ (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set ) : ( ( ) ( )
set ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in ].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
\/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
(
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f1,
f2 being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( (
(dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) or (
(dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) )
c= (dom f1 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f2 : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) ) ) holds
lim (
f1 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
<= lim (
f2 : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) or
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g1 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g2 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) holds
(
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
(f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ^) : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g1 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g2 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
<= f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
r1,
r2 being ( ( ) (
V11()
real ext-real )
Real) st
r1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) holds
ex
g1,
g2 being ( ( ) (
V11()
real ext-real )
Real) st
(
r1 : ( ( ) (
V11()
real ext-real )
Real)
< g1 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
< x0 : ( ( ) (
V11()
real ext-real )
Real) &
g1 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
< r2 : ( ( ) (
V11()
real ext-real )
Real) &
x0 : ( ( ) (
V11()
real ext-real )
Real)
< g2 : ( ( ) (
V11()
real ext-real )
Real) &
g2 : ( ( ) (
V11()
real ext-real )
Real)
in dom f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( ( ) ( )
set ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g1 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g2 : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
<= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to+infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
x0 being ( ( ) (
V11()
real ext-real )
Real)
for
f being ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
is_convergent_in x0 : ( ( ) (
V11()
real ext-real )
Real) &
lim (
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,) ,
x0 : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) (
V11()
real ext-real )
Real)
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) & ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) & ( for
g being ( ( ) (
V11()
real ext-real )
Real) st
g : ( ( ) (
V11()
real ext-real )
Real)
in (dom f : ( ( V21() ) ( Relation-like REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -defined REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) -valued V21() complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( ( ) ( )
set )
/\ (].(x0 : ( ( ) ( V11() real ext-real ) Real) - r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) ,x0 : ( ( ) ( V11() real ext-real ) Real) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) \/ ].x0 : ( ( ) ( V11() real ext-real ) Real) ,(x0 : ( ( ) ( V11() real ext-real ) Real) + r : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) .[ : ( ( ) ( V69() V70() V71() ) Element of K6(REAL : ( ( ) ( non empty V49() V69() V70() V71() V75() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) (
V69()
V70()
V71() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
. g : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) )
< 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative V69()
V70()
V71()
V72()
V73()
V74()
V85()
V86() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal V69()
V70()
V71()
V72()
V73()
V74()
V75() )
Element of
K6(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) ( )
set ) ) ) ) ) holds
f : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
V21() ) (
Relation-like REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-defined REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set )
-valued V21()
complex-valued ext-real-valued real-valued )
Element of
K6(
K7(
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ,
REAL : ( ( ) ( non
empty V49()
V69()
V70()
V71()
V75() )
set ) ) : ( ( ) (
complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
is_divergent_to-infty_in x0 : ( ( ) (
V11()
real ext-real )
Real) ;