begin
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
G being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
rng (F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) + G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
c= (rng F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ (rng G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
G being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
sup (F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) + G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
<= (sup F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
+ (sup G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
G being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(inf F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
+ (inf G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal)
<= inf (F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) + G : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b3 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
rng (- F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
= - (rng F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(
inf (- F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
= - (sup F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal) &
sup (- F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
= - (inf F : ( ( Function-like V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) -valued Function-like non empty total V18(b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ext-real-valued ) Function of b1 : ( ( non empty ) ( non empty ) set ) ,b2 : ( ( non empty ) ( non empty ext-real-membered ) Subset of ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded iff (
sup F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
< +infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) &
-infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
< inf F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_above iff
- F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_below ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_below iff
- F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_above ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) holds
(
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded iff
- F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined - b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
- b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
(
inf F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
<= F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
R_eal) &
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real )
R_eal)
<= sup F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) st
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
c= REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) holds
(
F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded iff (
inf F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
in REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) &
sup F : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
in REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F1 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
F2 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) st
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_above &
F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_above holds
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
+ F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_above ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F1 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
F2 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) st
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_below &
F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_below holds
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
+ F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded_below ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
Y,
Z being ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
for
F1 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Y : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
for
F2 being ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
X : ( ( non
empty ) ( non
empty )
set ) ,
Z : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) st
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded &
F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded holds
F1 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
+ F2 : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) : ( (
Function-like V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
-valued Function-like non
empty total V18(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) )
ext-real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
b2 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) )
+ b3 : ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) : ( ( ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) is
bounded ;
theorem
(
incl NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set )
-valued NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-valued RAT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered V46() )
set )
-valued INT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered integer-membered V46() )
set )
-valued Function-like one-to-one non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) )
complex-valued ext-real-valued real-valued natural-valued )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) &
incl NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set )
-valued NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-valued RAT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered V46() )
set )
-valued INT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered integer-membered V46() )
set )
-valued Function-like one-to-one non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) )
complex-valued ext-real-valued real-valued natural-valued )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
one-to-one &
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
= rng (incl NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set )
-valued NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-valued RAT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered V46() )
set )
-valued INT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered integer-membered V46() )
set )
-valued Function-like one-to-one non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) )
complex-valued ext-real-valued real-valued natural-valued )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) &
rng (incl NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set )
-valued NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-valued RAT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered V46() )
set )
-valued INT : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered rational-membered integer-membered V46() )
set )
-valued Function-like one-to-one non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) )
complex-valued ext-real-valued real-valued natural-valued )
Element of
K19(
K20(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) is ( ( non
empty ) ( non
empty ext-real-membered )
Subset of ( ( ) ( )
set ) ) ) ;
definition
let IT be ( ( ) ( )
set ) ;
end;
theorem
for
D being ( ( non
empty countable nonnegative ) ( non
empty ext-real-membered countable nonnegative )
Pos_Denum_Set_of_R_EAL)
for
N being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Num of
D : ( ( non
empty countable nonnegative ) ( non
empty ext-real-membered countable nonnegative )
Pos_Denum_Set_of_R_EAL) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(
(Ser (D : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ,N : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Num of b1 : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ) )) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= (Ser (D : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ,N : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Num of b1 : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ) )) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) &
0. : ( ( ) (
ext-real )
R_eal)
<= (Ser (D : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ,N : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Num of b1 : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ) )) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ) ;
theorem
for
D being ( ( non
empty countable nonnegative ) ( non
empty ext-real-membered countable nonnegative )
Pos_Denum_Set_of_R_EAL)
for
N being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Num of
D : ( ( non
empty countable nonnegative ) ( non
empty ext-real-membered countable nonnegative )
Pos_Denum_Set_of_R_EAL) )
for
n,
m being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(Ser (D : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ,N : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Num of b1 : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ) )) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= (Ser (D : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ,N : ( ( ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Num of b1 : ( ( non empty countable nonnegative ) ( non empty ext-real-membered countable nonnegative ) Pos_Denum_Set_of_R_EAL) ) )) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ;
definition
let F be ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ;
func Ser F -> ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
means
for
N being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Num of
rng F : ( ( ) ( )
set ) : ( ( non
empty countable ) ( non
empty ext-real-membered countable )
Denum_Set_of_R_EAL) ) st
N : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Num of
rng F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( non
empty countable ) ( non
empty ext-real-membered countable )
Denum_Set_of_R_EAL) )
= F : ( ( ) ( )
set ) holds
it : ( ( ) ( )
set )
= Ser (
(rng F : ( ( ) ( ) set ) ) : ( ( non
empty countable ) ( non
empty ext-real-membered countable )
Denum_Set_of_R_EAL) ,
N : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Num of
rng F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( non
empty countable ) ( non
empty ext-real-membered countable )
Denum_Set_of_R_EAL) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ;
end;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative holds
(
(Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= (Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) &
0. : ( ( ) (
ext-real )
R_eal)
<= (Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative holds
for
n,
m being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= (Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + m : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ;
theorem
for
F1,
F2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= F2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ) holds
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(Ser F1 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= (Ser F2 : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ;
theorem
for
F1,
F2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= F2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ) holds
SUM F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal)
<= SUM F2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) holds
(
(Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) & ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) )
for
y being ( ( ) (
ext-real )
R_eal) st
y : ( ( ) (
ext-real )
R_eal)
= (Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) holds
(Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= y : ( ( ) (
ext-real )
R_eal)
+ (F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) . (n : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() V36() ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
ext-real )
R_eal) : ( ( ) (
ext-real )
R_eal) ) ) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative & ex
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= +infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) holds
SUM F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal)
= +infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative & ex
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= +infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) holds
not
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
summable ;
theorem
for
F1,
F2 being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative & ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<= F2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal) ) &
F2 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
summable holds
F1 : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
summable ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative holds
for
n being ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real )
Nat) st ( for
r being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real )
Nat)
<= r : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. r : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= 0. : ( ( ) (
ext-real )
R_eal) ) holds
SUM F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) : ( ( ) (
ext-real )
R_eal)
= (Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( (
natural ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real )
Nat) : ( ( ) (
ext-real )
R_eal) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
in REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) holds
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
(Ser F : ( ( Function-like V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) -defined ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) -valued Function-like non empty total V18( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ext-real-valued ) Function of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() ) Element of K19(REAL : ( ( ) ( non empty V12() V23() complex-membered ext-real-membered real-membered V46() ) set ) ) : ( ( ) ( ) set ) ) , ExtREAL : ( ( ) ( non empty ext-real-membered ) set ) ) ) : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
in REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ;
theorem
for
F being ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) st
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
nonnegative & ex
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
( ( for
k being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) )
<= k : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. k : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
= 0. : ( ( ) (
ext-real )
R_eal) ) & ( for
k being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) st
k : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) )
<= n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) holds
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
. k : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
V36()
ext-real complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V50()
V51() )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
ext-real )
R_eal)
<> +infty : ( ( ) (
V36()
ext-real )
Element of
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) ) holds
F : ( (
Function-like V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) ) (
Relation-like NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) )
-defined ExtREAL : ( ( ) ( non
empty ext-real-membered )
set )
-valued Function-like non
empty total V18(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) )
ext-real-valued )
Function of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V46() )
Element of
K19(
REAL : ( ( ) ( non
empty V12()
V23()
complex-membered ext-real-membered real-membered V46() )
set ) ) : ( ( ) ( )
set ) ) ,
ExtREAL : ( ( ) ( non
empty ext-real-membered )
set ) ) is
summable ;