begin
definition
let X,
Y be ( ( non
empty ) ( non
empty )
MetrStruct ) ;
let f be ( (
Function-like V33( the
carrier of
X : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
Y : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
X : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
Y : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
X : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
Y : ( ( non
empty ) ( non
empty )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) ;
attr f is
uniformly_continuous means
for
r being ( ( ) (
V11()
real ext-real )
Real) st
0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
< r : ( ( ) (
V11()
real ext-real )
Real) holds
ex
s being ( ( ) (
V11()
real ext-real )
Real) st
(
0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
< s : ( ( ) (
V11()
real ext-real )
Real) & ( for
u1,
u2 being ( ( ) ( )
Element of ( ( ) ( )
set ) ) st
dist (
u1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
u2 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< s : ( ( ) (
V11()
real ext-real )
Real) holds
dist (
(f : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) /. u1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
Y : ( (
Function-like V33(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) ) ) (
V19()
V22(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like total V33(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) )
V168()
V169()
V170() )
Element of
K6(
K7(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ,
(f : ( ( ) ( ) Element of X : ( ( ) ( ) MetrStruct ) ) /. u2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of the
carrier of
Y : ( (
Function-like V33(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) ) ) (
V19()
V22(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like total V33(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) )
V168()
V169()
V170() )
Element of
K6(
K7(
K7(
X : ( ( ) ( )
MetrStruct ) ,
X : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< r : ( ( ) (
V11()
real ext-real )
Real) ) );
end;
theorem
for
X being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
M being ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace)
for
f being ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
for
r being ( ( ) (
V11()
real ext-real )
Real)
for
u being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of )
= Ball (
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
r : ( ( ) (
V11()
real ext-real )
Real) ) : ( ( ) ( )
Element of
K6( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
" P : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) is
open ;
theorem
for
N,
M being ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace)
for
f being ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st ( for
r being ( (
real ) (
V11()
real ext-real )
number )
for
u being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
u1 being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
r : ( (
real ) (
V11()
real ext-real )
number )
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
u1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) holds
ex
s being ( (
real ) (
V11()
real ext-real )
number ) st
(
s : ( (
real ) (
V11()
real ext-real )
number )
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) & ( for
w being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
w1 being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
w1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. w : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) &
dist (
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
w : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< s : ( (
real ) (
V11()
real ext-real )
number ) holds
dist (
u1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
w1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< r : ( (
real ) (
V11()
real ext-real )
number ) ) ) ) holds
f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous ;
theorem
for
N,
M being ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace)
for
f being ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
for
r being ( ( ) (
V11()
real ext-real )
Real)
for
u being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
u1 being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
r : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
u1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) holds
ex
s being ( ( ) (
V11()
real ext-real )
Real) st
(
s : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) & ( for
w being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
for
w1 being ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) st
w1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) )
= f : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
. w : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) &
dist (
u : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
w : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< s : ( ( ) (
V11()
real ext-real )
Real) holds
dist (
u1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ,
w1 : ( ( ) ( )
Element of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< r : ( ( ) (
V11()
real ext-real )
Real) ) ) ;
theorem
for
N,
M being ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace)
for
f being ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
g being ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= g : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
uniformly_continuous holds
g : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous ;
begin
theorem
for
N,
M being ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace)
for
f being ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
g being ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
g : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) &
TopSpaceMetr N : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) is
compact &
g : ( (
Function-like V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(TopSpaceMetr b1 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TopSpaceMetr b2 : ( ( non empty Reflexive discerning V86() triangle ) ( non empty Reflexive discerning V86() triangle Discerning ) MetrSpace) ) : ( ( ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
f : ( (
Function-like V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
b1 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty Reflexive discerning V86()
triangle ) ( non
empty Reflexive discerning V86()
triangle Discerning )
MetrSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
uniformly_continuous ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) )
for
f being ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous &
f : ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
uniformly_continuous ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
P being ( ( ) ( )
Subset of )
for
Q being ( ( non
empty ) ( non
empty )
Subset of )
for
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) ) (
V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( )
set ) )
for
f being ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
P : ( ( ) ( )
Subset of )
= Q : ( ( non
empty ) ( non
empty )
Subset of ) &
g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) ) (
V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( )
set ) ) is
continuous &
f : ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) ) (
V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) )
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( V194() ) ( non empty TopSpace-like V133() V158() V159() V160() V161() V162() V163() V164() V194() ) L15()) | b2 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( )
set ) ) holds
f : ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
((Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict Reflexive discerning V86() triangle ) ( non empty strict Reflexive discerning V86() triangle Discerning ) MetrStruct ) | b3 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
Euclid b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
uniformly_continuous ;
begin
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) holds
g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) is ( (
Function-like V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) )
V23( the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
(Closed-Interval-MSpace (0 : ( ( ) ( empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative functional integer FinSequence-membered ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ,1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) )) : ( ( non
empty strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
SubSpace of
RealSpace : ( (
strict ) ( non
empty strict Reflexive discerning V86()
triangle Discerning V116() )
MetrStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(Euclid b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict Reflexive discerning V86()
triangle ) ( non
empty strict Reflexive discerning V86()
triangle Discerning )
MetrStruct ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
e being ( ( ) (
V11()
real ext-real )
Real)
for
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) (
V43(
b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) )
FinSequence-like V170() )
Element of ( ( ) ( non
empty )
set ) ) st
e : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
ex
h being ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) st
(
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) )
. 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
set )
= 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) )
. (len h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
set )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) & 5 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
<= len h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
rng h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
V179()
V180()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) )
c= the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) &
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) is
increasing & ( for
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
Q being ( ( ) ( )
Subset of )
for
W being ( ( ) ( )
Subset of ) st 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
<= i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
< len h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
Q : ( ( ) ( )
Subset of )
= [.(h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) /. i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non finite ) set ) ) ,(h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) /. (i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non finite ) set ) ) .] : ( ( ) ( )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) &
W : ( ( ) ( )
Subset of )
= g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) )
.: Q : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
diameter W : ( ( ) ( )
Subset of ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< e : ( ( ) (
V11()
real ext-real )
Real) ) ) ;
theorem
for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
e being ( ( ) (
V11()
real ext-real )
Real)
for
g being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) )
for
p1,
p2 being ( ( ) (
V43(
b1 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) )
FinSequence-like V170() )
Element of ( ( ) ( non
empty )
set ) ) st
e : ( ( ) (
V11()
real ext-real )
Real)
> 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
ex
h being ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) st
(
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) )
. 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
set )
= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) )
. (len h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V11()
real ext-real )
set )
= 0 : ( ( ) (
empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11()
real ext-real non
positive non
negative functional integer FinSequence-membered )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) & 5 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
<= len h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
rng h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
V179()
V180()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) )
c= the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) &
h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) is
decreasing & ( for
i being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
for
Q being ( ( ) ( )
Subset of )
for
W being ( ( ) ( )
Subset of ) st 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real positive non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
<= i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
i : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
< len h : ( ( ) (
V19()
V22(
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) )
V23(
REAL : ( ( ) ( non
empty non
finite )
set ) )
Function-like finite FinSequence-like FinSubsequence-like V168()
V169()
V170() )
FinSequence of
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V11()
real ext-real non
negative integer )
Element of
NAT : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) ) &
Q : ( ( ) ( )
Subset of )
= [.(h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) /. (i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non finite ) set ) ) ,(h : ( ( ) ( V19() V22( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) V23( REAL : ( ( ) ( non empty non finite ) set ) ) Function-like finite FinSequence-like FinSubsequence-like V168() V169() V170() ) FinSequence of REAL : ( ( ) ( non empty non finite ) set ) ) /. i : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty non finite ) set ) ) .] : ( ( ) ( )
Element of
K6(
REAL : ( ( ) ( non
empty non
finite )
set ) ) : ( ( ) ( non
empty )
set ) ) &
W : ( ( ) ( )
Subset of )
= g : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) ) ( non
empty V19()
V22( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) )
V23( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) )
Function-like total V33( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_2 compact V116() )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like V116() )
TopStruct ) ) : ( ( ) ( non
empty V181() )
set ) , the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty V181() )
set ) , ( ( ) ( non
empty )
set ) )
.: Q : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL b1 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative integer ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal ) Element of K6(REAL : ( ( ) ( non empty non finite ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
V194() ) ( non
empty TopSpace-like V133()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
V194() )
L15()) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
set ) ) holds
diameter W : ( ( ) ( )
Subset of ) : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
finite )
set ) )
< e : ( ( ) (
V11()
real ext-real )
Real) ) ) ;