begin
theorem
for
f being ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
for
P being ( ( non
empty ) (
functional non
empty )
Subset of )
for
F being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
for
i being ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) st 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
+ 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= len f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) is
being_S-Seq &
P : ( ( non
empty ) (
functional non
empty )
Subset of )
= L~ f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) ) is
being_homeomorphism &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63()
V66() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( functional non empty ) set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) holds
ex
p1,
p2 being ( ( ) (
V28()
real ext-real )
Real) st
(
p1 : ( ( ) (
V28()
real ext-real )
Real)
< p2 : ( ( ) (
V28()
real ext-real )
Real) &
0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63()
V66() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= p1 : ( ( ) (
V28()
real ext-real )
Real) &
p1 : ( ( ) (
V28()
real ext-real )
Real)
<= 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63()
V66() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= p2 : ( ( ) (
V28()
real ext-real )
Real) &
p2 : ( ( ) (
V28()
real ext-real )
Real)
<= 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
LSeg (
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ,
i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) )
= F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
.: [.p1 : ( ( ) ( V28() real ext-real ) Real) ,p2 : ( ( ) ( V28() real ext-real ) Real) .] : ( ( ) (
V45()
V46()
V47()
V66() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
K19( the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. p1 : ( ( ) (
V28()
real ext-real )
Real) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. p2 : ( ( ) (
V28()
real ext-real )
Real) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. (i : ( ( ) ( natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) ;
theorem
for
f being ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
for
Q,
R being ( ( non
empty ) (
functional non
empty )
Subset of )
for
F being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
for
i being ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
for
P being ( ( non
empty ) ( non
empty V45()
V46()
V47() )
Subset of ) st
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) is
being_S-Seq &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) ) is
being_homeomorphism &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. 0 : ( ( ) (
Function-like functional empty natural V28()
real ext-real non
positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63()
V66() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
. 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. (len f : ( ( ) ( Relation-like NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( functional non empty ) set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) & 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
+ 1 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
<= len f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
.: P : ( ( non
empty ) ( non
empty V45()
V46()
V47() )
Subset of ) : ( ( ) ( )
Element of
K19( the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= LSeg (
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ,
i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) &
Q : ( ( non
empty ) (
functional non
empty )
Subset of )
= L~ f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) &
R : ( ( non
empty ) (
functional non
empty )
Subset of )
= LSeg (
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ,
i : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
ex
G being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(I[01] : ( ( ) ( non empty strict TopSpace-like V145() ) TopStruct ) | b6 : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like V145() )
SubSpace of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b3 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) ) st
(
G : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(I[01] : ( ( ) ( non empty strict TopSpace-like V145() ) TopStruct ) | b6 : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like V145() )
SubSpace of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b3 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
= F : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) )
| P : ( ( non
empty ) ( non
empty V45()
V46()
V47() )
Subset of ) : ( (
Function-like ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
K19(
K20( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) : ( ( ) ( non
empty V45()
V46()
V47() )
set ) , the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b2 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
G : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
(I[01] : ( ( ) ( non empty strict TopSpace-like V145() ) TopStruct ) | b6 : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like V145() )
SubSpace of
I[01] : ( ( ) ( non
empty strict TopSpace-like V145() )
TopStruct ) ) : ( ( ) ( non
empty V45()
V46()
V47() )
set )
-defined the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) | b3 : ( ( non empty ) ( functional non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty V45()
V46()
V47() )
set ) , ( ( ) ( non
empty )
set ) ) is
being_homeomorphism ) ;
begin
theorem
for
p1,
p2,
q1,
q2,
q3 being ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) st
p1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) )
<> p2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) &
LE q1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
q2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) &
LE q2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
q3 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) holds
LE q1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
q3 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p1 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ;
begin
theorem
for
f being ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
for
p,
q being ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) st
p : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) )
in L~ f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) &
q : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) )
in L~ f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) & (
Index (
p : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
< Index (
q : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) or (
Index (
p : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) )
= Index (
q : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) &
LE p : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
q : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. (Index (p : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Point of ( ( ) ( functional non empty ) set ) ) ,f : ( ( ) ( Relation-like NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) )
/. ((Index (p : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Point of ( ( ) ( functional non empty ) set ) ) ,f : ( ( ) ( Relation-like NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( natural V28() real ext-real V43() V44() V45() V46() V47() V48() V49() V50() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) (
natural V28()
real ext-real V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) ) &
p : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) )
<> q : ( ( ) (
Relation-like Function-like V33()
V34()
V35()
V69(2 : ( ( ) ( non
empty natural V28()
real ext-real positive non
negative V43()
V44()
V45()
V46()
V47()
V48()
V49()
V50()
V61()
V63() )
Element of
NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like )
Point of ( ( ) (
functional non
empty )
set ) ) holds
L~ (B_Cut (f : ( ( ) ( Relation-like NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) -defined the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V158() V183() V184() V185() V186() V187() V188() V189() strict V257() ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) -valued Function-like FinSequence-like ) FinSequence of ( ( ) ( functional non empty ) set ) ) ,p : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Point of ( ( ) ( functional non empty ) set ) ) ,q : ( ( ) ( Relation-like Function-like V33() V34() V35() V69(2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) )
c= L~ f : ( ( ) (
Relation-like NAT : ( ( ) (
V45()
V46()
V47()
V48()
V49()
V50()
V51()
V63() )
Element of
K19(
REAL : ( ( ) (
V45()
V46()
V47()
V51()
V63()
V64()
V66() )
set ) ) : ( ( ) ( )
set ) )
-defined the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like FinSequence-like )
FinSequence of ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional )
Element of
K19( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V28() real ext-real positive non negative V43() V44() V45() V46() V47() V48() V49() V50() V61() V63() ) Element of NAT : ( ( ) ( V45() V46() V47() V48() V49() V50() V51() V63() ) Element of K19(REAL : ( ( ) ( V45() V46() V47() V51() V63() V64() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V158()
V183()
V184()
V185()
V186()
V187()
V188()
V189()
strict V257() )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) : ( ( ) ( )
set ) ) ;