begin
theorem
for
P,
Q being ( ( non
empty ) ( non
empty functional )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
for
f being ( ( ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Path of
p1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) )
for
g being ( ( ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Path of
q1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ) st
rng f : ( ( ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Path of
b3 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
b4 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ) : ( ( ) ( non
empty functional )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= P : ( ( non
empty ) ( non
empty functional )
Subset of ) &
rng g : ( ( ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Path of
b5 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
b6 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) ) : ( ( ) ( non
empty functional )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= Q : ( ( non
empty ) ( non
empty functional )
Subset of ) & ( for
p being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) st
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
in P : ( ( non
empty ) ( non
empty functional )
Subset of ) holds
(
p1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) ) ) & ( for
p being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) st
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
in Q : ( ( non
empty ) ( non
empty functional )
Subset of ) holds
(
p1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) ) ) & ( for
p being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) st
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
in P : ( ( non
empty ) ( non
empty functional )
Subset of ) holds
(
q1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= q2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) ) ) & ( for
p being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) st
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
in Q : ( ( non
empty ) ( non
empty functional )
Subset of ) holds
(
q1 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
p : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= q2 : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) ) ) holds
P : ( ( non
empty ) ( non
empty functional )
Subset of )
meets Q : ( ( non
empty ) ( non
empty functional )
Subset of ) ;
theorem
for
a,
b,
c,
d being ( (
real ) (
V11()
real ext-real )
number )
for
f,
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Function of ( ( ) ( non
empty V148()
V149()
V150() )
set ) , ( ( ) ( non
empty functional )
set ) )
for
O,
I being ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) ) st
O : ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
= 0 : ( ( ) (
empty natural V11()
real ext-real non
positive non
negative V22()
non-empty empty-yielding V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
V26(
RAT : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V151()
V154() )
set ) )
Function-like one-to-one constant functional V36()
FinSequence-like FinSubsequence-like FinSequence-membered integer V101()
V138()
V139()
V140()
V141()
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222()
V223()
V224()
V225() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) &
I : ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
= 1 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) &
(f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . O : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= a : ( (
real ) (
V11()
real ext-real )
number ) &
(f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . I : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= b : ( (
real ) (
V11()
real ext-real )
number ) &
(g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . O : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= c : ( (
real ) (
V11()
real ext-real )
number ) &
(g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . I : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= d : ( (
real ) (
V11()
real ext-real )
number ) & ( for
r being ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) ) holds
(
a : ( (
real ) (
V11()
real ext-real )
number )
<= (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
(f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= b : ( (
real ) (
V11()
real ext-real )
number ) &
a : ( (
real ) (
V11()
real ext-real )
number )
<= (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
(g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= b : ( (
real ) (
V11()
real ext-real )
number ) &
c : ( (
real ) (
V11()
real ext-real )
number )
<= (f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
(f : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= d : ( (
real ) (
V11()
real ext-real )
number ) &
c : ( (
real ) (
V11()
real ext-real )
number )
<= (g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) &
(g : ( ( Function-like V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) ( non empty V22() V25( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) ) V26( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) Function-like total V33( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 connected compact V210() pathwise_connected ) TopStruct ) : ( ( ) ( non empty V148() V149() V150() ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V114() V160() V161() V162() V163() V164() V165() V166() strict pathwise_connected ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) continuous ) Function of ( ( ) ( non empty V148() V149() V150() ) set ) , ( ( ) ( non empty functional ) set ) ) . r : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V148() V149() V150() ) set ) ) ) : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
<= d : ( (
real ) (
V11()
real ext-real )
number ) ) ) holds
rng f : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Function of ( ( ) ( non
empty V148()
V149()
V150() )
set ) , ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( non
empty functional )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
meets rng g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous ) ( non
empty V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
TopStruct ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
continuous )
Function of ( ( ) ( non
empty V148()
V149()
V150() )
set ) , ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( non
empty functional )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative integer V101() V148() V149() V150() V151() V152() V153() V220() V222() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() V222() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() V222() V223() V225() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) ) ;
theorem
for
a,
b,
c,
d being ( (
real ) (
V11()
real ext-real )
number )
for
ar,
br,
cr,
dr being ( ( ) ( )
Point of ( ( ) ( )
set ) )
for
h being ( ( ) (
V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) )
Path of
ar : ( ( ) ( )
Point of ( ( ) ( )
set ) ) ,
br : ( ( ) ( )
Point of ( ( ) ( )
set ) ) )
for
v being ( ( ) (
V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) )
Path of
dr : ( ( ) ( )
Point of ( ( ) ( )
set ) ) ,
cr : ( ( ) ( )
Point of ( ( ) ( )
set ) ) )
for
Ar,
Br,
Cr,
Dr being ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) st
Ar : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= a : ( (
real ) (
V11()
real ext-real )
number ) &
Br : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= b : ( (
real ) (
V11()
real ext-real )
number ) &
Cr : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= c : ( (
real ) (
V11()
real ext-real )
number ) &
Dr : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) )
= d : ( (
real ) (
V11()
real ext-real )
number ) &
ar : ( ( ) ( )
Point of ( ( ) ( )
set ) )
= Ar : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) &
br : ( ( ) ( )
Point of ( ( ) ( )
set ) )
= Br : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) &
cr : ( ( ) ( )
Point of ( ( ) ( )
set ) )
= Cr : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) &
dr : ( ( ) ( )
Point of ( ( ) ( )
set ) )
= Dr : ( ( ) (
V22()
V25(
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) )
Function-like V36()
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like FinSubsequence-like V138()
V139()
V140() )
Point of ( ( ) ( non
empty functional )
set ) ) holds
ex
s,
t being ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) ) st
h : ( ( ) (
V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) )
Path of
b5 : ( ( ) ( )
Point of ( ( ) ( )
set ) ) ,
b6 : ( ( ) ( )
Point of ( ( ) ( )
set ) ) )
. s : ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) ) : ( ( ) ( )
Element of the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) )
= v : ( ( ) (
V22()
V25( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) )
V26( the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 connected compact V210()
pathwise_connected )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V210() )
TopStruct ) ) : ( ( ) ( non
empty V148()
V149()
V150() )
set ) , the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) )
Path of
b8 : ( ( ) ( )
Point of ( ( ) ( )
set ) ) ,
b7 : ( ( ) ( )
Point of ( ( ) ( )
set ) ) )
. t : ( ( ) (
V11()
real ext-real )
Point of ( ( ) ( non
empty V148()
V149()
V150() )
set ) ) : ( ( ) ( )
Element of the
carrier of
(Trectangle (b1 : ( ( real ) ( V11() real ext-real ) number ) ,b2 : ( ( real ) ( V11() real ext-real ) number ) ,b3 : ( ( real ) ( V11() real ext-real ) number ) ,b4 : ( ( real ) ( V11() real ext-real ) number ) )) : ( ( ) (
TopSpace-like convex )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative integer V101()
V148()
V149()
V150()
V151()
V152()
V153()
V220()
V222() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154()
V222() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154()
V222()
V223()
V225() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) ;