begin
definition
let X be ( ( ) ( )
set ) ;
func PGraph X -> ( ( ) ( )
MultiGraphStruct )
equals
MultiGraphStruct(#
X : ( ( ) ( )
RLTopStruct ) ,
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) ,
(pr1 (X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) )) : ( (
Function-like V18(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
RLTopStruct ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
RLTopStruct ) )
Function-like V18(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
RLTopStruct ) ) )
Element of
bool [:[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) ) ,
(pr2 (X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) )) : ( (
Function-like V18(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
RLTopStruct ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
RLTopStruct ) )
Function-like V18(
[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
RLTopStruct ) ) )
Element of
bool [:[:X : ( ( ) ( ) RLTopStruct ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) RLTopStruct ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) ) #) : ( (
strict ) (
strict )
MultiGraphStruct ) ;
end;
begin
definition
let X be ( ( non
empty ) ( non
empty )
set ) ;
let f,
g be ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
X : ( ( non
empty ) ( non
empty )
set ) ) ;
pred g is_Shortcut_of f means
(
f : ( ( ) ( )
set )
. 1 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= g : ( (
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
set ) )
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) )
Element of
bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) )
. 1 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set ) &
f : ( ( ) ( )
set )
. (len f : ( ( ) ( ) set ) ) : ( ( ) (
ordinal natural V28()
real ext-real non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= g : ( (
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
set ) )
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) )
Element of
bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) )
. (len g : ( ( Function-like V18([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) ) ) ( V1() V4([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ) V5(X : ( ( ) ( ) set ) ) Function-like V18([:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) ) ) Element of bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) : ( ( ) ( ) set ) ) ) : ( ( ) (
ordinal natural V28()
real ext-real non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set ) & ex
fc being ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier' of
(PGraph X : ( ( ) ( ) set ) ) : ( ( ) ( )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSubsequence-like )
Subset of ( ( ) (
finite V45() )
set ) ) ex
fvs being ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5(
X : ( ( ) ( )
set ) )
Function-like finite FinSubsequence-like )
Subset of ( ( ) ( )
set ) ) ex
sc being ( (
oriented simple ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier' of
(PGraph X : ( ( ) ( ) set ) ) : ( ( ) ( )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSequence-like FinSubsequence-like oriented simple )
Chain of
PGraph X : ( ( ) ( )
set ) : ( ( ) ( )
MultiGraphStruct ) ) ex
g1 being ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier of
(PGraph X : ( ( ) ( ) set ) ) : ( ( ) ( )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of the
carrier of
(PGraph X : ( ( ) ( ) set ) ) : ( ( ) ( )
MultiGraphStruct ) : ( ( ) ( )
set ) ) st
(
Seq fc : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier' of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSubsequence-like )
Subset of ( ( ) (
finite V45() )
set ) ) : ( (
V1()
Function-like ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
set )
= sc : ( (
oriented simple ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier' of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSequence-like FinSubsequence-like oriented simple )
Chain of
PGraph X : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) ) &
Seq fvs : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5(
X : ( ( non
empty ) ( non
empty )
set ) )
Function-like finite FinSubsequence-like )
Subset of ( ( ) (
finite V45() )
set ) ) : ( (
V1()
Function-like ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite FinSequence-like FinSubsequence-like )
set )
= g : ( (
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
set ) )
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) )
Element of
bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) ) &
g1 : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( non
empty )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of the
carrier of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( non
empty )
set ) )
= g : ( (
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) ) (
V1()
V4(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) )
V5(
X : ( ( ) ( )
set ) )
Function-like V18(
[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) ,
X : ( ( ) ( )
set ) ) )
Element of
bool [:[:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( V1() ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) (
V1() )
set ) : ( ( ) ( )
set ) ) &
g1 : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( non
empty )
set ) )
Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of the
carrier of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( non
empty )
set ) )
is_oriented_vertex_seq_of sc : ( (
oriented simple ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
V5( the
carrier' of
(PGraph X : ( ( non empty ) ( non empty ) set ) ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) : ( ( ) ( )
set ) )
Function-like finite FinSequence-like FinSubsequence-like oriented simple )
Chain of
PGraph X : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty V76() )
MultiGraphStruct ) ) ) );
end;
begin
begin
theorem
for
X,
Y being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
f1 being ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= f1 : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) &
f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
f1 : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous ;
theorem
for
X,
Y being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
f being ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
P being ( ( non
empty ) ( non
empty )
Subset of ) st
X : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
compact &
Y : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
T_2 &
f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous &
f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
one-to-one &
P : ( ( non
empty ) ( non
empty )
Subset of )
= rng f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( )
set ) ) holds
ex
f1 being ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
(
f : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= f1 : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) &
f1 : ( (
Function-like V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) ) (
V1()
V4( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
being_homeomorphism ) ;
theorem
for
f,
g being ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) )
for
a,
b,
c,
d being ( (
real ) (
V28()
real ext-real )
number )
for
O,
I being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
O : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
= 0 : ( ( ) (
ordinal natural V28()
real ext-real non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) &
I : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
= 1 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) ) &
f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) is
continuous &
f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) is
one-to-one &
g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) is
continuous &
g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) is
one-to-one &
(f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . O : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
= a : ( (
real ) (
V28()
real ext-real )
number ) &
(f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . I : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
= b : ( (
real ) (
V28()
real ext-real )
number ) &
(g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . O : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
= c : ( (
real ) (
V28()
real ext-real )
number ) &
(g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . I : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
= d : ( (
real ) (
V28()
real ext-real )
number ) & ( for
r being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
(
a : ( (
real ) (
V28()
real ext-real )
number )
<= (f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) ) &
(f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
<= b : ( (
real ) (
V28()
real ext-real )
number ) &
a : ( (
real ) (
V28()
real ext-real )
number )
<= (g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) ) &
(g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`1 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
<= b : ( (
real ) (
V28()
real ext-real )
number ) &
c : ( (
real ) (
V28()
real ext-real )
number )
<= (f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) ) &
(f : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
<= d : ( (
real ) (
V28()
real ext-real )
number ) &
c : ( (
real ) (
V28()
real ext-real )
number )
<= (g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) ) &
(g : ( ( Function-like V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) ( V1() V4( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) ) V5( the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) Function-like non empty total V18( the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like ) SubSpace of K716() : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V128() V194() V211() V212() V213() V214() V215() V216() V217() strict ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( functional non empty ) set ) ) . r : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) (
V1()
V4(
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
Function-like finite 2 : ( ( ) ( non
empty ordinal natural V28()
real ext-real positive non
negative V33()
V38()
finite cardinal V181()
V182()
V183()
V184()
V185()
V186()
V281()
V282()
V283()
V284()
V285() )
Element of
NAT : ( ( ) ( non
trivial ordinal non
finite cardinal limit_cardinal V181()
V182()
V183()
V184()
V185()
V186()
V187()
V283() )
Element of
bool REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) : ( ( ) ( )
set ) ) )
-element FinSequence-like FinSubsequence-like complex-yielding V172()
V173() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
`2 : ( ( ) (
V28()
real ext-real )
Element of
REAL : ( ( ) (
V181()
V182()
V183()
V187()
V283()
V284()
V286() )
set ) )
<= d : ( (
real ) (
V28()
real ext-real )
number ) ) ) holds
rng f : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional non
empty )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( )
set ) )
meets rng g : ( (
Function-like V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) (
V1()
V4( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) )
V5( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
Function-like non
empty total V18( the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like )
SubSpace of
K716() : ( (
TopSpace-like ) (
TopSpace-like )
TopStruct ) ) : ( ( ) ( non
empty )
set ) , the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) )
Function of ( ( ) ( non
empty )
set ) , ( ( ) (
functional non
empty )
set ) ) : ( ( ) (
functional non
empty )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V28() real ext-real positive non negative V33() V38() finite cardinal V181() V182() V183() V184() V185() V186() V281() V282() V283() V284() V285() ) Element of NAT : ( ( ) ( non trivial ordinal non finite cardinal limit_cardinal V181() V182() V183() V184() V185() V186() V187() V283() ) Element of bool REAL : ( ( ) ( V181() V182() V183() V187() V283() V284() V286() ) set ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V128()
V194()
V211()
V212()
V213()
V214()
V215()
V216()
V217()
strict )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( )
set ) ) ;