begin
theorem
for
C being ( ( non
empty ) ( non
empty )
set )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) holds
( (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total implies
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total ) & (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
+ f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total implies (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total ) ) & (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total implies
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
- f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total ) & (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
- f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total implies (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total ) ) & (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total implies
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total ) & (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
(#) f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
total implies (
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total ) ) ) ;
theorem
for
C being ( ( non
empty ) ( non
empty )
set )
for
c being ( ( ) ( )
Element of
C : ( ( non
empty ) ( non
empty )
set ) )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total holds
(
(f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
. c : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real complex real )
set )
= (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set )
+ (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set ) : ( ( ) (
complex )
set ) &
(f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
. c : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real complex real )
set )
= (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set )
- (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set ) : ( ( ) (
complex )
set ) &
(f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
. c : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real complex real )
set )
= (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set )
* (f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set ) : ( ( ) (
complex )
set ) ) ;
theorem
for
C being ( ( non
empty ) ( non
empty )
set )
for
c being ( ( ) ( )
Element of
C : ( ( non
empty ) ( non
empty )
set ) )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total &
f2 : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
^ : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) is
total holds
(f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) / f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
. c : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
ext-real complex real )
set )
= (f1 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
ext-real complex real )
set )
* ((f2 : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) . c : ( ( ) ( ) Element of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real complex real ) set ) ") : ( (
complex ) (
ext-real complex real )
set ) : ( ( ) (
complex )
set ) ;
registration
let X,
C be ( ( ) ( )
set ) ;
end;
theorem
for
X,
Y being ( ( ) ( )
set )
for
C being ( ( non
empty ) ( non
empty )
set )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant holds
(
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant &
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant &
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant ) ;
theorem
for
Y being ( ( ) ( )
set )
for
C being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) st
f : ( (
Function-like ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant holds
( ( for
r being ( (
real ) (
ext-real complex real )
number ) holds
(r : ( ( real ) ( ext-real complex real ) number ) (#) f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded ) &
(- f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded &
(abs f : ( ( Function-like ) ( Relation-like b2 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued bounded_below )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b2 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued bounded_below )
Element of
K19(
K20(
b2 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded ) ;
theorem
for
X,
Y being ( ( ) ( )
set )
for
C being ( ( non
empty ) ( non
empty )
set )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) holds
( (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above ) & (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below ) & (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) + f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded ) ) ;
theorem
for
X,
Y being ( ( ) ( )
set )
for
C being ( ( non
empty ) ( non
empty )
set )
for
f1,
f2 being ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,) holds
( (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_above ) & (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded_below ) & (
f1 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| X : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b1 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded &
f2 : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
PartFunc of ,)
| Y : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b2 : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
constant implies (
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded &
(f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) - f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded &
(f1 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) (#) f2 : ( ( Function-like ) ( Relation-like b3 : ( ( non empty ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty complex-membered ext-real-membered real-membered V51() V52() ) set ) -valued Function-like complex-valued ext-real-valued real-valued ) PartFunc of ,) ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) )
| (X : ( ( ) ( ) set ) /\ Y : ( ( ) ( ) set ) ) : ( ( ) ( )
set ) : ( (
Function-like ) (
Relation-like b3 : ( ( non
empty ) ( non
empty )
set )
-defined b1 : ( ( ) ( )
set )
/\ b2 : ( ( ) ( )
set ) : ( ( ) ( )
set )
-defined b3 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
K19(
K20(
b3 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty complex-membered ext-real-membered real-membered V51()
V52() )
set ) ) : ( ( ) (
Relation-like complex-valued ext-real-valued real-valued )
set ) ) : ( ( ) ( )
set ) ) is
bounded ) ) ) ;