begin
theorem
for
T,
S being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
B being ( ( ) ( )
Subset-Family of ) st
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous &
B : ( ( ) ( )
Subset-Family of ) is
open holds
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
" B : ( ( ) ( )
Subset-Family of ) : ( ( ) ( )
Element of
K6( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) is
open ;
theorem
for
T,
S being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
P being ( ( ) ( )
Subset of )
for
F being ( ( ) ( )
Subset-Family of ) st ex
B being ( ( ) ( )
Subset-Family of ) st
(
B : ( ( ) ( )
Subset-Family of )
c= f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
" F : ( ( ) ( )
Subset-Family of ) : ( ( ) ( )
Element of
K6( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) &
B : ( ( ) ( )
Subset-Family of ) is ( ( ) ( )
Cover of
P : ( ( ) ( )
Subset of ) ) &
B : ( ( ) ( )
Subset-Family of ) is
finite ) holds
ex
G being ( ( ) ( )
Subset-Family of ) st
(
G : ( ( ) ( )
Subset-Family of )
c= F : ( ( ) ( )
Subset-Family of ) &
G : ( ( ) ( )
Subset-Family of ) is ( ( ) ( )
Cover of
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
.: P : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
G : ( ( ) ( )
Subset-Family of ) is
finite ) ;
begin
theorem
for
T,
S being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of ) is
compact &
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
.: P : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) is
compact ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) )
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of )
<> {} : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real functional V47()
V48()
V49()
V50()
V51()
V52()
V53()
finite V58()
FinSequence-membered )
set ) &
P : ( ( ) ( )
Subset of ) is
compact &
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) is
continuous holds
ex
x1 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
(
x1 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( ) ( )
Subset of ) &
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) )
. x1 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= upper_bound (f : ( ( Function-like V30( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) -valued Function-like V30( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V47() V48() V49() ) set ) ) .: P : ( ( ) ( ) Subset of ) ) : ( ( ) (
V47()
V48()
V49() )
Element of
K6( the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Real) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) )
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of )
<> {} : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real functional V47()
V48()
V49()
V50()
V51()
V52()
V53()
finite V58()
FinSequence-membered )
set ) &
P : ( ( ) ( )
Subset of ) is
compact &
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) is
continuous holds
ex
x2 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
(
x2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( ) ( )
Subset of ) &
f : ( (
Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set )
-valued Function-like V30( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty V47()
V48()
V49() )
set ) )
. x2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set )
= lower_bound (f : ( ( Function-like V30( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) -valued Function-like V30( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V200() ) TopStruct ) : ( ( ) ( non empty V47() V48() V49() ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V47() V48() V49() ) set ) ) .: P : ( ( ) ( ) Subset of ) ) : ( ( ) (
V47()
V48()
V49() )
Element of
K6( the
carrier of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V200() )
TopStruct ) : ( ( ) ( non
empty V47()
V48()
V49() )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
V11()
real ext-real )
Real) ) ;
begin