begin
theorem
for
T being ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace)
for
P,
Q being ( ( ) ( )
Subset of )
for
p being ( ( ) ( )
Point of ( ( ) ( )
set ) )
for
f being ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
for
g being ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) ) st
P : ( ( ) ( )
Subset of )
/\ Q : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K19( the
carrier of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= {p : ( ( ) ( ) Point of ( ( ) ( ) set ) ) } : ( ( ) ( non
empty )
set ) &
f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism &
f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 1 : ( ( ) ( non
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
ext-real positive V118()
V120() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= p : ( ( ) ( )
Point of ( ( ) ( )
set ) ) &
g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism &
g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
V36()
ext-real V120()
V123() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= p : ( ( ) ( )
Point of ( ( ) ( )
set ) ) holds
ex
h being ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) ) st
(
h : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism &
h : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
V36()
ext-real V120()
V123() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 0 : ( ( ) (
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
V36()
ext-real V120()
V123() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set ) &
h : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | (b2 : ( ( ) ( ) Subset of ) \/ b3 : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 1 : ( ( ) ( non
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
ext-real positive V118()
V120() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set )
-defined the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set )
-valued Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V117() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V117() )
TopStruct ) ) : ( ( ) ( non
empty V30()
V31()
V32() )
set ) , the
carrier of
(b1 : ( ( TopSpace-like T_2 ) ( TopSpace-like T_0 T_1 T_2 ) TopSpace) | b3 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b1 : ( (
TopSpace-like T_2 ) (
TopSpace-like T_0 T_1 T_2 )
TopSpace) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V30()
V31()
V32() )
set ) , ( ( ) ( )
set ) )
. 1 : ( ( ) ( non
empty V27()
V28()
V29()
V30()
V31()
V32()
V33()
V34()
V35()
ext-real positive V118()
V120() )
Element of
NAT : ( ( ) (
V30()
V31()
V32()
V33()
V34()
V35()
V36()
V120() )
Element of
K19(
REAL : ( ( ) ( non
empty V30()
V31()
V32()
V36()
V43()
V120()
V121()
V123() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set ) ) ;