begin
theorem
for
T1,
T2 being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
D being ( ( ) ( )
Subset of ) st
D : ( ( ) ( )
Subset of ) is
open holds
for
x1 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
x2 being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
X1 being ( ( ) ( )
Subset of )
for
X2 being ( ( ) ( )
Subset of ) holds
( (
X1 : ( ( ) ( )
Subset of )
= (pr1 ( the carrier of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like [: 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 ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [:[: 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 ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
.: (D : ( ( ) ( ) Subset of ) /\ [: the carrier of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,{x2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) ) : ( ( ) ( )
Element of
bool the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) implies
X1 : ( ( ) ( )
Subset of ) is
open ) & (
X2 : ( ( ) ( )
Subset of )
= (pr2 ( the carrier of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) )) : ( (
Function-like quasi_total ) (
Relation-like [: 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 ) :] : ( ( ) ( non
empty )
set )
-defined the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Element of
bool [:[: 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 ) :] : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
.: (D : ( ( ) ( ) Subset of ) /\ [:{x1 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) -element ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , the carrier of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) : ( ( ) ( )
Element of
bool the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) implies
X2 : ( ( ) ( )
Subset of ) is
open ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st ( for
pmet9 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= pmet9 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
pmet9 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) is
continuous ) holds
for
x being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
dist (
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ,
x : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) is
continuous ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
f : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of X : ( ( non
empty ) ( non
empty )
set ) holds
for
A being ( ( non
empty ) ( non
empty )
Subset of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) holds
(lower_bound (f : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) )) : ( (
Function-like quasi_total ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
>= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ;
theorem
for
X being ( ( non
empty ) ( non
empty )
set )
for
f being ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[:X : ( ( non empty ) ( non empty ) set ) ,X : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
f : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of X : ( ( non
empty ) ( non
empty )
set ) holds
for
A being ( ( ) ( )
Subset of ( ( ) ( non
empty )
set ) )
for
x being ( ( ) ( )
Element of
X : ( ( non
empty ) ( non
empty )
set ) ) st
x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
in A : ( ( ) ( )
Subset of ( ( ) ( non
empty )
set ) ) holds
(lower_bound (f : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) )) : ( (
Function-like quasi_total ) (
Relation-like b1 : ( ( non
empty ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
b1 : ( ( non
empty ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. x : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) holds
for
x,
y being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
A being ( ( non
empty ) ( non
empty )
Subset of ) holds
abs (((lower_bound (pmet : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( non empty ) ( non empty ) Subset of ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) . x : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V35() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) - ((lower_bound (pmet : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( non empty ) ( non empty ) Subset of ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) . y : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( V35() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
<= pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. (
x : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
y : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
dist (
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ,
p : ( ( non
empty ) ( non
empty )
Subset of ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) is
continuous ) holds
for
A being ( ( non
empty ) ( non
empty )
Subset of ) holds
lower_bound (
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ,
A : ( ( non
empty ) ( non
empty )
Subset of ) ) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) is
continuous ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_metric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
A being ( ( non
empty ) ( non
empty )
Subset of ) holds
Cl A : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) (
closed )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= { p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : (lower_bound (pmet : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( non empty ) ( non empty ) Subset of ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) . p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( V35() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) = 0 : ( ( ) ( epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) } ) holds
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
metrizable ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
FS2 being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ex
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
(
FS2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
. n : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( (
Function-like ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
= pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) &
pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) ) & ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
FS2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
# pq : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) is
summable ) holds
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. pq : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= Sum (FS2 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined PFuncs ([: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Functional_Sequence of ( ( ) ( ) set ) ,[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) # pq : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ) holds
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
FS1 being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs ( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) , the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ex
f being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
(
FS1 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs ( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) , the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
. n : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
bool [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
= f : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) &
f : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) is
continuous & ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
>= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ) ) ) & ex
seq being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Real_Sequence) st
(
seq : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) is
summable & ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) )
for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
(FS1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined PFuncs ( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Functional_Sequence of ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) # p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
. n : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
<= seq : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) )
. n : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ) ) holds
for
f being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) holds
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= Sum (FS1 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined PFuncs ( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Functional_Sequence of ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) # p : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ) holds
f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) is
continuous ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
s being ( ( ) (
V35()
real ext-real )
Real)
for
FS2 being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ex
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
(
FS2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
. n : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( (
Function-like ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
= pmet : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) &
pmet : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
pmet : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) )
. pq : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
<= s : ( ( ) (
V35()
real ext-real )
Real) ) & ( for
pmet9 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) )
= pmet9 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) holds
pmet9 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) is
continuous ) ) ) holds
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. pq : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= Sum (((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( V35() real ext-real non negative ) Element of REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) GeoSeq) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non empty non trivial non finite complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) (#) (FS2 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined PFuncs ([: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Functional_Sequence of ( ( ) ( ) set ) ,[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) # pq : ( ( Function-like quasi_total ) ( Relation-like the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) RealMap of ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non empty non trivial non finite complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( (
Function-like ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ) holds
(
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
pmet9 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= pmet9 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) holds
pmet9 : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) is
continuous ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
pmet9 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= pmet9 : ( ( non
empty ) ( non
empty )
Subset of ) holds
pmet9 : ( ( non
empty ) ( non
empty )
Subset of ) is
continuous ) holds
for
A being ( ( non
empty ) ( non
empty )
Subset of )
for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) st
p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
in Cl A : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) (
closed )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) holds
(lower_bound (pmet : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A : ( ( non empty ) ( non empty ) Subset of ) )) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. p : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) st
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
T_1 holds
for
s being ( ( ) (
V35()
real ext-real )
Real)
for
FS2 being ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) st ( for
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ex
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
(
FS2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
. n : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( (
Function-like ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
= pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) &
pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
is_a_pseudometric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
. pq : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
<= s : ( ( ) (
V35()
real ext-real )
Real) ) & ( for
pmet9 being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
[:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( (
strict TopSpace-like ) ( non
empty strict TopSpace-like )
TopStruct ) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
RealMap of ( ( ) ( non
empty )
set ) ) st
pmet : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
= pmet9 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) holds
pmet9 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) is
continuous ) ) ) & ( for
p being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
A9 being ( ( non
empty ) ( non
empty )
Subset of ) st not
p : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
in A9 : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) &
A9 : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) is
closed holds
ex
n being ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) st
for
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
FS2 : ( (
Function-like quasi_total ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined PFuncs (
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Functional_Sequence of ( ( ) ( )
set ) ,
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) )
. n : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) : ( (
Function-like ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like complex-valued ext-real-valued real-valued )
Element of
bool [:[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
= pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) holds
(lower_bound (pmet : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) ,A9 : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) )) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. p : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
> 0 : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ) holds
( ex
pmet being ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) st
(
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
is_metric_of the
carrier of
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) & ( for
pq being ( ( ) ( )
Element of
[: the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) holds
pmet : ( (
Function-like quasi_total ) (
Relation-like [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Function of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ,
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
. pq : ( ( ) ( )
Element of
[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) )
= Sum (((1 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) / 2 : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real positive non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() ) Element of NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) ) : ( ( ) ( V35() real ext-real non negative ) Element of REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) GeoSeq) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non empty non trivial non finite complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) (#) (FS2 : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined PFuncs ([: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Functional_Sequence of ( ( ) ( ) set ) ,[: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) # pq : ( ( ) ( ) Element of [: the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued ) Element of bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non empty non trivial non finite complex-valued ext-real-valued real-valued ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ) : ( (
Function-like ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set )
-valued Function-like non
empty total quasi_total complex-valued ext-real-valued real-valued )
Element of
bool [:NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) ,REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) :] : ( ( ) ( non
empty non
trivial non
finite complex-valued ext-real-valued real-valued )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) : ( ( ) (
V35()
real ext-real )
Element of
REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) ) ) ) &
T : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) is
metrizable ) ;
theorem
for
D being ( ( non
empty ) ( non
empty )
set )
for
p,
q being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
D : ( ( non
empty ) ( non
empty )
set ) )
for
B being ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
D : ( ( non
empty ) ( non
empty )
set ) ) st
p : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
one-to-one &
q : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
one-to-one &
rng q : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
c= rng p : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
B : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
commutative &
B : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
associative & (
B : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
having_a_unity or (
len q : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) )
>= 1 : ( ( ) ( non
empty epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real positive non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) &
len p : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) )
> len q : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
epsilon-transitive epsilon-connected ordinal natural V35()
real V37()
ext-real non
negative finite cardinal V65()
V76()
V77()
V78()
V79()
V80()
V81() )
Element of
NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) ) ) ) ) holds
ex
r being ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
D : ( ( non
empty ) ( non
empty )
set ) ) st
(
r : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) is
one-to-one &
rng r : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= (rng p : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
\ (rng q : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
finite )
Element of
bool b1 : ( ( non
empty ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
B : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) )
"**" p : ( ( ) (
Relation-like NAT : ( ( ) ( non
empty non
trivial epsilon-transitive epsilon-connected ordinal non
finite cardinal limit_cardinal V76()
V77()
V78()
V79()
V80()
V81()
V82() )
Element of
bool REAL : ( ( ) ( non
empty non
trivial non
finite V76()
V77()
V78()
V82() )
set ) : ( ( ) ( non
empty non
trivial non
finite )
set ) )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like finite FinSequence-like FinSubsequence-like )
FinSequence of
b1 : ( ( non
empty ) ( non
empty )
set ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) )
= B : ( (
Function-like quasi_total ) (
Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non
empty )
set )
-defined b1 : ( ( non
empty ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
BinOp of
b1 : ( ( non
empty ) ( non
empty )
set ) )
. (
(B : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) "**" q : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ,
(B : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( non empty ) ( non empty ) set ) ,b1 : ( ( non empty ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) BinOp of b1 : ( ( non empty ) ( non empty ) set ) ) "**" r : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() ) Element of bool REAL : ( ( ) ( non empty non trivial non finite V76() V77() V78() V82() ) set ) : ( ( ) ( non empty non trivial non finite ) set ) ) -defined b1 : ( ( non empty ) ( non empty ) set ) -valued Function-like finite FinSequence-like FinSubsequence-like ) FinSequence of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
b1 : ( ( non
empty ) ( non
empty )
set ) ) ) ;