REAL is non empty non trivial non finite V76() V77() V78() V82() set
NAT is 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
bool REAL is non empty non trivial non finite set
{} is set
the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V35() real ext-real non positive non negative finite V49() cardinal {} -element FinSequence-membered V76() V77() V78() V79() V80() V81() V82() set
1 is 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
{{},1} is finite set
COMPLEX is non empty non trivial non finite V76() V82() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal V76() V77() V78() V79() V80() V81() V82() set
bool omega is non empty non trivial non finite set
[:NAT,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial non finite set
bool (bool REAL) is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
K115(NAT) is V26() set
RAT is non empty non trivial non finite V76() V77() V78() V79() V82() set
INT is non empty non trivial non finite V76() V77() V78() V79() V80() V82() set
[:1,1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty finite V49() set
[:[:1,1:],1:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty finite V49() set
[:[:1,1:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty non trivial non finite set
[:REAL,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
[:[:REAL,REAL:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite set
2 is 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
[:2,2:] is RAT -valued INT -valued non empty finite complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty non trivial non finite set
K546() is non empty strict TopSpace-like V162() TopStruct
the carrier of K546() is non empty V76() V77() V78() set
RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V162() MetrStruct
R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V162() TopStruct
K553() is non empty strict TopSpace-like V162() SubSpace of R^1
[:COMPLEX,COMPLEX:] is non empty non trivial non finite complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite set
[:COMPLEX,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty non trivial non finite set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite set
bool [:REAL,REAL:] is non empty non trivial non finite set
[:RAT,RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial non finite set
[:[:RAT,RAT:],RAT:] is RAT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite set
[:INT,INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial non finite set
[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite set
[:NAT,NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty non trivial non finite complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite set
K680(2) is V222() L15()
the carrier of K680(2) is set
[: the carrier of K680(2),REAL:] is complex-valued ext-real-valued real-valued set
bool [: the carrier of K680(2),REAL:] is non empty set
bool the carrier of K680(2) is non empty set
3 is 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
0 is 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
real_dist is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
MetrStruct(# REAL,real_dist #) is strict MetrStruct
the carrier of RealSpace is non empty V76() V77() V78() set
TopSpaceMetr RealSpace is TopStruct
the carrier of R^1 is non empty V76() V77() V78() set
dom {} is set
rng {} is set
4 is 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
T is 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
T + 1 is 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
Bn is 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
2 |^ 0 is 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
0 * 2 is 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
(0 * 2) + 1 is 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
1 * ((0 * 2) + 1) is 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
Bn mod 2 is 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
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
2 * bbcT is 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
(2 * bbcT) + 1 is 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
2 |^ 0 is 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
PM is 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
2 * PM is 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
(2 * PM) + 1 is 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
(2 |^ 0) * ((2 * PM) + 1) is 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
Bn mod 2 is 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
bbcT is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
2 * bbcT is 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
(2 * bbcT) + 0 is 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
PM is 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
PM + PM is 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
FB is 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
2 |^ FB is 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
TPM is 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
2 * TPM is 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
(2 * TPM) + 1 is 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
(2 |^ FB) * ((2 * TPM) + 1) is 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
2 * (2 |^ FB) is 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
(2 * (2 |^ FB)) * ((2 * TPM) + 1) is 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
FB + 1 is 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
2 |^ (FB + 1) is 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
(2 |^ (FB + 1)) * ((2 * TPM) + 1) is 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
Bn mod 2 is 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
bbcT is 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
2 |^ bbcT is 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
PM is 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
2 * PM is 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
(2 * PM) + 1 is 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
(2 |^ bbcT) * ((2 * PM) + 1) is 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
T is 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
Bn is 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
T is 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
2 |^ T is 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
Bn is 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
2 * Bn is 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
(2 * Bn) + 1 is 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
(2 |^ T) * ((2 * Bn) + 1) is 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
((2 |^ T) * ((2 * Bn) + 1)) - 1 is V35() real ext-real Element of REAL
T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
Bn is 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
2 |^ Bn is 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
bbcT is 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
[Bn,bbcT] is Element of [:NAT,NAT:]
{Bn,bbcT} is finite V49() V76() V77() V78() V79() V80() V81() set
{Bn} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{Bn,bbcT},{Bn}} is finite V49() set
T . [Bn,bbcT] is 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
2 * bbcT is 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
(2 * bbcT) + 1 is 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
(2 |^ Bn) * ((2 * bbcT) + 1) is 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
((2 |^ Bn) * ((2 * bbcT) + 1)) - 1 is V35() real ext-real Element of REAL
T . (Bn,bbcT) is 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
[Bn,bbcT] is set
T . [Bn,bbcT] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
In ((((2 |^ Bn) * ((2 * bbcT) + 1)) - 1),NAT) is 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
T is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
Bn is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
bbcT is 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
PM is 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
[bbcT,PM] is Element of [:NAT,NAT:]
{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set
{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{bbcT,PM},{bbcT}} is finite V49() set
T . [bbcT,PM] is 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
2 |^ bbcT is 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
2 * PM is 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
(2 * PM) + 1 is 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
(2 |^ bbcT) * ((2 * PM) + 1) is 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
((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL
T . (bbcT,PM) is 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
[bbcT,PM] is set
T . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
Bn . (bbcT,PM) is 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
Bn . [bbcT,PM] is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
() is Relation-like [:NAT,NAT:] -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:[:NAT,NAT:],NAT:]
T is set
Bn is set
() . T is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
() . Bn is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
bbcT is set
PM is set
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
FB is set
TPM is set
[FB,TPM] is set
{FB,TPM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,TPM},{FB}} is finite V49() set
UX is 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
2 |^ UX is 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
k is 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
2 * k is 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
(2 * k) + 1 is 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
(2 |^ UX) * ((2 * k) + 1) is 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
((2 |^ UX) * ((2 * k) + 1)) - 1 is V35() real ext-real Element of REAL
Un is 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
2 |^ Un is 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
UXk is 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
2 * UXk is 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
(2 * UXk) + 1 is 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
(2 |^ Un) * ((2 * UXk) + 1) is 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
((2 |^ Un) * ((2 * UXk) + 1)) - 1 is V35() real ext-real Element of REAL
T is set
Bn is 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
Bn + 1 is 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
bbcT is 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
2 |^ bbcT is 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
PM is 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
2 * PM is 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
(2 * PM) + 1 is 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
(2 |^ bbcT) * ((2 * PM) + 1) is 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
Bn - 0 is V35() real ext-real Element of REAL
((2 |^ bbcT) * ((2 * PM) + 1)) - 1 is V35() real ext-real Element of REAL
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
[bbcT,PM] is Element of [:NAT,NAT:]
{bbcT,PM} is finite V49() V76() V77() V78() V79() V80() V81() set
{bbcT} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{bbcT,PM},{bbcT}} is finite V49() set
() . [bbcT,PM] is 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
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty set
[:T,REAL:] is complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of T
PM is set
Bn . (bbcT,PM) is set
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
Bn . [bbcT,PM] is V35() real ext-real set
Bn . [bbcT,PM] is V35() real ext-real Element of REAL
PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Element of T
[bbcT,FB] is set
{bbcT,FB} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,FB},{bbcT}} is finite V49() set
dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]
bool [:T,T:] is non empty set
Bn . [bbcT,FB] is V35() real ext-real Element of REAL
dom PM is Element of bool T
bool T is non empty set
Bn . (bbcT,FB) is V35() real ext-real Element of REAL
Bn . [bbcT,FB] is V35() real ext-real set
PM . FB is V35() real ext-real Element of REAL
FB is Element of T
PM . FB is V35() real ext-real Element of REAL
Bn . (bbcT,FB) is V35() real ext-real Element of REAL
[bbcT,FB] is set
{bbcT,FB} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,FB},{bbcT}} is finite V49() set
Bn . [bbcT,FB] is V35() real ext-real set
PM is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Relation-like T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
TPM is Element of T
PM . TPM is V35() real ext-real Element of REAL
Bn . (bbcT,TPM) is V35() real ext-real Element of REAL
[bbcT,TPM] is set
{bbcT,TPM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,TPM},{bbcT}} is finite V49() set
Bn . [bbcT,TPM] is V35() real ext-real set
FB . TPM is V35() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
Bn is non empty TopSpace-like TopStruct
[:T,Bn:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,Bn:] is non empty set
bool the carrier of [:T,Bn:] is non empty set
the carrier of Bn is non empty set
bool the carrier of Bn is non empty set
[: the carrier of T, the carrier of Bn:] is non empty set
pr1 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:]
[:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set
bool [:[: the carrier of T, the carrier of Bn:], the carrier of T:] is non empty set
pr2 ( the carrier of T, the carrier of Bn) is Relation-like [: the carrier of T, the carrier of Bn:] -defined the carrier of Bn -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:]
[:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set
bool [:[: the carrier of T, the carrier of Bn:], the carrier of Bn:] is non empty set
FB is Element of bool the carrier of [:T,Bn:]
bool (bool the carrier of [:T,Bn:]) is non empty set
TPM is Element of bool (bool the carrier of [:T,Bn:])
union TPM is Element of bool the carrier of [:T,Bn:]
Un is Element of the carrier of T
{Un} is non empty trivial finite 1 -element Element of bool the carrier of T
[:{Un}, the carrier of Bn:] is non empty set
FB /\ [:{Un}, the carrier of Bn:] is Element of bool the carrier of [:T,Bn:]
(pr2 ( the carrier of T, the carrier of Bn)) .: (FB /\ [:{Un}, the carrier of Bn:]) is Element of bool the carrier of Bn
UX is Element of the carrier of Bn
{UX} is non empty trivial finite 1 -element Element of bool the carrier of Bn
[: the carrier of T,{UX}:] is non empty set
FB /\ [: the carrier of T,{UX}:] is Element of bool the carrier of [:T,Bn:]
(pr1 ( the carrier of T, the carrier of Bn)) .: (FB /\ [: the carrier of T,{UX}:]) is Element of bool the carrier of T
UXk is Element of bool the carrier of T
k is Element of bool the carrier of Bn
UXk9 is set
dom (pr1 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]
bool [: the carrier of T, the carrier of Bn:] is non empty set
nm is set
(pr1 ( the carrier of T, the carrier of Bn)) . nm is set
n is set
m is Element of bool the carrier of T
Unn is Element of bool the carrier of Bn
[:m,Unn:] is Element of bool the carrier of [:T,Bn:]
B is set
B1 is set
[B,B1] is set
{B,B1} is finite set
{B} is non empty trivial finite 1 -element set
{{B,B1},{B}} is finite V49() set
k is set
[k,UX] is set
{k,UX} is finite set
{k} is non empty trivial finite 1 -element set
{{k,UX},{k}} is finite V49() set
(pr1 ( the carrier of T, the carrier of Bn)) . (k,UX) is set
(pr1 ( the carrier of T, the carrier of Bn)) . [k,UX] is set
(pr1 ( the carrier of T, the carrier of Bn)) . (B,B1) is set
(pr1 ( the carrier of T, the carrier of Bn)) . [B,B1] is set
nm is Element of bool the carrier of T
n is Element of bool the carrier of T
UXk9 is set
dom (pr2 ( the carrier of T, the carrier of Bn)) is Relation-like the carrier of T -defined the carrier of Bn -valued Element of bool [: the carrier of T, the carrier of Bn:]
bool [: the carrier of T, the carrier of Bn:] is non empty set
nm is set
(pr2 ( the carrier of T, the carrier of Bn)) . nm is set
n is set
m is set
Unn is set
[m,Unn] is set
{m,Unn} is finite set
{m} is non empty trivial finite 1 -element set
{{m,Unn},{m}} is finite V49() set
(pr2 ( the carrier of T, the carrier of Bn)) . (m,Unn) is set
(pr2 ( the carrier of T, the carrier of Bn)) . [m,Unn] is set
B is Element of bool the carrier of T
B1 is Element of bool the carrier of Bn
[:B,B1:] is Element of bool the carrier of [:T,Bn:]
k is set
[Un,k] is set
{Un,k} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,k},{Un}} is finite V49() set
(pr2 ( the carrier of T, the carrier of Bn)) . (Un,k) is set
(pr2 ( the carrier of T, the carrier of Bn)) . [Un,k] is set
nm is Element of bool the carrier of Bn
n is Element of bool the carrier of Bn
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
bbcT is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of [:T,T:], the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set
PM is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
TPM is Element of the carrier of T
( the carrier of T,bbcT,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
FB is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
bool the carrier of R^1 is non empty set
Un is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
UX is Element of the carrier of T
Un . UX is V35() real ext-real Element of the carrier of R^1
bool the carrier of T is non empty set
[TPM,UX] is Element of [: the carrier of T, the carrier of T:]
{TPM,UX} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,UX},{TPM}} is finite V49() set
pr2 ( the carrier of T, the carrier of T) is Relation-like [: the carrier of T, the carrier of T:] -defined the carrier of T -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of T, the carrier of T:], the carrier of T:]
[:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set
bool [:[: the carrier of T, the carrier of T:], the carrier of T:] is non empty set
dom (pr2 ( the carrier of T, the carrier of T)) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
UXk is Element of the carrier of [:T,T:]
bbcT . (TPM,UX) is V35() real ext-real Element of REAL
[TPM,UX] is set
bbcT . [TPM,UX] is V35() real ext-real set
k is V76() V77() V78() Element of bool the carrier of R^1
bool the carrier of [:T,T:] is non empty set
UXk9 is Element of bool the carrier of [:T,T:]
FB .: UXk9 is V76() V77() V78() Element of bool the carrier of R^1
{TPM} is non empty trivial finite 1 -element Element of bool the carrier of T
[:{TPM}, the carrier of T:] is non empty set
UXk9 /\ [:{TPM}, the carrier of T:] is Element of bool the carrier of [:T,T:]
(pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:]) is Element of bool the carrier of T
(pr2 ( the carrier of T, the carrier of T)) . (TPM,UX) is Element of the carrier of T
(pr2 ( the carrier of T, the carrier of T)) . [TPM,UX] is set
Un .: ((pr2 ( the carrier of T, the carrier of T)) .: (UXk9 /\ [:{TPM}, the carrier of T:])) is V76() V77() V78() Element of bool the carrier of R^1
n is set
dom Un is Element of bool the carrier of T
m is set
Un . m is V35() real ext-real Element of REAL
Unn is Element of the carrier of T
B is set
(pr2 ( the carrier of T, the carrier of T)) . B is set
B1 is set
k is set
[B1,k] is set
{B1,k} is finite set
{B1} is non empty trivial finite 1 -element set
{{B1,k},{B1}} is finite V49() set
q is Element of the carrier of T
s is Element of the carrier of T
[q,s] is Element of [: the carrier of T, the carrier of T:]
{q,s} is finite set
{q} is non empty trivial finite 1 -element set
{{q,s},{q}} is finite V49() set
(pr2 ( the carrier of T, the carrier of T)) . (q,s) is Element of the carrier of T
[q,s] is set
(pr2 ( the carrier of T, the carrier of T)) . [q,s] is set
bbcT . (q,s) is V35() real ext-real Element of REAL
bbcT . [q,s] is V35() real ext-real set
dom FB is Element of bool the carrier of [:T,T:]
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of bool T
PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Element of T
PM . FB is V35() real ext-real Element of REAL
(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,FB) .: bbcT is V76() V77() V78() Element of bool REAL
lower_bound ((T,Bn,FB) .: bbcT) is V35() real ext-real Element of REAL
PM is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
TPM is Element of T
PM . TPM is V35() real ext-real Element of REAL
(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,TPM) .: bbcT is V76() V77() V78() Element of bool REAL
lower_bound ((T,Bn,TPM) .: bbcT) is V35() real ext-real Element of REAL
FB . TPM is V35() real ext-real Element of REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
PM is Element of T
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
bbcT is non empty Element of bool T
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
FB is ext-real set
dom (T,Bn,PM) is Element of bool T
TPM is set
(T,Bn,PM) . TPM is V35() real ext-real Element of REAL
Un is Element of T
Bn . (PM,Un) is V35() real ext-real Element of REAL
[PM,Un] is set
{PM,Un} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,Un},{PM}} is finite V49() set
Bn . [PM,Un] is V35() real ext-real set
dom (T,Bn,PM) is Element of bool T
bbcT is set
dom Bn is Relation-like T -defined T -valued Element of bool [:T,T:]
bool [:T,T:] is non empty set
PM is set
FB is set
[PM,FB] is set
{PM,FB} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,FB},{PM}} is finite V49() set
TPM is Element of T
Un is Element of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
- 1 is V35() real ext-real non positive Element of REAL
Bn . bbcT is V35() real ext-real Element of REAL
PM is Element of T
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
bbcT is non empty Element of bool T
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
TPM is Element of T
(T,Bn,TPM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is non empty Element of bool T
(T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is non empty Element of bool T
(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
PM is Element of T
(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL
FB is V35() real ext-real set
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,PM) .: bbcT is V76() V77() V78() Element of bool REAL
dom (T,Bn,PM) is Element of bool T
TPM is set
(T,Bn,PM) . TPM is V35() real ext-real Element of REAL
Bn . (PM,TPM) is set
[PM,TPM] is set
{PM,TPM} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,TPM},{PM}} is finite V49() set
Bn . [PM,TPM] is V35() real ext-real set
lower_bound ((T,Bn,PM) .: bbcT) is V35() real ext-real Element of REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty non trivial non finite set
bool T is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of bool T
(T,Bn,bbcT) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
[:T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:T,REAL:] is non empty non trivial non finite set
PM is Element of T
(T,Bn,bbcT) . PM is V35() real ext-real Element of REAL
(T,Bn,PM) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
FB is non empty Element of bool T
(T,Bn,PM) .: FB is V76() V77() V78() Element of bool REAL
Bn . (PM,PM) is V35() real ext-real Element of REAL
[PM,PM] is set
{PM,PM} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,PM},{PM}} is finite V49() set
Bn . [PM,PM] is V35() real ext-real set
dom (T,Bn,PM) is Element of bool T
(T,Bn,PM) . PM is V35() real ext-real Element of REAL
lower_bound ((T,Bn,PM) .: FB) is V35() real ext-real Element of REAL
(T,Bn,FB) is Relation-like T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:T,REAL:]
(T,Bn,FB) . PM is V35() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
bbcT is Element of the carrier of T
PM is Element of the carrier of T
Bn . (bbcT,PM) is V35() real ext-real Element of REAL
[bbcT,PM] is set
{bbcT,PM} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,PM},{bbcT}} is finite V49() set
Bn . [bbcT,PM] is V35() real ext-real set
FB is non empty Element of bool the carrier of T
( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
( the carrier of T,Bn,FB) . bbcT is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . PM is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM) is V35() real ext-real Element of REAL
abs ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL
TPM is Element of the carrier of T
Un is Element of the carrier of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
- (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . Un is V35() real ext-real Element of REAL
( the carrier of T,Bn,FB) . TPM is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . Un) - (( the carrier of T,Bn,FB) . TPM) is V35() real ext-real Element of REAL
( the carrier of T,Bn,TPM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,TPM) .: FB is V76() V77() V78() Element of bool REAL
( the carrier of T,Bn,Un) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,Un) .: FB is V76() V77() V78() Element of bool REAL
lower_bound (( the carrier of T,Bn,TPM) .: FB) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,TPM) .: FB)) - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
UX is V35() real ext-real set
dom ( the carrier of T,Bn,Un) is Element of bool the carrier of T
UXk is set
( the carrier of T,Bn,Un) . UXk is V35() real ext-real Element of REAL
k is Element of the carrier of T
( the carrier of T,Bn,TPM) . k is V35() real ext-real Element of REAL
Bn . (TPM,k) is V35() real ext-real Element of REAL
[TPM,k] is set
{TPM,k} is finite set
{{TPM,k},{TPM}} is finite V49() set
Bn . [TPM,k] is V35() real ext-real set
Bn . (Un,k) is V35() real ext-real Element of REAL
[Un,k] is set
{Un,k} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,k},{Un}} is finite V49() set
Bn . [Un,k] is V35() real ext-real set
(Bn . (TPM,Un)) + (Bn . (Un,k)) is V35() real ext-real Element of REAL
dom ( the carrier of T,Bn,TPM) is Element of bool the carrier of T
(lower_bound (( the carrier of T,Bn,TPM) .: FB)) + 0 is V35() real ext-real Element of REAL
(Bn . (Un,k)) - 0 is V35() real ext-real Element of REAL
lower_bound (( the carrier of T,Bn,Un) .: FB) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,Un) .: FB)) - 0 is V35() real ext-real Element of REAL
0 - (Bn . (TPM,Un)) is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,Bn,Un) .: FB)) - (lower_bound (( the carrier of T,Bn,TPM) .: FB)) is V35() real ext-real Element of REAL
- (Bn . (bbcT,PM)) is V35() real ext-real Element of REAL
(( the carrier of T,Bn,FB) . PM) - (( the carrier of T,Bn,FB) . bbcT) is V35() real ext-real Element of REAL
- ((( the carrier of T,Bn,FB) . bbcT) - (( the carrier of T,Bn,FB) . PM)) is V35() real ext-real Element of REAL
Bn . (PM,bbcT) is V35() real ext-real Element of REAL
[PM,bbcT] is set
{PM,bbcT} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,bbcT},{PM}} is finite V49() set
Bn . [PM,bbcT] is V35() real ext-real set
- (Bn . (PM,bbcT)) is V35() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
bbcT is non empty Element of bool the carrier of T
( the carrier of T,Bn,bbcT) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
FB is Element of the carrier of T
( the carrier of T,Bn,FB) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
bool the carrier of R^1 is non empty set
PM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
PM . FB is V35() real ext-real Element of the carrier of R^1
PM . FB is V35() real ext-real Element of REAL
TPM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
TPM . FB is V35() real ext-real Element of REAL
UXk is V76() V77() V78() Element of bool the carrier of R^1
Un is V35() real ext-real Element of the carrier of RealSpace
k is V35() real ext-real set
Ball (Un,k) is V76() V77() V78() Element of bool the carrier of RealSpace
bool the carrier of RealSpace is non empty set
UX is V35() real ext-real Element of the carrier of RealSpace
Ball (UX,k) is V76() V77() V78() Element of bool the carrier of RealSpace
TPM . FB is V35() real ext-real Element of the carrier of R^1
(TPM . FB) - (TPM . FB) is V35() real ext-real set
abs ((TPM . FB) - (TPM . FB)) is V35() real ext-real Element of REAL
dist (UX,UX) is V35() real ext-real Element of REAL
UXk9 is V76() V77() V78() Element of bool the carrier of R^1
nm is Element of bool the carrier of T
TPM .: nm is V76() V77() V78() Element of bool the carrier of R^1
PM .: nm is V76() V77() V78() Element of bool the carrier of R^1
n is set
dom PM is Element of bool the carrier of T
m is set
PM . m is V35() real ext-real Element of REAL
Unn is Element of the carrier of T
PM . Unn is V35() real ext-real Element of REAL
TPM . Unn is V35() real ext-real Element of REAL
Bn . (FB,Unn) is V35() real ext-real Element of REAL
[FB,Unn] is set
{FB,Unn} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,Unn},{FB}} is finite V49() set
Bn . [FB,Unn] is V35() real ext-real set
TPM . Unn is V35() real ext-real Element of the carrier of R^1
Bn . (FB,FB) is V35() real ext-real Element of REAL
[FB,FB] is set
{FB,FB} is finite set
{{FB,FB},{FB}} is finite V49() set
Bn . [FB,FB] is V35() real ext-real set
B1 is V35() real ext-real Element of the carrier of RealSpace
dist (UX,B1) is V35() real ext-real Element of REAL
0 - (TPM . Unn) is V35() real ext-real Element of REAL
abs (0 - (TPM . Unn)) is V35() real ext-real Element of REAL
dom TPM is Element of bool the carrier of T
- (0 - (TPM . Unn)) is V35() real ext-real Element of REAL
abs (- (0 - (TPM . Unn))) is V35() real ext-real Element of REAL
( the carrier of T,Bn,bbcT) . FB is V35() real ext-real Element of REAL
( the carrier of T,Bn,bbcT) . Unn is V35() real ext-real Element of REAL
(( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn) is V35() real ext-real Element of REAL
abs ((( the carrier of T,Bn,bbcT) . FB) - (( the carrier of T,Bn,bbcT) . Unn)) is V35() real ext-real Element of REAL
B is V35() real ext-real Element of the carrier of RealSpace
dist (Un,B) is V35() real ext-real Element of REAL
T is set
[:T,T:] is set
[:[:T,T:],REAL:] is complex-valued ext-real-valued real-valued set
bool [:[:T,T:],REAL:] is non empty set
Bn is Relation-like [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[:T,T:],REAL:]
bbcT is Element of T
Bn . (bbcT,bbcT) is V35() real ext-real Element of REAL
[bbcT,bbcT] is set
{bbcT,bbcT} is finite set
{bbcT} is non empty trivial finite 1 -element set
{{bbcT,bbcT},{bbcT}} is finite V49() set
Bn . [bbcT,bbcT] is V35() real ext-real set
PM is Element of T
FB is Element of T
Bn . (PM,FB) is V35() real ext-real Element of REAL
[PM,FB] is set
{PM,FB} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,FB},{PM}} is finite V49() set
Bn . [PM,FB] is V35() real ext-real set
Bn . (FB,PM) is V35() real ext-real Element of REAL
[FB,PM] is set
{FB,PM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,PM},{FB}} is finite V49() set
Bn . [FB,PM] is V35() real ext-real set
TPM is Element of T
UX is Element of T
Bn . (TPM,UX) is V35() real ext-real Element of REAL
[TPM,UX] is set
{TPM,UX} is finite set
{TPM} is non empty trivial finite 1 -element set
{{TPM,UX},{TPM}} is finite V49() set
Bn . [TPM,UX] is V35() real ext-real set
Un is Element of T
Bn . (TPM,Un) is V35() real ext-real Element of REAL
[TPM,Un] is set
{TPM,Un} is finite set
{{TPM,Un},{TPM}} is finite V49() set
Bn . [TPM,Un] is V35() real ext-real set
Bn . (Un,UX) is V35() real ext-real Element of REAL
[Un,UX] is set
{Un,UX} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,UX},{Un}} is finite V49() set
Bn . [Un,UX] is V35() real ext-real set
(Bn . (TPM,Un)) + (Bn . (Un,UX)) is V35() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,Bn) is strict Reflexive discerning symmetric triangle MetrStruct
PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of PM is non empty set
FB is Element of the carrier of PM
TPM is Element of the carrier of PM
Bn . (FB,TPM) is set
[FB,TPM] is set
{FB,TPM} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,TPM},{FB}} is finite V49() set
Bn . [FB,TPM] is V35() real ext-real set
dist (FB,TPM) is V35() real ext-real Element of REAL
MetrStruct(# the carrier of T,Bn #) is strict MetrStruct
Family_open_set PM is Element of bool (bool the carrier of PM)
bool the carrier of PM is non empty set
bool (bool the carrier of PM) is non empty set
the topology of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
FB is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
Un is set
UX is Element of the carrier of PM
UXk is V35() real ext-real Element of REAL
Ball (UX,UXk) is Element of bool the carrier of PM
UXk9 is Element of bool the carrier of T
UXk9 ` is Element of bool the carrier of T
the carrier of T \ UXk9 is set
( the carrier of T,Bn,(UXk9 `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
{ b1 where b1 is Element of the carrier of T : ( the carrier of T,Bn,(UXk9 `)) . b1 = 0 } is set
n is set
n is set
m is set
( the carrier of T,Bn,(UXk9 `)) . m is V35() real ext-real Element of REAL
m is set
Unn is Element of the carrier of T
( the carrier of T,Bn,(UXk9 `)) . Unn is V35() real ext-real Element of REAL
( the carrier of T,Bn,Unn) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,Unn) .: (UXk9 `) is V76() V77() V78() Element of bool REAL
B is Element of the carrier of PM
B1 is V35() real ext-real Element of REAL
Ball (B,B1) is Element of bool the carrier of PM
lower_bound (( the carrier of T,Bn,Unn) .: (UXk9 `)) is V35() real ext-real Element of REAL
0 + B1 is V35() real ext-real Element of REAL
k is V35() real ext-real set
dom ( the carrier of T,Bn,Unn) is Element of bool the carrier of T
q is set
( the carrier of T,Bn,Unn) . q is V35() real ext-real Element of REAL
s is Element of the carrier of T
Bn . (Unn,s) is V35() real ext-real Element of REAL
[Unn,s] is set
{Unn,s} is finite set
{Unn} is non empty trivial finite 1 -element set
{{Unn,s},{Unn}} is finite V49() set
Bn . [Unn,s] is V35() real ext-real set
b is Element of the carrier of PM
dist (B,b) is V35() real ext-real Element of REAL
Cl (UXk9 `) is closed Element of bool the carrier of T
k is Element of the carrier of T
Bn . (k,k) is V35() real ext-real Element of REAL
[k,k] is set
{k,k} is finite set
{k} is non empty trivial finite 1 -element set
{{k,k},{k}} is finite V49() set
Bn . [k,k] is V35() real ext-real set
dist (UX,UX) is V35() real ext-real Element of REAL
UX is Element of bool the carrier of T
UXk is Element of bool the carrier of T
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
FB is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
[#] T is non empty non proper open closed Element of bool the carrier of T
([#] T) ` is open closed Element of bool the carrier of T
the carrier of T \ ([#] T) is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
Un is Element of bool the carrier of PM
UX is Element of the carrier of PM
( the carrier of T,Bn,(TPM `)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
UXk is Element of the carrier of T
( the carrier of T,Bn,(TPM `)) . UXk is V35() real ext-real Element of REAL
k is V35() real ext-real Element of REAL
Ball (UX,k) is Element of bool the carrier of PM
( the carrier of T,Bn,UXk) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,Bn,UXk) .: (TPM `) is V76() V77() V78() Element of bool REAL
UXk9 is set
nm is Element of the carrier of PM
dist (UX,nm) is V35() real ext-real Element of REAL
dom ( the carrier of T,Bn,UXk) is Element of bool the carrier of T
n is Element of the carrier of T
( the carrier of T,Bn,UXk) . n is V35() real ext-real Element of REAL
lower_bound (( the carrier of T,Bn,UXk) .: (TPM `)) is V35() real ext-real Element of REAL
Bn . (UXk,n) is V35() real ext-real Element of REAL
[UXk,n] is set
{UXk,n} is finite set
{UXk} is non empty trivial finite 1 -element set
{{UXk,n},{UXk}} is finite V49() set
Bn . [UXk,n] is V35() real ext-real set
Cl (TPM `) is closed Element of bool the carrier of T
{ b1 where b1 is Element of the carrier of T : ( the carrier of T,Bn,(TPM `)) . b1 = 0 } is set
TPM is Element of bool the carrier of T
TPM ` is Element of bool the carrier of T
the carrier of T \ TPM is set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
PFuncs ([: the carrier of T, the carrier of T:],REAL) is set
[:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is set
bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
bbcT is Relation-like NAT -defined PFuncs ([: the carrier of T, the carrier of T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):]
PM is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
FB is Element of the carrier of T
PM . (FB,FB) is V35() real ext-real Element of REAL
[FB,FB] is set
{FB,FB} is finite set
{FB} is non empty trivial finite 1 -element set
{{FB,FB},{FB}} is finite V49() set
PM . [FB,FB] is V35() real ext-real set
[FB,FB] is Element of [: the carrier of T, the carrier of T:]
bbcT # [FB,FB] is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
k is 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
bbcT . k is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
UXk9 . (FB,FB) is V35() real ext-real Element of REAL
UXk9 . [FB,FB] is V35() real ext-real set
(bbcT # [FB,FB]) . k is V35() real ext-real Element of REAL
0 * ((bbcT # [FB,FB]) . k) is V35() real ext-real Element of REAL
0 (#) (bbcT # [FB,FB]) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (bbcT # [FB,FB]) is V35() real ext-real Element of REAL
0 * (Sum (bbcT # [FB,FB])) is V35() real ext-real Element of REAL
Un is Element of the carrier of T
PM . (FB,Un) is V35() real ext-real Element of REAL
[FB,Un] is set
{FB,Un} is finite set
{{FB,Un},{FB}} is finite V49() set
PM . [FB,Un] is V35() real ext-real set
TPM is Element of the carrier of T
PM . (FB,TPM) is V35() real ext-real Element of REAL
[FB,TPM] is set
{FB,TPM} is finite set
{{FB,TPM},{FB}} is finite V49() set
PM . [FB,TPM] is V35() real ext-real set
PM . (Un,TPM) is V35() real ext-real Element of REAL
[Un,TPM] is set
{Un,TPM} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,TPM},{Un}} is finite V49() set
PM . [Un,TPM] is V35() real ext-real set
(PM . (FB,TPM)) + (PM . (Un,TPM)) is V35() real ext-real Element of REAL
[FB,TPM] is Element of [: the carrier of T, the carrier of T:]
[Un,TPM] is Element of [: the carrier of T, the carrier of T:]
[FB,Un] is Element of [: the carrier of T, the carrier of T:]
bbcT # [FB,Un] is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
bbcT # [FB,TPM] is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
bbcT # [Un,TPM] is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
m is 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
bbcT . m is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(bbcT . m) . [FB,Un] is V35() real ext-real Element of REAL
(bbcT # [FB,Un]) . m is V35() real ext-real Element of REAL
(bbcT . m) . [FB,TPM] is V35() real ext-real Element of REAL
(bbcT # [FB,TPM]) . m is V35() real ext-real Element of REAL
Unn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
Unn . (FB,Un) is V35() real ext-real Element of REAL
Unn . [FB,Un] is V35() real ext-real set
Unn . (FB,TPM) is V35() real ext-real Element of REAL
Unn . [FB,TPM] is V35() real ext-real set
Unn . (Un,TPM) is V35() real ext-real Element of REAL
Unn . [Un,TPM] is V35() real ext-real set
(Unn . (FB,TPM)) + (Unn . (Un,TPM)) is V35() real ext-real Element of REAL
(bbcT # [Un,TPM]) . m is V35() real ext-real Element of REAL
((bbcT # [FB,TPM]) . m) + ((bbcT # [Un,TPM]) . m) is V35() real ext-real Element of REAL
(bbcT # [FB,TPM]) + (bbcT # [Un,TPM]) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((bbcT # [FB,TPM]) + (bbcT # [Un,TPM])) . m is V35() real ext-real Element of REAL
Sum (bbcT # [FB,Un]) is V35() real ext-real Element of REAL
Sum ((bbcT # [FB,TPM]) + (bbcT # [Un,TPM])) is V35() real ext-real Element of REAL
Sum (bbcT # [FB,TPM]) is V35() real ext-real Element of REAL
PM . [FB,TPM] is V35() real ext-real Element of REAL
Sum (bbcT # [Un,TPM]) is V35() real ext-real Element of REAL
PM . [Un,TPM] is V35() real ext-real Element of REAL
(Sum (bbcT # [FB,TPM])) + (Sum (bbcT # [Un,TPM])) is V35() real ext-real Element of REAL
T is V35() real ext-real Element of REAL
Bn is 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
bbcT is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums bbcT is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
PM is 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
(Partial_Sums bbcT) . PM is V35() real ext-real Element of REAL
PM + 1 is 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
T * (PM + 1) is V35() real ext-real Element of REAL
(Partial_Sums bbcT) . (PM + 1) is V35() real ext-real Element of REAL
(PM + 1) + 1 is 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
T * ((PM + 1) + 1) is V35() real ext-real Element of REAL
bbcT . (PM + 1) is V35() real ext-real Element of REAL
((Partial_Sums bbcT) . PM) + (bbcT . (PM + 1)) is V35() real ext-real Element of REAL
(T * (PM + 1)) + T is V35() real ext-real Element of REAL
(Partial_Sums bbcT) . 0 is V35() real ext-real Element of REAL
bbcT . 0 is V35() real ext-real Element of REAL
0 + 1 is 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
T * (0 + 1) is V35() real ext-real Element of REAL
PM is 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
(Partial_Sums bbcT) . PM is V35() real ext-real Element of REAL
PM + 1 is 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
T * (PM + 1) is V35() real ext-real Element of REAL
T is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums T is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs T is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums (abs T) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
PM is 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
(Partial_Sums T) . PM is V35() real ext-real Element of REAL
abs ((Partial_Sums T) . PM) is V35() real ext-real Element of REAL
(Partial_Sums (abs T)) . PM is V35() real ext-real Element of REAL
PM + 1 is 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
(Partial_Sums T) . (PM + 1) is V35() real ext-real Element of REAL
abs ((Partial_Sums T) . (PM + 1)) is V35() real ext-real Element of REAL
(Partial_Sums (abs T)) . (PM + 1) is V35() real ext-real Element of REAL
T . (PM + 1) is V35() real ext-real Element of REAL
abs (T . (PM + 1)) is V35() real ext-real Element of REAL
(abs ((Partial_Sums T) . PM)) + (abs (T . (PM + 1))) is V35() real ext-real Element of REAL
((Partial_Sums (abs T)) . PM) + (abs (T . (PM + 1))) is V35() real ext-real Element of REAL
((Partial_Sums T) . PM) + (T . (PM + 1)) is V35() real ext-real Element of REAL
(abs T) . (PM + 1) is V35() real ext-real Element of REAL
((Partial_Sums (abs T)) . PM) + ((abs T) . (PM + 1)) is V35() real ext-real Element of REAL
(Partial_Sums (abs T)) . 0 is V35() real ext-real Element of REAL
(abs T) . 0 is V35() real ext-real Element of REAL
T . 0 is V35() real ext-real Element of REAL
abs (T . 0) is V35() real ext-real Element of REAL
(Partial_Sums T) . 0 is V35() real ext-real Element of REAL
abs ((Partial_Sums T) . 0) is V35() real ext-real Element of REAL
PM is 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
(Partial_Sums T) . PM is V35() real ext-real Element of REAL
abs ((Partial_Sums T) . PM) is V35() real ext-real Element of REAL
(Partial_Sums (abs T)) . PM is V35() real ext-real Element of REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
PFuncs ( the carrier of T,REAL) is set
[:NAT,(PFuncs ( the carrier of T,REAL)):] is set
bool [:NAT,(PFuncs ( the carrier of T,REAL)):] is non empty set
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
Bn is Relation-like NAT -defined PFuncs ( the carrier of T,REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ( the carrier of T,REAL)):]
bbcT is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
bool the carrier of R^1 is non empty set
PM is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
FB is Element of the carrier of T
PM . FB is V35() real ext-real Element of the carrier of R^1
bool the carrier of T is non empty set
PM . FB is V35() real ext-real Element of REAL
Un is V76() V77() V78() Element of bool the carrier of R^1
TPM is V35() real ext-real Element of the carrier of RealSpace
UX is V35() real ext-real set
Ball (TPM,UX) is V76() V77() V78() Element of bool the carrier of RealSpace
bool the carrier of RealSpace is non empty set
UX / 2 is V35() real ext-real Element of REAL
UX / 4 is V35() real ext-real Element of REAL
nm is V35() real ext-real Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
n is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums n is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (Partial_Sums n) is V35() real ext-real Element of REAL
m is 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
UXk9 is V35() real ext-real Element of REAL
m + 1 is 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
UXk9 / (m + 1) is V35() real ext-real Element of REAL
{0} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() Element of bool REAL
Seg m is finite m -element V76() V77() V78() V79() V80() V81() Element of bool NAT
{0} \/ (Seg m) is finite V76() V77() V78() V79() V80() V81() set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
Unn is set
Bn . Unn is set
B is 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
Bn . B is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
B1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
k is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
k . FB is V35() real ext-real Element of REAL
q is V35() real ext-real Element of the carrier of RealSpace
Ball (q,(UXk9 / (m + 1))) is V76() V77() V78() Element of bool the carrier of RealSpace
dist (q,q) is V35() real ext-real Element of REAL
b is V76() V77() V78() Element of bool the carrier of R^1
a is Element of bool the carrier of T
k .: a is V76() V77() V78() Element of bool the carrier of R^1
b is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
m is V35() real ext-real Element of the carrier of RealSpace
b . FB is V35() real ext-real Element of REAL
b .: a is V76() V77() V78() Element of bool REAL
Ball (m,(UXk9 / (m + 1))) is V76() V77() V78() Element of bool the carrier of RealSpace
[:({0} \/ (Seg m)),(bool the carrier of T):] is set
bool [:({0} \/ (Seg m)),(bool the carrier of T):] is non empty set
Unn is Relation-like {0} \/ (Seg m) -defined bool the carrier of T -valued Function-like total quasi_total finite Element of bool [:({0} \/ (Seg m)),(bool the carrier of T):]
B is 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
B1 is Element of the carrier of T
Bn # B1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Bn # B1) . B is V35() real ext-real Element of REAL
Bn . B is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
(Bn . B) . B1 is V35() real ext-real Element of REAL
k is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
n ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
B is 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
(n ^\ (m + 1)) . B is V35() real ext-real Element of REAL
Bn # FB is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(m + 1) + B is 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
(Bn # FB) . ((m + 1) + B) is V35() real ext-real Element of REAL
n . ((m + 1) + B) is V35() real ext-real Element of REAL
rng Unn is finite Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty set
B is Element of bool (bool the carrier of T)
B1 is Element of bool the carrier of T
dom Unn is finite V76() V77() V78() V79() V80() V81() Element of bool ({0} \/ (Seg m))
bool ({0} \/ (Seg m)) is non empty finite V49() set
k is set
Unn . k is set
Bn . k is set
q is Element of bool the carrier of T
Sum n is V35() real ext-real Element of REAL
(Partial_Sums n) . m is V35() real ext-real Element of REAL
Sum (n ^\ (m + 1)) is V35() real ext-real Element of REAL
((Partial_Sums n) . m) + (Sum (n ^\ (m + 1))) is V35() real ext-real Element of REAL
((Partial_Sums n) . m) - (lim (Partial_Sums n)) is V35() real ext-real Element of REAL
abs (((Partial_Sums n) . m) - (lim (Partial_Sums n))) is V35() real ext-real Element of REAL
- (Sum (n ^\ (m + 1))) is V35() real ext-real Element of REAL
abs (- (Sum (n ^\ (m + 1)))) is V35() real ext-real Element of REAL
abs (Sum (n ^\ (m + 1))) is V35() real ext-real Element of REAL
k is Element of the carrier of T
Bn # k is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Bn # k) ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum ((Bn # k) ^\ (m + 1)) is V35() real ext-real Element of REAL
s is 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
(m + 1) + s is 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
n . ((m + 1) + s) is V35() real ext-real Element of REAL
(n ^\ (m + 1)) . s is V35() real ext-real Element of REAL
(Bn # k) . ((m + 1) + s) is V35() real ext-real Element of REAL
((Bn # k) ^\ (m + 1)) . s is V35() real ext-real Element of REAL
s is 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
(Bn # k) . s is V35() real ext-real Element of REAL
b is 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
(Bn # k) . b is V35() real ext-real Element of REAL
n . b is V35() real ext-real Element of REAL
B1 is non empty Element of bool (bool the carrier of T)
meet B1 is Element of bool the carrier of T
PM .: (meet B1) is V76() V77() V78() Element of bool the carrier of R^1
k is set
dom PM is Element of bool the carrier of T
q is set
PM . q is V35() real ext-real Element of REAL
Bn # FB is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
s is Element of the carrier of T
Bn # s is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Bn # FB) ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Bn # s) ^\ (m + 1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Bn # FB) - (Bn # s) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
abs ((Bn # FB) - (Bn # s)) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums (abs ((Bn # FB) - (Bn # s))) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
m is 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
(abs ((Bn # FB) - (Bn # s))) . m is V35() real ext-real Element of REAL
Unn . m is set
dom ((Bn # FB) - (Bn # s)) is V76() V77() V78() V79() V80() V81() Element of bool NAT
((Bn # FB) - (Bn # s)) . m is V35() real ext-real Element of REAL
(Bn # FB) . m is V35() real ext-real Element of REAL
(Bn # s) . m is V35() real ext-real Element of REAL
((Bn # FB) . m) - ((Bn # s) . m) is V35() real ext-real Element of REAL
Bn . m is Relation-like the carrier of T -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
V is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
V . FB is V35() real ext-real Element of REAL
V . s is V35() real ext-real Element of REAL
V .: (Unn . m) is V76() V77() V78() Element of bool REAL
Ba is V35() real ext-real Element of the carrier of RealSpace
Ball (Ba,(UXk9 / (m + 1))) is V76() V77() V78() Element of bool the carrier of RealSpace
W is Element of bool the carrier of T
dom V is Element of bool the carrier of T
ca is V35() real ext-real Element of the carrier of RealSpace
dist (Ba,ca) is V35() real ext-real Element of REAL
(V . FB) - (V . s) is V35() real ext-real Element of REAL
abs ((V . FB) - (V . s)) is V35() real ext-real Element of REAL
abs (((Bn # FB) . m) - ((Bn # s) . m)) is V35() real ext-real Element of REAL
(Partial_Sums (abs ((Bn # FB) - (Bn # s)))) . m is V35() real ext-real Element of REAL
(UXk9 / (m + 1)) * (m + 1) is V35() real ext-real Element of REAL
Partial_Sums (Bn # FB) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums (Bn # s) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Partial_Sums ((Bn # FB) - (Bn # s)) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(Partial_Sums (Bn # FB)) - (Partial_Sums (Bn # s)) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
dom ((Partial_Sums (Bn # FB)) - (Partial_Sums (Bn # s))) is V76() V77() V78() V79() V80() V81() Element of bool NAT
(Partial_Sums (Bn # FB)) . m is V35() real ext-real Element of REAL
(Partial_Sums (Bn # s)) . m is V35() real ext-real Element of REAL
((Partial_Sums (Bn # FB)) . m) - ((Partial_Sums (Bn # s)) . m) is V35() real ext-real Element of REAL
abs (((Partial_Sums (Bn # FB)) . m) - ((Partial_Sums (Bn # s)) . m)) is V35() real ext-real Element of REAL
(Partial_Sums ((Bn # FB) - (Bn # s))) . m is V35() real ext-real Element of REAL
abs ((Partial_Sums ((Bn # FB) - (Bn # s))) . m) is V35() real ext-real Element of REAL
Sum ((Bn # FB) ^\ (m + 1)) is V35() real ext-real Element of REAL
abs (Sum ((Bn # FB) ^\ (m + 1))) is V35() real ext-real Element of REAL
Sum ((Bn # s) ^\ (m + 1)) is V35() real ext-real Element of REAL
abs (Sum ((Bn # s) ^\ (m + 1))) is V35() real ext-real Element of REAL
PM . s is V35() real ext-real Element of REAL
(Sum ((Bn # FB) ^\ (m + 1))) - (Sum ((Bn # s) ^\ (m + 1))) is V35() real ext-real Element of REAL
abs ((Sum ((Bn # FB) ^\ (m + 1))) - (Sum ((Bn # s) ^\ (m + 1)))) is V35() real ext-real Element of REAL
(abs (Sum ((Bn # FB) ^\ (m + 1)))) + (abs (Sum ((Bn # s) ^\ (m + 1)))) is V35() real ext-real Element of REAL
Sum (Bn # FB) is V35() real ext-real Element of REAL
ca is V35() real ext-real Element of the carrier of RealSpace
Sum (Bn # s) is V35() real ext-real Element of REAL
((Partial_Sums (Bn # FB)) . m) + (Sum ((Bn # FB) ^\ (m + 1))) is V35() real ext-real Element of REAL
((Partial_Sums (Bn # s)) . m) + (Sum ((Bn # s) ^\ (m + 1))) is V35() real ext-real Element of REAL
PM . s is V35() real ext-real Element of the carrier of R^1
(PM . FB) - (PM . s) is V35() real ext-real set
abs ((PM . FB) - (PM . s)) is V35() real ext-real Element of REAL
(((Partial_Sums (Bn # FB)) . m) - ((Partial_Sums (Bn # s)) . m)) + ((Sum ((Bn # FB) ^\ (m + 1))) - (Sum ((Bn # s) ^\ (m + 1)))) is V35() real ext-real Element of REAL
abs ((((Partial_Sums (Bn # FB)) . m) - ((Partial_Sums (Bn # s)) . m)) + ((Sum ((Bn # FB) ^\ (m + 1))) - (Sum ((Bn # s) ^\ (m + 1))))) is V35() real ext-real Element of REAL
(abs (((Partial_Sums (Bn # FB)) . m) - ((Partial_Sums (Bn # s)) . m))) + (abs ((Sum ((Bn # FB) ^\ (m + 1))) - (Sum ((Bn # s) ^\ (m + 1))))) is V35() real ext-real Element of REAL
nm + nm is V35() real ext-real Element of REAL
UXk9 + UXk9 is V35() real ext-real Element of REAL
dist (TPM,ca) is V35() real ext-real Element of REAL
k is set
dom Unn is finite V76() V77() V78() V79() V80() V81() Element of bool ({0} \/ (Seg m))
bool ({0} \/ (Seg m)) is non empty finite V49() set
q is set
Unn . q is set
Bn . q is set
s is Element of bool the carrier of T
1 / 2 is V35() real ext-real non negative Element of REAL
(1 / 2) GeoSeq is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
PFuncs ([: the carrier of T, the carrier of T:],REAL) is set
[:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is set
bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
FB is V35() real ext-real Element of REAL
TPM is Relation-like NAT -defined PFuncs ([: the carrier of T, the carrier of T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):]
FB (#) ((1 / 2) GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UX is Relation-like NAT -defined PFuncs ([: the carrier of T, the carrier of T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):]
PFuncs ( the carrier of [:T,T:],REAL) is set
[:NAT,(PFuncs ( the carrier of [:T,T:],REAL)):] is set
bool [:NAT,(PFuncs ( the carrier of [:T,T:],REAL)):] is non empty set
k is Element of [: the carrier of T, the carrier of T:]
UX # k is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UXk9 is 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
(UX # k) . UXk9 is V35() real ext-real Element of REAL
(FB (#) ((1 / 2) GeoSeq)) . UXk9 is V35() real ext-real Element of REAL
nm is set
n is set
[nm,n] is set
{nm,n} is finite set
{nm} is non empty trivial finite 1 -element set
{{nm,n},{nm}} is finite V49() set
TPM . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
B is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
m is Element of the carrier of T
Unn is Element of the carrier of T
B . (m,Unn) is V35() real ext-real Element of REAL
[m,Unn] is set
{m,Unn} is finite set
{m} is non empty trivial finite 1 -element set
{{m,Unn},{m}} is finite V49() set
B . [m,Unn] is V35() real ext-real set
((1 / 2) GeoSeq) . UXk9 is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) (#) (TPM . UXk9) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
dom ((((1 / 2) GeoSeq) . UXk9) (#) (TPM . UXk9)) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
(TPM . UXk9) . k is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * ((TPM . UXk9) . k) is V35() real ext-real Element of REAL
((((1 / 2) GeoSeq) . UXk9) (#) (TPM . UXk9)) . k is V35() real ext-real Element of REAL
UX . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(UX . UXk9) . k is V35() real ext-real Element of REAL
(1 / 2) |^ UXk9 is V35() real ext-real Element of REAL
B . k is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * (B . k) is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * FB is V35() real ext-real Element of REAL
UXk is Relation-like NAT -defined PFuncs ( the carrier of [:T,T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ( the carrier of [:T,T:],REAL)):]
k is 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
UXk . k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
TPM . k is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[: the carrier of [:T,T:], the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set
nm is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
n is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
((1 / 2) GeoSeq) . k is V35() real ext-real Element of REAL
m is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
Unn is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
dom Unn is Element of bool the carrier of [:T,T:]
bool the carrier of [:T,T:] is non empty set
dom UXk9 is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
(((1 / 2) GeoSeq) . k) (#) (TPM . k) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
dom (TPM . k) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
dom (UXk . k) is Element of bool the carrier of [:T,T:]
B is Element of the carrier of [:T,T:]
(UXk . k) . B is V35() real ext-real Element of REAL
UXk9 . B is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . k) * (UXk9 . B) is V35() real ext-real Element of REAL
Unn . B is V35() real ext-real Element of REAL
B is Element of the carrier of [:T,T:]
(UXk . k) . B is V35() real ext-real Element of REAL
B1 is Element of [: the carrier of T, the carrier of T:]
UX # B1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(UX # B1) . k is V35() real ext-real Element of REAL
Unn . B is V35() real ext-real Element of REAL
B is Element of the carrier of [:T,T:]
Unn . B is V35() real ext-real Element of REAL
k is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
UXk9 is Element of [: the carrier of T, the carrier of T:]
k . UXk9 is V35() real ext-real Element of REAL
UX # UXk9 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (UX # UXk9) is V35() real ext-real Element of REAL
nm is set
n is 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
TPM . n is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
((1 / 2) GeoSeq) . n is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . n) (#) (TPM . n) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
dom ((((1 / 2) GeoSeq) . n) (#) (TPM . n)) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
m is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(TPM . n) . UXk9 is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . n) * ((TPM . n) . UXk9) is V35() real ext-real Element of REAL
((((1 / 2) GeoSeq) . n) (#) (TPM . n)) . UXk9 is V35() real ext-real Element of REAL
UX . n is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(UX . n) . UXk9 is V35() real ext-real Element of REAL
(UX # UXk9) . n is V35() real ext-real Element of REAL
TPM # UXk9 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(TPM # UXk9) . n is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . n) * ((TPM # UXk9) . n) is V35() real ext-real Element of REAL
((1 / 2) GeoSeq) (#) (TPM # UXk9) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(((1 / 2) GeoSeq) (#) (TPM # UXk9)) . n is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) (#) (TPM # UXk9)) . nm is V35() real ext-real Element of REAL
(UX # UXk9) . nm is V35() real ext-real Element of REAL
UXk9 is 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
UX . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
TPM . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
nm is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
((1 / 2) GeoSeq) . UXk9 is V35() real ext-real Element of REAL
n is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(1 / 2) |^ UXk9 is V35() real ext-real Element of REAL
m is Element of the carrier of T
B is Element of the carrier of T
nm . (m,B) is V35() real ext-real Element of REAL
[m,B] is set
{m,B} is finite set
{m} is non empty trivial finite 1 -element set
{{m,B},{m}} is finite V49() set
nm . [m,B] is V35() real ext-real set
Unn is Element of the carrier of T
nm . (m,Unn) is V35() real ext-real Element of REAL
[m,Unn] is set
{m,Unn} is finite set
{{m,Unn},{m}} is finite V49() set
nm . [m,Unn] is V35() real ext-real set
nm . (B,Unn) is V35() real ext-real Element of REAL
[B,Unn] is set
{B,Unn} is finite set
{B} is non empty trivial finite 1 -element set
{{B,Unn},{B}} is finite V49() set
nm . [B,Unn] is V35() real ext-real set
(nm . (m,Unn)) + (nm . (B,Unn)) is V35() real ext-real Element of REAL
(nm . (m,B)) * (((1 / 2) GeoSeq) . UXk9) is V35() real ext-real Element of REAL
((nm . (m,Unn)) + (nm . (B,Unn))) * (((1 / 2) GeoSeq) . UXk9) is V35() real ext-real Element of REAL
n . (m,B) is V35() real ext-real Element of REAL
n . [m,B] is V35() real ext-real set
(((1 / 2) GeoSeq) . UXk9) * (nm . (m,Unn)) is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * (nm . (B,Unn)) is V35() real ext-real Element of REAL
((((1 / 2) GeoSeq) . UXk9) * (nm . (m,Unn))) + ((((1 / 2) GeoSeq) . UXk9) * (nm . (B,Unn))) is V35() real ext-real Element of REAL
n . (m,m) is V35() real ext-real Element of REAL
[m,m] is set
{m,m} is finite set
{{m,m},{m}} is finite V49() set
n . [m,m] is V35() real ext-real set
nm . (m,m) is V35() real ext-real Element of REAL
nm . [m,m] is V35() real ext-real set
(((1 / 2) GeoSeq) . UXk9) * (nm . (m,m)) is V35() real ext-real Element of REAL
n . (m,Unn) is V35() real ext-real Element of REAL
n . [m,Unn] is V35() real ext-real set
n . (B,Unn) is V35() real ext-real Element of REAL
n . [B,Unn] is V35() real ext-real set
(n . (m,Unn)) + (n . (B,Unn)) is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) (#) (TPM . UXk9) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
dom (TPM . UXk9) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
bool [: the carrier of T, the carrier of T:] is non empty set
dom (UX . UXk9) is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
m is set
Unn is set
[m,Unn] is set
{m,Unn} is finite set
{m} is non empty trivial finite 1 -element set
{{m,Unn},{m}} is finite V49() set
B is Element of the carrier of T
B1 is Element of the carrier of T
n . (B,B1) is V35() real ext-real Element of REAL
[B,B1] is set
{B,B1} is finite set
{B} is non empty trivial finite 1 -element set
{{B,B1},{B}} is finite V49() set
n . [B,B1] is V35() real ext-real set
nm . (B,B1) is V35() real ext-real Element of REAL
nm . [B,B1] is V35() real ext-real set
(((1 / 2) GeoSeq) . UXk9) * (nm . (B,B1)) is V35() real ext-real Element of REAL
(UX . UXk9) . (m,Unn) is set
(UX . UXk9) . [m,Unn] is V35() real ext-real set
n . (m,Unn) is set
n . [m,Unn] is V35() real ext-real set
dom nm is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
dom n is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]
abs (1 / 2) is V35() real ext-real Element of REAL
UXk9 is Element of [: the carrier of T, the carrier of T:]
UX # UXk9 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
nm is Element of the carrier of [:T,T:]
UXk # nm is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
n is 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
(UX # UXk9) . n is V35() real ext-real Element of REAL
UX . n is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(UX . n) . UXk9 is V35() real ext-real Element of REAL
(UXk # nm) . n is V35() real ext-real Element of REAL
nm is Element of the carrier of [:T,T:]
UXk # nm is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UXk9 is 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
(UXk # nm) . UXk9 is V35() real ext-real Element of REAL
n is Element of [: the carrier of T, the carrier of T:]
UX # n is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(UX # n) . UXk9 is V35() real ext-real Element of REAL
(FB (#) ((1 / 2) GeoSeq)) . UXk9 is V35() real ext-real Element of REAL
nm is Element of the carrier of [:T,T:]
UXk # nm is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UXk9 is 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
(UXk # nm) . UXk9 is V35() real ext-real Element of REAL
(FB (#) ((1 / 2) GeoSeq)) . UXk9 is V35() real ext-real Element of REAL
UXk9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
nm is Element of the carrier of [:T,T:]
UXk9 . nm is V35() real ext-real Element of REAL
UXk # nm is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (UXk # nm) is V35() real ext-real Element of REAL
n is Element of [: the carrier of T, the carrier of T:]
k . n is V35() real ext-real Element of REAL
UX # n is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (UX # n) is V35() real ext-real Element of REAL
nm is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UXk9 is Element of [: the carrier of T, the carrier of T:]
UX # UXk9 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
nm is 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
(UX # UXk9) . nm is V35() real ext-real Element of REAL
n is 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
(UX # UXk9) . n is V35() real ext-real Element of REAL
(FB (#) ((1 / 2) GeoSeq)) . n is V35() real ext-real Element of REAL
UXk9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
bbcT is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
PM is non empty Element of bool the carrier of T
Cl PM is closed Element of bool the carrier of T
( the carrier of T,bbcT,PM) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
FB is Element of the carrier of T
( the carrier of T,bbcT,PM) . FB is V35() real ext-real Element of REAL
dom ( the carrier of T,bbcT,PM) is Element of bool the carrier of T
bool the carrier of R^1 is non empty set
{0} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() Element of bool REAL
( the carrier of T,bbcT,PM) .: PM is V76() V77() V78() Element of bool REAL
Un is V76() V77() V78() Element of bool the carrier of R^1
TPM is V76() V77() V78() Element of bool the carrier of R^1
UX is set
UXk is set
( the carrier of T,bbcT,PM) . UXk is V35() real ext-real Element of REAL
Cl Un is V76() V77() V78() closed Element of bool the carrier of R^1
Cl TPM is V76() V77() V78() closed Element of bool the carrier of R^1
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
UXk is Element of the carrier of T
( the carrier of T,bbcT,UXk) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
UX is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
UX .: (Cl PM) is V76() V77() V78() Element of bool the carrier of R^1
UX .: PM is V76() V77() V78() Element of bool the carrier of R^1
Cl (UX .: PM) is V76() V77() V78() closed Element of bool the carrier of R^1
( the carrier of T,bbcT,PM) .: (Cl PM) is V76() V77() V78() Element of bool REAL
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
[: the carrier of T, the carrier of T:] is non empty set
PFuncs ([: the carrier of T, the carrier of T:],REAL) is set
[:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is set
bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
bool the carrier of T is non empty set
PM is V35() real ext-real Element of REAL
FB is Relation-like NAT -defined PFuncs ([: the carrier of T, the carrier of T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):]
TPM is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
Un is Element of [: the carrier of T, the carrier of T:]
TPM . Un is V35() real ext-real Element of REAL
FB # Un is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((1 / 2) GeoSeq) (#) (FB # Un) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (((1 / 2) GeoSeq) (#) (FB # Un)) is V35() real ext-real Element of REAL
UX is set
UXk is set
[UX,UXk] is set
{UX,UXk} is finite set
{UX} is non empty trivial finite 1 -element set
{{UX,UXk},{UX}} is finite V49() set
TPM . (UX,UXk) is set
TPM . [UX,UXk] is V35() real ext-real set
PM (#) ((1 / 2) GeoSeq) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Un is Element of [: the carrier of T, the carrier of T:]
FB # Un is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((1 / 2) GeoSeq) (#) (FB # Un) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
UX is 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
(((1 / 2) GeoSeq) (#) (FB # Un)) . UX is V35() real ext-real Element of REAL
(PM (#) ((1 / 2) GeoSeq)) . UX is V35() real ext-real Element of REAL
UXk is set
k is set
[UXk,k] is set
{UXk,k} is finite set
{UXk} is non empty trivial finite 1 -element set
{{UXk,k},{UXk}} is finite V49() set
((1 / 2) GeoSeq) . UX is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UX) * PM is V35() real ext-real Element of REAL
(1 / 2) |^ UX is V35() real ext-real Element of REAL
FB . UX is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
n is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
UXk9 is Element of the carrier of T
nm is Element of the carrier of T
n . (UXk9,nm) is V35() real ext-real Element of REAL
[UXk9,nm] is set
{UXk9,nm} is finite set
{UXk9} is non empty trivial finite 1 -element set
{{UXk9,nm},{UXk9}} is finite V49() set
n . [UXk9,nm] is V35() real ext-real set
n . Un is V35() real ext-real Element of REAL
(FB # Un) . UX is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UX) * ((FB # Un) . UX) is V35() real ext-real Element of REAL
Un is Element of the carrier of T
UX is Element of the carrier of T
TPM . (Un,UX) is V35() real ext-real Element of REAL
[Un,UX] is set
{Un,UX} is finite set
{Un} is non empty trivial finite 1 -element set
{{Un,UX},{Un}} is finite V49() set
TPM . [Un,UX] is V35() real ext-real set
{UX} is non empty trivial finite 1 -element Element of bool the carrier of T
[Un,UX] is Element of [: the carrier of T, the carrier of T:]
FB # [Un,UX] is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((1 / 2) GeoSeq) (#) (FB # [Un,UX]) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
Sum (((1 / 2) GeoSeq) (#) (FB # [Un,UX])) is V35() real ext-real Element of REAL
UXk9 is 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
(((1 / 2) GeoSeq) (#) (FB # [Un,UX])) . UXk9 is V35() real ext-real Element of REAL
nm is 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
(((1 / 2) GeoSeq) (#) (FB # [Un,UX])) . nm is V35() real ext-real Element of REAL
(PM (#) ((1 / 2) GeoSeq)) . nm is V35() real ext-real Element of REAL
UXk9 is 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
FB . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
nm is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
( the carrier of T,nm,{UX}) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
( the carrier of T,nm,{UX}) . Un is V35() real ext-real Element of REAL
( the carrier of T,nm,Un) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,nm,Un) .: {UX} is finite V76() V77() V78() Element of bool REAL
lower_bound (( the carrier of T,nm,Un) .: {UX}) is V35() real ext-real Element of REAL
abs (1 / 2) is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) (#) (FB # [Un,UX])) . UXk9 is V35() real ext-real Element of REAL
((1 / 2) GeoSeq) . UXk9 is V35() real ext-real Element of REAL
(FB # [Un,UX]) . UXk9 is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * ((FB # [Un,UX]) . UXk9) is V35() real ext-real Element of REAL
(1 / 2) |^ UXk9 is V35() real ext-real Element of REAL
nm . (Un,UX) is V35() real ext-real Element of REAL
nm . [Un,UX] is V35() real ext-real set
( the carrier of T,nm,Un) . UX is V35() real ext-real Element of REAL
dom ( the carrier of T,nm,Un) is Element of bool the carrier of T
Un is non empty Element of bool the carrier of T
Cl Un is closed Element of bool the carrier of T
( the carrier of T,TPM,Un) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
{ b1 where b1 is Element of the carrier of T : ( the carrier of T,TPM,Un) . b1 = 0 } is set
UXk is set
k is Element of the carrier of T
( the carrier of T,TPM,Un) . k is V35() real ext-real Element of REAL
( the carrier of T,TPM,k) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,TPM,k) .: Un is V76() V77() V78() Element of bool REAL
lower_bound (( the carrier of T,TPM,k) .: Un) is V35() real ext-real Element of REAL
UXk9 is set
UXk9 is 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
FB . UXk9 is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
(1 / 2) |^ UXk9 is V35() real ext-real Element of REAL
((1 / 2) GeoSeq) . UXk9 is V35() real ext-real Element of REAL
nm is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
( the carrier of T,nm,(Cl Un)) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,nm,(Cl Un)) . k is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * (( the carrier of T,nm,(Cl Un)) . k) is V35() real ext-real Element of REAL
( the carrier of T,nm,k) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,nm,k) .: (Cl Un) is V76() V77() V78() Element of bool REAL
lower_bound (( the carrier of T,nm,k) .: (Cl Un)) is V35() real ext-real Element of REAL
((((1 / 2) GeoSeq) . UXk9) * (( the carrier of T,nm,(Cl Un)) . k)) / 2 is V35() real ext-real Element of REAL
(lower_bound (( the carrier of T,TPM,k) .: Un)) + (((((1 / 2) GeoSeq) . UXk9) * (( the carrier of T,nm,(Cl Un)) . k)) / 2) is V35() real ext-real Element of REAL
m is V35() real ext-real set
dom ( the carrier of T,TPM,k) is Element of bool the carrier of T
Unn is set
( the carrier of T,TPM,k) . Unn is V35() real ext-real Element of REAL
B is Element of the carrier of T
[k,B] is Element of [: the carrier of T, the carrier of T:]
{k,B} is finite set
{k} is non empty trivial finite 1 -element set
{{k,B},{k}} is finite V49() set
( the carrier of T,nm,k) . B is V35() real ext-real Element of REAL
nm . (k,B) is V35() real ext-real Element of REAL
[k,B] is set
nm . [k,B] is V35() real ext-real set
dom ( the carrier of T,nm,k) is Element of bool the carrier of T
B1 is Element of [: the carrier of T, the carrier of T:]
FB # B1 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(FB # B1) . UXk9 is V35() real ext-real Element of REAL
(((1 / 2) GeoSeq) . UXk9) * ((FB # B1) . UXk9) is V35() real ext-real Element of REAL
((1 / 2) GeoSeq) (#) (FB # B1) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(((1 / 2) GeoSeq) (#) (FB # B1)) . UXk9 is V35() real ext-real Element of REAL
k is 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
(((1 / 2) GeoSeq) (#) (FB # B1)) . k is V35() real ext-real Element of REAL
q is 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
(((1 / 2) GeoSeq) (#) (FB # B1)) . q is V35() real ext-real Element of REAL
(PM (#) ((1 / 2) GeoSeq)) . q is V35() real ext-real Element of REAL
TPM . B1 is V35() real ext-real Element of REAL
TPM . (k,B) is V35() real ext-real Element of REAL
TPM . [k,B] is V35() real ext-real set
abs (1 / 2) is V35() real ext-real Element of REAL
Sum (((1 / 2) GeoSeq) (#) (FB # B1)) is V35() real ext-real Element of REAL
UXk is set
UXk9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
k is Element of the carrier of T
( the carrier of T,TPM,Un) . k is V35() real ext-real Element of REAL
T is non empty set
[:T,T:] is non empty set
[:[:T,T:],T:] is non empty set
bool [:[:T,T:],T:] is non empty set
Bn is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
bbcT is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
rng bbcT is finite Element of bool T
bool T is non empty set
rng Bn is finite Element of bool T
len bbcT is 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
len Bn is 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
(rng Bn) \ (rng bbcT) is finite Element of bool T
PM is Relation-like [:T,T:] -defined T -valued Function-like non empty total quasi_total Element of bool [:[:T,T:],T:]
PM "**" Bn is Element of T
PM "**" bbcT is Element of T
card (rng Bn) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of omega
FB is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng FB is finite set
TPM is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
bbcT ^ TPM is Relation-like NAT -defined T -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of T
rng (bbcT ^ TPM) is finite Element of bool T
(rng bbcT) \/ ((rng Bn) \ (rng bbcT)) is finite Element of bool T
rng TPM is finite Element of bool T
card (rng (bbcT ^ TPM)) is epsilon-transitive epsilon-connected ordinal natural V35() real V37() ext-real non negative finite cardinal V65() V76() V77() V78() V79() V80() V81() Element of omega
len (bbcT ^ TPM) is 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
len TPM is 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
(len bbcT) + (len TPM) is 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
dom Bn is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
[:(dom Bn),(dom Bn):] is RAT -valued INT -valued finite complex-valued ext-real-valued real-valued natural-valued set
bool [:(dom Bn),(dom Bn):] is non empty finite V49() set
PM "**" (bbcT ^ TPM) is Element of T
Un is Relation-like dom Bn -defined dom Bn -valued Function-like one-to-one total quasi_total onto bijective finite complex-valued ext-real-valued real-valued natural-valued Element of bool [:(dom Bn),(dom Bn):]
Bn * Un is Relation-like dom Bn -defined T -valued Function-like finite Element of bool [:(dom Bn),T:]
[:(dom Bn),T:] is set
bool [:(dom Bn),T:] is non empty set
dom Un is finite V76() V77() V78() V79() V80() V81() Element of bool (dom Bn)
bool (dom Bn) is non empty finite V49() set
rng Un is finite V76() V77() V78() V79() V80() V81() Element of bool (dom Bn)
PM "**" TPM is Element of T
PM . ((PM "**" bbcT),(PM "**" TPM)) is Element of T
[(PM "**" bbcT),(PM "**" TPM)] is set
{(PM "**" bbcT),(PM "**" TPM)} is finite set
{(PM "**" bbcT)} is non empty trivial finite 1 -element set
{{(PM "**" bbcT),(PM "**" TPM)},{(PM "**" bbcT)}} is finite V49() set
PM . [(PM "**" bbcT),(PM "**" TPM)] is set
T is TopSpace-like TopStruct
Bn is TopSpace-like TopStruct
[:T,Bn:] is strict TopSpace-like TopStruct
the carrier of [:T,Bn:] is set
[: the carrier of [:T,Bn:],REAL:] is complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,Bn:],REAL:] is non empty set
the carrier of T is set
the carrier of Bn is set
bbcT is Relation-like the carrier of [:T,Bn:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,Bn:],REAL:]
PM is Element of the carrier of T
FB is Element of the carrier of Bn
bbcT . (PM,FB) is set
[PM,FB] is set
{PM,FB} is finite set
{PM} is non empty trivial finite 1 -element set
{{PM,FB},{PM}} is finite V49() set
bbcT . [PM,FB] is V35() real ext-real set
() /" is Relation-like NAT -defined [:NAT,NAT:] -valued Function-like non empty total quasi_total Element of bool [:NAT,[:NAT,NAT:]:]
[:NAT,[:NAT,NAT:]:] is non empty non trivial non finite set
bool [:NAT,[:NAT,NAT:]:] is non empty non trivial non finite set
() " is Relation-like Function-like set
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
[:T,T:] is non empty strict TopSpace-like TopStruct
the carrier of [:T,T:] is non empty set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
Funcs ( the carrier of [:T,T:],REAL) is functional non empty FUNCTION_DOMAIN of the carrier of [:T,T:], REAL
TPM is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
TPM is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
[: the carrier of [:T,T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:],REAL:] is non empty non trivial non finite set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
Union TPM is Element of bool (bool the carrier of T)
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
Un is 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
TPM . Un is set
UX is 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
TPM . UX is set
TPM . UX is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= a1 ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= a1 ) } is set
TPM . Un is Element of bool (bool the carrier of T)
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses a1 ) } is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses a2 ) } is set
k is set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= k ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= k ) } is set
nm is set
n is set
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
[:(bool the carrier of T),(bool the carrier of T):] is non empty set
bool [:(bool the carrier of T),(bool the carrier of T):] is non empty set
k is Relation-like bool the carrier of T -defined bool the carrier of T -valued Function-like non empty total quasi_total Element of bool [:(bool the carrier of T),(bool the carrier of T):]
UXk9 is Element of bool the carrier of T
k . UXk9 is Element of bool the carrier of T
Cl (k . UXk9) is closed Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= UXk9 ) } is set
n is set
m is Element of bool the carrier of T
Cl m is closed Element of bool the carrier of T
n is Element of bool (bool the carrier of T)
clf n is Element of bool (bool the carrier of T)
union (clf n) is Element of bool the carrier of T
m is set
Unn is set
B is Element of bool the carrier of T
B1 is Element of bool the carrier of T
Cl B1 is closed Element of bool the carrier of T
k is Element of bool the carrier of T
Cl k is closed Element of bool the carrier of T
m is set
Unn is Element of bool the carrier of T
Cl Unn is closed Element of bool the carrier of T
union n is Element of bool the carrier of T
Cl (union n) is closed Element of bool the carrier of T
Funcs ( the carrier of T,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of T, REAL
UXk9 is set
the topology of T is non empty Element of bool (bool the carrier of T)
nm is open Element of bool the carrier of T
nm ` is closed Element of bool the carrier of T
the carrier of T \ nm is set
k . nm is Element of bool the carrier of T
Cl (k . nm) is closed Element of bool the carrier of T
[: the carrier of T, the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of T, the carrier of R^1:] is non empty set
n is Relation-like the carrier of T -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T, the carrier of R^1:]
m is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn is Element of the carrier of T
m . Unn is V35() real ext-real Element of REAL
B is Element of the carrier of T
m . B is V35() real ext-real Element of REAL
B1 is Element of the carrier of T
m . B1 is V35() real ext-real Element of REAL
k is Element of the carrier of T
m . k is V35() real ext-real Element of REAL
B is Element of bool the carrier of T
Unn is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
B ` is Element of bool the carrier of T
the carrier of T \ B is set
k . B is Element of bool the carrier of T
Cl (k . B) is closed Element of bool the carrier of T
[:(TPM . Un),(Funcs ( the carrier of T,REAL)):] is set
bool [:(TPM . Un),(Funcs ( the carrier of T,REAL)):] is non empty set
UXk9 is Relation-like TPM . Un -defined Funcs ( the carrier of T,REAL) -valued Function-like total quasi_total Element of bool [:(TPM . Un),(Funcs ( the carrier of T,REAL)):]
nm is Element of the carrier of T
[: the carrier of T,(bool the carrier of T):] is non empty set
bool [: the carrier of T,(bool the carrier of T):] is non empty set
nm is Relation-like the carrier of T -defined bool the carrier of T -valued Function-like non empty total quasi_total Element of bool [: the carrier of T,(bool the carrier of T):]
bool the carrier of [:T,T:] is non empty Element of bool (bool the carrier of [:T,T:])
bool the carrier of [:T,T:] is non empty set
bool (bool the carrier of [:T,T:]) is non empty set
n is set
m is set
Unn is set
[m,Unn] is set
{m,Unn} is finite set
{m} is non empty trivial finite 1 -element set
{{m,Unn},{m}} is finite V49() set
k is Element of the carrier of T
q is Element of the carrier of T
[k,q] is Element of [: the carrier of T, the carrier of T:]
{k,q} is finite set
{k} is non empty trivial finite 1 -element set
{{k,q},{k}} is finite V49() set
B is Element of the carrier of T
nm . B is Element of bool the carrier of T
B1 is Element of the carrier of T
nm . B1 is Element of bool the carrier of T
[:(nm . B),(nm . B1):] is Element of bool the carrier of [:T,T:]
nm . k is Element of bool the carrier of T
nm . q is Element of bool the carrier of T
[:(nm . k),(nm . q):] is Element of bool the carrier of [:T,T:]
[: the carrier of [:T,T:],(bool the carrier of [:T,T:]):] is non empty set
bool [: the carrier of [:T,T:],(bool the carrier of [:T,T:]):] is non empty set
n is Relation-like the carrier of [:T,T:] -defined bool the carrier of [:T,T:] -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T,T:],(bool the carrier of [:T,T:]):]
m is Element of the carrier of [:T,T:]
n . m is Element of bool the carrier of [:T,T:]
Unn is set
B is set
[Unn,B] is set
{Unn,B} is finite set
{Unn} is non empty trivial finite 1 -element set
{{Unn,B},{Unn}} is finite V49() set
B1 is Element of the carrier of T
nm . B1 is Element of bool the carrier of T
k is Element of the carrier of T
nm . k is Element of bool the carrier of T
[:(nm . B1),(nm . k):] is Element of bool the carrier of [:T,T:]
m is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
Unn is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
m + Unn is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
[:(Funcs ( the carrier of [:T,T:],REAL)),(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
[:[:(Funcs ( the carrier of [:T,T:],REAL)),(Funcs ( the carrier of [:T,T:],REAL)):],(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
bool [:[:(Funcs ( the carrier of [:T,T:],REAL)),(Funcs ( the carrier of [:T,T:],REAL)):],(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
m is Relation-like [:(Funcs ( the carrier of [:T,T:],REAL)),(Funcs ( the carrier of [:T,T:],REAL)):] -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:[:(Funcs ( the carrier of [:T,T:],REAL)),(Funcs ( the carrier of [:T,T:],REAL)):],(Funcs ( the carrier of [:T,T:],REAL)):]
Unn is Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of T,REAL)
B is Element of the carrier of T
Unn . B is V35() real ext-real Element of REAL
B1 is Element of the carrier of T
Unn . B1 is V35() real ext-real Element of REAL
(Unn . B) - (Unn . B1) is V35() real ext-real Element of REAL
abs ((Unn . B) - (Unn . B1)) is V35() real ext-real Element of REAL
B is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
bool [:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
Unn is Relation-like Funcs ( the carrier of T,REAL) -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:(Funcs ( the carrier of T,REAL)),(Funcs ( the carrier of [:T,T:],REAL)):]
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . a1 ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . a1) ) } is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in a1 } is set
B is Element of the carrier of T
nm . B is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . B ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . B) ) } is set
{ H5(b1) where b1 is Element of bool the carrier of T : b1 in H2(nm . B) } is set
k is set
q is Element of bool the carrier of T
UXk9 . q is Relation-like Function-like set
B is Element of the carrier of T
nm . B is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . B ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . B) ) } is set
B1 is Element of the carrier of T
nm . B1 is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . B1 ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . B1) ) } is set
H3(B) \/ H3(B1) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(B) \/ H3(B1) } is set
k is set
q is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . q is Relation-like Function-like set
{ H5(b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of T,REAL) : b1 in H3(B) \/ H3(B1) } is set
q is set
s is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . s is Relation-like Function-like set
(Funcs ( the carrier of [:T,T:],REAL)) * is functional non empty FinSequence-membered set
B is Element of the carrier of [:T,T:]
B1 is set
k is set
[B1,k] is set
{B1,k} is finite set
{B1} is non empty trivial finite 1 -element set
{{B1,k},{B1}} is finite V49() set
q is Element of the carrier of T
nm . q is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . q ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . q) ) } is set
s is Element of the carrier of T
nm . s is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . s ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . s) ) } is set
H3(q) \/ H3(s) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(q) \/ H3(s) } is set
b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng b is finite set
a is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
[: the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *):] is non empty set
bool [: the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *):] is non empty set
B is Relation-like the carrier of [:T,T:] -defined (Funcs ( the carrier of [:T,T:],REAL)) * -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T,T:],((Funcs ( the carrier of [:T,T:],REAL)) *):]
B1 is set
B . B1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
k is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
m "**" k is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
q is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
m "**" q is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
bool [: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)):] is non empty set
B1 is Relation-like the carrier of [:T,T:] -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:],REAL)):]
Funcs ( the carrier of [:T,T:], the carrier of R^1) is functional non empty FUNCTION_DOMAIN of the carrier of [:T,T:], the carrier of R^1
[: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:], the carrier of R^1)):] is non empty set
bool [: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:], the carrier of R^1)):] is non empty set
k is Relation-like the carrier of [:T,T:] -defined Funcs ( the carrier of [:T,T:], the carrier of R^1) -valued Function-like non empty total quasi_total Element of bool [: the carrier of [:T,T:],(Funcs ( the carrier of [:T,T:], the carrier of R^1)):]
k Toler is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
[: the carrier of [:T,T:], the carrier of R^1:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of [:T,T:], the carrier of R^1:] is non empty set
b is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
a is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . (b,a) is set
[b,a] is set
{b,a} is functional finite set
{b} is functional non empty trivial finite 1 -element set
{{b,a},{b}} is finite V49() set
m . [b,a] is Relation-like Function-like set
b + a is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
b is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
m is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
m . (b,m) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[b,m] is set
{b,m} is functional finite set
{b} is functional non empty trivial finite 1 -element set
{{b,m},{b}} is finite V49() set
m . [b,m] is Relation-like Function-like set
b + m is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
q is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
b is Element of the carrier of T
a is Element of the carrier of T
[b,a] is Element of [: the carrier of T, the carrier of T:]
{b,a} is finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is finite V49() set
q . [b,a] is V35() real ext-real Element of REAL
b is Element of bool the carrier of T
m is Element of bool the carrier of T
Cl b is closed Element of bool the carrier of T
b is Element of bool the carrier of T
m is Element of bool the carrier of T
Cl b is closed Element of bool the carrier of T
UXk9 . m is Relation-like Function-like set
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= m ) } is set
union { b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . UX & Cl b1 c= m ) } is set
k . m is Element of bool the carrier of T
Cl (k . m) is closed Element of bool the carrier of T
nm . b is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . b ) } is set
r is Element of the carrier of [:T,T:]
B . r is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
m is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng m is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
bool (Funcs ( the carrier of [:T,T:],REAL)) is non empty set
V is Element of the carrier of T
Ba is Element of the carrier of T
[V,Ba] is Element of [: the carrier of T, the carrier of T:]
{V,Ba} is finite set
{V} is non empty trivial finite 1 -element set
{{V,Ba},{V}} is finite V49() set
nm . V is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . V ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . V) ) } is set
nm . Ba is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . Ba ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . Ba) ) } is set
H3(V) \/ H3(Ba) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(V) \/ H3(Ba) } is set
m "**" m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
W is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
m ` is Element of bool the carrier of T
the carrier of T \ m is set
W . a is V35() real ext-real Element of REAL
cb is Element of bool the carrier of T
Bb is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
cb ` is Element of bool the carrier of T
the carrier of T \ cb is set
k . cb is Element of bool the carrier of T
Cl (k . cb) is closed Element of bool the carrier of T
Unn . W is Relation-like Function-like set
len m is 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
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
m . 1 is Relation-like Function-like set
cb is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
cb . 1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
cb . (len m) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
s is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
s . r is V35() real ext-real Element of REAL
B1 . r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(B1 . r) . r is set
ca is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
k is 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
m . k is Relation-like Function-like set
dom m is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
x is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . x is Relation-like Function-like set
y is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
y . r is V35() real ext-real Element of REAL
y . (b,a) is V35() real ext-real set
[b,a] is set
y . [b,a] is V35() real ext-real set
x . b is V35() real ext-real Element of REAL
x . a is V35() real ext-real Element of REAL
(x . b) - (x . a) is V35() real ext-real Element of REAL
abs ((x . b) - (x . a)) is V35() real ext-real Element of REAL
k is 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
cb . k is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k + 1 is 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
cb . (k + 1) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
x is 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
m . x is Relation-like Function-like set
dom m is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
m . (k + 1) is Relation-like Function-like set
Fdistfd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . ((cb . k),(m . (k + 1))) is set
[(cb . k),(m . (k + 1))] is set
{(cb . k),(m . (k + 1))} is functional finite set
{(cb . k)} is functional non empty trivial finite 1 -element set
{{(cb . k),(m . (k + 1))},{(cb . k)}} is finite V49() set
m . [(cb . k),(m . (k + 1))] is Relation-like Function-like set
fd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
y is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
fd + y is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
y . r is V35() real ext-real Element of REAL
fd . r is V35() real ext-real Element of REAL
(fd . r) + 0 is V35() real ext-real Element of REAL
(fd . r) + (y . r) is V35() real ext-real Element of REAL
Fk1 . r is V35() real ext-real Element of REAL
Fdistfd . r is V35() real ext-real Element of REAL
Fdistfd . r is V35() real ext-real Element of REAL
Fk1 . r is V35() real ext-real Element of REAL
k + 0 is 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
m . k is Relation-like Function-like set
Fk is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk . r is V35() real ext-real Element of REAL
fd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
fd . r is V35() real ext-real Element of REAL
Fdistfd . r is V35() real ext-real Element of REAL
0 + (Fdistfd . r) is V35() real ext-real Element of REAL
(fd . r) + (Fdistfd . r) is V35() real ext-real Element of REAL
m . ((cb . k),(m . (k + 1))) is set
[(cb . k),(m . (k + 1))] is set
{(cb . k),(m . (k + 1))} is functional finite set
{(cb . k)} is functional non empty trivial finite 1 -element set
{{(cb . k),(m . (k + 1))},{(cb . k)}} is finite V49() set
m . [(cb . k),(m . (k + 1))] is Relation-like Function-like set
fd + Fdistfd is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 . r is V35() real ext-real Element of REAL
y is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
fd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
y . r is V35() real ext-real Element of REAL
fd . r is V35() real ext-real Element of REAL
cb . 0 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is 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
x is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . k is Relation-like Function-like set
y is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
x . r is V35() real ext-real Element of REAL
y . r is V35() real ext-real Element of REAL
dom m is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
k is set
m . k is Relation-like Function-like set
Seg (len m) is finite len m -element V76() V77() V78() V79() V80() V81() Element of bool NAT
W . b is V35() real ext-real Element of REAL
y is Element of bool the carrier of T
x is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
y ` is Element of bool the carrier of T
the carrier of T \ y is set
k . y is Element of bool the carrier of T
Cl (k . y) is closed Element of bool the carrier of T
Bb is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Bb . (b,a) is V35() real ext-real set
[b,a] is set
Bb . [b,a] is V35() real ext-real set
1 - 0 is V35() real ext-real Element of REAL
abs (1 - 0) is V35() real ext-real Element of REAL
abs 1 is V35() real ext-real V65() Element of REAL
x is 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
b is Element of the carrier of T
a is Element of the carrier of T
[b,a] is Element of [: the carrier of T, the carrier of T:]
{b,a} is finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is finite V49() set
q . [b,a] is V35() real ext-real Element of REAL
b is Element of bool the carrier of T
m is Element of bool the carrier of T
Cl b is closed Element of bool the carrier of T
min (1,(q . [b,a])) is V35() real ext-real set
min (1,q) is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
(min (1,q)) . [b,a] is V35() real ext-real Element of REAL
b is Element of the carrier of [:T,T:]
a is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
a . b is V35() real ext-real Element of REAL
m . (a,a) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[a,a] is set
{a,a} is functional finite set
{a} is functional non empty trivial finite 1 -element set
{{a,a},{a}} is finite V49() set
m . [a,a] is Relation-like Function-like set
a + a is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
(a + a) . b is V35() real ext-real Element of REAL
(a . b) + (a . b) is V35() real ext-real Element of REAL
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & ( for b2 being Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] holds
( not UXk9 . b1 = b2 or not b2 . a1 <= 0 or not b2 . a2 <= 0 ) ) ) } is set
b is Element of the carrier of [:T,T:]
a is Element of the carrier of [:T,T:]
n . a is Element of bool the carrier of [:T,T:]
B1 . b is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(B1 . b) . b is set
B1 . a is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(B1 . a) . b is set
B . b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
B . a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
b is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng b is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
bool (Funcs ( the carrier of [:T,T:],REAL)) is non empty set
r is Element of the carrier of T
m is Element of the carrier of T
[r,m] is Element of [: the carrier of T, the carrier of T:]
{r,m} is finite set
{r} is non empty trivial finite 1 -element set
{{r,m},{r}} is finite V49() set
nm . r is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . r ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . r) ) } is set
nm . m is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . m ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . m) ) } is set
H3(r) \/ H3(m) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(r) \/ H3(m) } is set
V is Element of the carrier of T
Ba is Element of the carrier of T
[V,Ba] is Element of [: the carrier of T, the carrier of T:]
{V,Ba} is finite set
{V} is non empty trivial finite 1 -element set
{{V,Ba},{V}} is finite V49() set
ca is Element of the carrier of T
W is Element of the carrier of T
[ca,W] is Element of [: the carrier of T, the carrier of T:]
{ca,W} is finite set
{ca} is non empty trivial finite 1 -element set
{{ca,W},{ca}} is finite V49() set
n . [ca,W] is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & ( for b2 being Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] holds
( not UXk9 . b1 = b2 or not b2 . V <= 0 or not b2 . Ba <= 0 ) ) ) } is set
nm . ca is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . ca ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . ca) ) } is set
nm . W is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . W ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . W) ) } is set
H3(ca) \/ H3(W) is set
[:(nm . ca),(nm . W):] is Element of bool the carrier of [:T,T:]
Bb is Element of the carrier of [:T,T:]
n . Bb is Element of bool the carrier of [:T,T:]
cb is set
k is Element of bool the carrier of T
UXk9 . k is Relation-like Function-like set
x is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
x . V is V35() real ext-real Element of REAL
x . Ba is V35() real ext-real Element of REAL
the carrier of T \ k is Element of bool the carrier of T
fd is Element of bool the carrier of T
y is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
fd ` is Element of bool the carrier of T
the carrier of T \ fd is set
k . fd is Element of bool the carrier of T
Cl (k . fd) is closed Element of bool the carrier of T
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & ( for b2 being Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] holds
( not UXk9 . b1 = b2 or not b2 . r <= 0 or not b2 . m <= 0 ) ) ) } is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H5(r,m) } is set
[:(nm . r),(nm . m):] is Element of bool the carrier of [:T,T:]
n . [r,m] is set
V is set
Ba is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . Ba is Relation-like Function-like set
V is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng V is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" V is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
W is Element of the carrier of T
nm . W is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . W ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . W) ) } is set
Bb is Element of the carrier of T
nm . Bb is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . Bb ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . Bb) ) } is set
H3(W) \/ H3(Bb) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(W) \/ H3(Bb) } is set
Ba is Element of the carrier of T
ca is Element of the carrier of T
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & ( for b2 being Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] holds
( not UXk9 . b1 = b2 or not b2 . Ba <= 0 or not b2 . ca <= 0 ) ) ) } is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H5(Ba,ca) } is set
H4(H3(W) \/ H3(Bb)) \ H4(H5(Ba,ca)) is Element of bool H4(H3(W) \/ H3(Bb))
bool H4(H3(W) \/ H3(Bb)) is non empty set
[Ba,ca] is Element of [: the carrier of T, the carrier of T:]
{Ba,ca} is finite set
{Ba} is non empty trivial finite 1 -element set
{{Ba,ca},{Ba}} is finite V49() set
(m "**" V) . [Ba,ca] is set
len V is 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
the_unity_wrt m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
cb is Element of the carrier of [:T,T:]
(m "**" V) . cb is set
len V is 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
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
V . 1 is Relation-like Function-like set
k is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
k . 1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k . (len V) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
cb is Element of the carrier of [:T,T:]
x is 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
k . x is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(k . x) . cb is set
x + 1 is 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
k . (x + 1) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(k . (x + 1)) . cb is set
dom V is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
V . (x + 1) is Relation-like Function-like set
y is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . y is Relation-like Function-like set
fd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
fd . (Ba,ca) is V35() real ext-real set
[Ba,ca] is set
fd . [Ba,ca] is V35() real ext-real set
y . Ba is V35() real ext-real Element of REAL
y . ca is V35() real ext-real Element of REAL
(y . Ba) - (y . ca) is V35() real ext-real Element of REAL
abs ((y . Ba) - (y . ca)) is V35() real ext-real Element of REAL
SFk1 is Element of bool the carrier of T
UXk9 . SFk1 is Relation-like Function-like set
F9 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
F9 . Ba is V35() real ext-real Element of REAL
F9 . ca is V35() real ext-real Element of REAL
ANoiS2 is Element of bool the carrier of T
AS2No is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
ANoiS2 ` is Element of bool the carrier of T
the carrier of T \ ANoiS2 is set
k . ANoiS2 is Element of bool the carrier of T
Cl (k . ANoiS2) is closed Element of bool the carrier of T
SFk1 is Element of bool the carrier of T
UXk9 . SFk1 is Relation-like Function-like set
F9 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
F9 . Ba is V35() real ext-real Element of REAL
F9 . ca is V35() real ext-real Element of REAL
ANoiS2 is Element of bool the carrier of T
AS2No is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
ANoiS2 ` is Element of bool the carrier of T
the carrier of T \ ANoiS2 is set
k . ANoiS2 is Element of bool the carrier of T
Cl (k . ANoiS2) is closed Element of bool the carrier of T
Fdistfd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . (Fk1,Fk) is set
[Fk1,Fk] is set
{Fk1,Fk} is functional finite set
{Fk1} is functional non empty trivial finite 1 -element set
{{Fk1,Fk},{Fk1}} is finite V49() set
m . [Fk1,Fk] is Relation-like Function-like set
Fk1 + Fk is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fdistfd . cb is V35() real ext-real Element of REAL
Fk . cb is V35() real ext-real Element of REAL
0 + (Fk . cb) is V35() real ext-real Element of REAL
k . 0 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(k . 0) . cb is set
(m "**" V) . cb is set
len V is 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
cb is Element of the carrier of [:T,T:]
(m "**" V) . cb is set
cb is Element of the carrier of [:T,T:]
(m "**" V) . cb is set
V is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng V is finite set
m is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng m is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
ca is Element of the carrier of T
W is Element of the carrier of T
[ca,W] is Element of [: the carrier of T, the carrier of T:]
{ca,W} is finite set
{ca} is non empty trivial finite 1 -element set
{{ca,W},{ca}} is finite V49() set
nm . ca is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . ca ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . ca) ) } is set
nm . W is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . W ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . W) ) } is set
H3(ca) \/ H3(W) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(ca) \/ H3(W) } is set
H4(H5(r,m)) /\ H4(H3(ca) \/ H3(W)) is set
cb is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
Bb is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng Bb is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
Ba is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng Ba is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
(rng Bb) \ (rng Ba) is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" Bb is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m "**" Ba is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
x is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng x is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" x is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m . ((m "**" Ba),(m "**" x)) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[(m "**" Ba),(m "**" x)] is set
{(m "**" Ba),(m "**" x)} is functional finite set
{(m "**" Ba)} is functional non empty trivial finite 1 -element set
{{(m "**" Ba),(m "**" x)},{(m "**" Ba)}} is finite V49() set
m . [(m "**" Ba),(m "**" x)] is Relation-like Function-like set
y is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng y is finite set
fd is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng fd is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
(rng Ba) \ (rng fd) is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" fd is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
Fdistfd is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng Fdistfd is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" Fdistfd is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m . ((m "**" fd),(m "**" Fdistfd)) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[(m "**" fd),(m "**" Fdistfd)] is set
{(m "**" fd),(m "**" Fdistfd)} is functional finite set
{(m "**" fd)} is functional non empty trivial finite 1 -element set
{{(m "**" fd),(m "**" Fdistfd)},{(m "**" fd)}} is finite V49() set
m . [(m "**" fd),(m "**" Fdistfd)] is Relation-like Function-like set
rng cb is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
(rng cb) \ (rng fd) is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" cb is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
Fk1 is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng Fk1 is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
m "**" Fk1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m . ((m "**" fd),(m "**" Fk1)) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
[(m "**" fd),(m "**" Fk1)] is set
{(m "**" fd),(m "**" Fk1)} is functional finite set
{{(m "**" fd),(m "**" Fk1)},{(m "**" fd)}} is finite V49() set
m . [(m "**" fd),(m "**" Fk1)] is Relation-like Function-like set
H4(H3(ca) \/ H3(W)) \ H4(H5(r,m)) is Element of bool H4(H3(ca) \/ H3(W))
bool H4(H3(ca) \/ H3(W)) is non empty set
AS2No is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
AS2No . b is V35() real ext-real Element of REAL
SFk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
ANoiS2 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
ANoiS2 + Fk is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SFk1 . b is V35() real ext-real Element of REAL
ANoiS2 . b is V35() real ext-real Element of REAL
Fk . b is V35() real ext-real Element of REAL
(ANoiS2 . b) + (Fk . b) is V35() real ext-real Element of REAL
AS1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
F9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SFk1 + F9 is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
AS1 . b is V35() real ext-real Element of REAL
F9 . b is V35() real ext-real Element of REAL
(SFk1 . b) + (F9 . b) is V35() real ext-real Element of REAL
AS2 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
ANoiS2 + AS2No is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
AS2 . b is V35() real ext-real Element of REAL
(ANoiS2 . b) + (AS2No . b) is V35() real ext-real Element of REAL
SumFdist1 is set
SumFdist2 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . SumFdist2 is Relation-like Function-like set
len Fdistfd is 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
the_unity_wrt m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
SumFdist1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
Fk . (r,m) is V35() real ext-real set
[r,m] is set
Fk . [r,m] is V35() real ext-real set
len Fdistfd is 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
the_unity_wrt m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
SumFdist2 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
len Fdistfd is 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
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
Fdistfd . 1 is Relation-like Function-like set
SumFdist2 is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
SumFdist2 . 1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
SumFdist2 . (len Fdistfd) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is 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
SumFdist2 . k is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k + 1 is 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
SumFdist2 . (k + 1) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
dom Fdistfd is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
Fdistfd . (k + 1) is Relation-like Function-like set
fd is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . fd is Relation-like Function-like set
fd . r is V35() real ext-real Element of REAL
fd . m is V35() real ext-real Element of REAL
(fd . r) - (fd . m) is V35() real ext-real Element of REAL
abs ((fd . r) - (fd . m)) is V35() real ext-real Element of REAL
Fdistfd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fdistfd . (r,m) is V35() real ext-real set
Fdistfd . [r,m] is V35() real ext-real set
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 . (r,m) is V35() real ext-real set
Fk1 . [r,m] is V35() real ext-real set
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Nk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . (Fk,Nk1) is set
[Fk,Nk1] is set
{Fk,Nk1} is functional finite set
{Fk} is functional non empty trivial finite 1 -element set
{{Fk,Nk1},{Fk}} is finite V49() set
m . [Fk,Nk1] is Relation-like Function-like set
Fk + Nk1 is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk . (r,m) is V35() real ext-real set
Fk . [r,m] is V35() real ext-real set
0 + 0 is 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
Nk1 . (r,m) is V35() real ext-real set
Nk1 . [r,m] is V35() real ext-real set
(Fk . (r,m)) + (Nk1 . (r,m)) is V35() real ext-real set
Fk1 . (r,m) is V35() real ext-real set
Fk1 . [r,m] is V35() real ext-real set
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 . (r,m) is V35() real ext-real set
Fk1 . [r,m] is V35() real ext-real set
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 . (r,m) is V35() real ext-real set
Fk1 . [r,m] is V35() real ext-real set
Fn is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fn . (r,m) is V35() real ext-real set
Fn . [r,m] is V35() real ext-real set
SumFdist2 . 0 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
k . (r,m) is V35() real ext-real set
k . [r,m] is V35() real ext-real set
len Fdistfd is 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
AS2 . (r,m) is V35() real ext-real set
AS2 . [r,m] is V35() real ext-real set
AS1 . (r,m) is V35() real ext-real set
AS1 . [r,m] is V35() real ext-real set
SumFdist1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SumFdist2 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SumFdist2 . b is V35() real ext-real Element of REAL
SumFdist1 . b is V35() real ext-real Element of REAL
SumFdist1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SumFdist2 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SumFdist2 . b is V35() real ext-real Element of REAL
SumFdist1 . b is V35() real ext-real Element of REAL
s is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
b is Element of the carrier of T
s . (b,b) is V35() real ext-real Element of REAL
[b,b] is set
{b,b} is finite set
{b} is non empty trivial finite 1 -element set
{{b,b},{b}} is finite V49() set
s . [b,b] is V35() real ext-real set
[b,b] is Element of [: the carrier of T, the carrier of T:]
m is Element of the carrier of [:T,T:]
B . m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
r is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
len r is 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
m "**" r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
the_unity_wrt m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
(m "**" r) . m is set
r is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
len r is 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
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
r . 1 is Relation-like Function-like set
m "**" r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
m . 1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m . (len r) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
V is 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
m . V is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(m . V) . m is set
V + 1 is 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
m . (V + 1) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(m . (V + 1)) . m is set
rng r is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
bool (Funcs ( the carrier of [:T,T:],REAL)) is non empty set
Ba is Element of the carrier of T
ca is Element of the carrier of T
[Ba,ca] is Element of [: the carrier of T, the carrier of T:]
{Ba,ca} is finite set
{Ba} is non empty trivial finite 1 -element set
{{Ba,ca},{Ba}} is finite V49() set
nm . Ba is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . Ba ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . Ba) ) } is set
nm . ca is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . ca ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . ca) ) } is set
H3(Ba) \/ H3(ca) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(Ba) \/ H3(ca) } is set
dom r is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
r . (V + 1) is Relation-like Function-like set
W is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . W is Relation-like Function-like set
Bb is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Bb . (b,b) is V35() real ext-real set
Bb . [b,b] is V35() real ext-real set
W . b is V35() real ext-real Element of REAL
(W . b) - (W . b) is V35() real ext-real Element of REAL
abs ((W . b) - (W . b)) is V35() real ext-real Element of REAL
cb is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
x is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . (k,x) is set
[k,x] is set
{k,x} is functional finite set
{k} is functional non empty trivial finite 1 -element set
{{k,x},{k}} is finite V49() set
m . [k,x] is Relation-like Function-like set
k + x is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
cb . m is V35() real ext-real Element of REAL
x . m is V35() real ext-real Element of REAL
0 + (x . m) is V35() real ext-real Element of REAL
m . 0 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(m . 0) . m is set
(m "**" r) . m is set
r is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
len r is 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
m "**" r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(m "**" r) . m is set
r is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
m "**" r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(m "**" r) . m is set
B1 . m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
b is Element of the carrier of T
s . (b,b) is V35() real ext-real Element of REAL
[b,b] is set
{b,b} is finite set
{{b,b},{b}} is finite V49() set
s . [b,b] is V35() real ext-real set
a is Element of the carrier of T
s . (b,a) is V35() real ext-real Element of REAL
[b,a] is set
{b,a} is finite set
{{b,a},{b}} is finite V49() set
s . [b,a] is V35() real ext-real set
s . (b,a) is V35() real ext-real Element of REAL
[b,a] is set
{b,a} is finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is finite V49() set
s . [b,a] is V35() real ext-real set
(s . (b,a)) + (s . (b,a)) is V35() real ext-real Element of REAL
[b,b] is Element of [: the carrier of T, the carrier of T:]
[b,a] is Element of [: the carrier of T, the carrier of T:]
[b,a] is Element of [: the carrier of T, the carrier of T:]
m is Element of the carrier of [:T,T:]
B . m is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
V is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
m "**" V is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
B1 . m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
r is Element of the carrier of [:T,T:]
B1 . r is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m is Element of the carrier of [:T,T:]
B1 . m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
s . m is V35() real ext-real Element of REAL
ca is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
ca . m is V35() real ext-real Element of REAL
s . r is V35() real ext-real Element of REAL
W is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
W . r is V35() real ext-real Element of REAL
ca . r is V35() real ext-real Element of REAL
ca . m is V35() real ext-real Element of REAL
Bb is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Bb . m is V35() real ext-real Element of REAL
(ca . r) + (ca . m) is V35() real ext-real Element of REAL
(W . r) + (Bb . m) is V35() real ext-real Element of REAL
len V is 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
the_unity_wrt m is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
cb is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of [:T,T:],REAL)
Ba is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Ba . m is V35() real ext-real Element of REAL
Ba . r is V35() real ext-real Element of REAL
Ba . m is V35() real ext-real Element of REAL
(Ba . r) + (Ba . m) is V35() real ext-real Element of REAL
len V is 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
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
V . 1 is Relation-like Function-like set
cb is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
cb . 1 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
cb . (len V) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is 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
cb . k is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k + 1 is 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
cb . (k + 1) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
rng V is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
bool (Funcs ( the carrier of [:T,T:],REAL)) is non empty set
x is Element of the carrier of T
y is Element of the carrier of T
[x,y] is Element of [: the carrier of T, the carrier of T:]
{x,y} is finite set
{x} is non empty trivial finite 1 -element set
{{x,y},{x}} is finite V49() set
nm . x is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . x ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . x) ) } is set
nm . y is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . y ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . y) ) } is set
H3(x) \/ H3(y) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(x) \/ H3(y) } is set
dom V is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
V . (k + 1) is Relation-like Function-like set
fd is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . fd is Relation-like Function-like set
fd . b is V35() real ext-real Element of REAL
fd . b is V35() real ext-real Element of REAL
(fd . b) - (fd . b) is V35() real ext-real Element of REAL
fd . a is V35() real ext-real Element of REAL
(fd . b) - (fd . a) is V35() real ext-real Element of REAL
(fd . a) - (fd . b) is V35() real ext-real Element of REAL
((fd . b) - (fd . a)) + ((fd . a) - (fd . b)) is V35() real ext-real Element of REAL
abs ((fd . b) - (fd . b)) is V35() real ext-real Element of REAL
abs ((fd . b) - (fd . a)) is V35() real ext-real Element of REAL
abs ((fd . a) - (fd . b)) is V35() real ext-real Element of REAL
(abs ((fd . b) - (fd . a))) + (abs ((fd . a) - (fd . b))) is V35() real ext-real Element of REAL
Fdistfd is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fdistfd . (b,b) is V35() real ext-real set
Fdistfd . [b,b] is V35() real ext-real set
Fdistfd . (b,a) is V35() real ext-real set
Fdistfd . [b,a] is V35() real ext-real set
- ((fd . a) - (fd . b)) is V35() real ext-real Element of REAL
abs (- ((fd . a) - (fd . b))) is V35() real ext-real Element of REAL
Fdistfd . (b,a) is V35() real ext-real set
Fdistfd . [b,a] is V35() real ext-real set
(fd . b) - (fd . a) is V35() real ext-real Element of REAL
abs ((fd . b) - (fd . a)) is V35() real ext-real Element of REAL
F9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
F9 . m is V35() real ext-real Element of REAL
F9 . r is V35() real ext-real Element of REAL
F9 . m is V35() real ext-real Element of REAL
(F9 . r) + (F9 . m) is V35() real ext-real Element of REAL
Fk is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk . m is V35() real ext-real Element of REAL
Fk . r is V35() real ext-real Element of REAL
Fk . m is V35() real ext-real Element of REAL
(Fk . r) + (Fk . m) is V35() real ext-real Element of REAL
SFk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
SFk1 . m is V35() real ext-real Element of REAL
(Fk . m) + (SFk1 . m) is V35() real ext-real Element of REAL
SFk1 . r is V35() real ext-real Element of REAL
SFk1 . m is V35() real ext-real Element of REAL
(SFk1 . r) + (SFk1 . m) is V35() real ext-real Element of REAL
((Fk . r) + (Fk . m)) + ((SFk1 . r) + (SFk1 . m)) is V35() real ext-real Element of REAL
Fk1 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m . (Fk,SFk1) is set
[Fk,SFk1] is set
{Fk,SFk1} is functional finite set
{Fk} is functional non empty trivial finite 1 -element set
{{Fk,SFk1},{Fk}} is finite V49() set
m . [Fk,SFk1] is Relation-like Function-like set
Fk + SFk1 is Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -defined REAL -valued Function-like non empty total total quasi_total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Fk1 . r is V35() real ext-real Element of REAL
(Fk . r) + (SFk1 . r) is V35() real ext-real Element of REAL
Fk1 . m is V35() real ext-real Element of REAL
(Fk . m) + (SFk1 . m) is V35() real ext-real Element of REAL
cb . 0 is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
k . m is V35() real ext-real Element of REAL
k . r is V35() real ext-real Element of REAL
k . m is V35() real ext-real Element of REAL
(k . r) + (k . m) is V35() real ext-real Element of REAL
Ba is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Ba . m is V35() real ext-real Element of REAL
Ba . r is V35() real ext-real Element of REAL
Ba . m is V35() real ext-real Element of REAL
(Ba . r) + (Ba . m) is V35() real ext-real Element of REAL
len V is 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
Ba is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Ba . m is V35() real ext-real Element of REAL
Ba . r is V35() real ext-real Element of REAL
Ba . m is V35() real ext-real Element of REAL
(Ba . r) + (Ba . m) is V35() real ext-real Element of REAL
Ba is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
Ba . m is V35() real ext-real Element of REAL
Ba . r is V35() real ext-real Element of REAL
Ba . m is V35() real ext-real Element of REAL
(Ba . r) + (Ba . m) is V35() real ext-real Element of REAL
b is Element of the carrier of T
nm . b is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . b ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . b) ) } is set
a is Relation-like the carrier of T -defined REAL -valued Function-like total quasi_total complex-valued ext-real-valued real-valued Element of Funcs ( the carrier of T,REAL)
Unn . a is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
m is Element of bool the carrier of T
UXk9 . m is Relation-like Function-like set
r is Element of the carrier of T
m is Element of the carrier of T
(Unn . a) . (r,m) is set
[r,m] is set
{r,m} is finite set
{r} is non empty trivial finite 1 -element set
{{r,m},{r}} is finite V49() set
(Unn . a) . [r,m] is set
a . r is V35() real ext-real Element of REAL
a . m is V35() real ext-real Element of REAL
(a . r) - (a . m) is V35() real ext-real Element of REAL
abs ((a . r) - (a . m)) is V35() real ext-real Element of REAL
b is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
m is Element of bool the carrier of T
r is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
m ` is Element of bool the carrier of T
the carrier of T \ m is set
k . m is Element of bool the carrier of T
Cl (k . m) is closed Element of bool the carrier of T
r is Element of the carrier of T
m is Element of the carrier of T
(Unn . a) . (r,m) is set
[r,m] is set
{r,m} is finite set
{r} is non empty trivial finite 1 -element set
{{r,m},{r}} is finite V49() set
(Unn . a) . [r,m] is set
a . r is V35() real ext-real Element of REAL
a . m is V35() real ext-real Element of REAL
(a . r) - (a . m) is V35() real ext-real Element of REAL
abs ((a . r) - (a . m)) is V35() real ext-real Element of REAL
b is Element of the carrier of [:T,T:]
B1 . b is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
B . b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like Element of (Funcs ( the carrier of [:T,T:],REAL)) *
a is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Funcs ( the carrier of [:T,T:],REAL)
rng a is functional finite Element of bool (Funcs ( the carrier of [:T,T:],REAL))
bool (Funcs ( the carrier of [:T,T:],REAL)) is non empty set
b is Element of the carrier of T
m is Element of the carrier of T
[b,m] is Element of [: the carrier of T, the carrier of T:]
{b,m} is finite set
{b} is non empty trivial finite 1 -element set
{{b,m},{b}} is finite V49() set
nm . b is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . b ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . b) ) } is set
nm . m is Element of bool the carrier of T
{ b1 where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & not b1 misses nm . m ) } is set
{ (UXk9 . b1) where b1 is Element of bool the carrier of T : ( b1 in TPM . Un & b1 in H2(nm . m) ) } is set
H3(b) \/ H3(m) is set
{ (Unn . b1) where b1 is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:] : b1 in H3(b) \/ H3(m) } is set
len a is 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
r is 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
a . r is Relation-like Function-like set
dom a is finite V76() V77() V78() V79() V80() V81() Element of bool NAT
m is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
Unn . m is Relation-like Function-like set
m "**" a is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
b is Element of the carrier of [:T,T:]
k . b is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:], the carrier of R^1)
B1 . b is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
a is Relation-like the carrier of [:T,T:] -defined the carrier of R^1 -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:], the carrier of R^1:]
b is Element of the carrier of T
a is Element of the carrier of T
[b,a] is Element of [: the carrier of T, the carrier of T:]
{b,a} is finite set
{b} is non empty trivial finite 1 -element set
{{b,a},{b}} is finite V49() set
(min (1,q)) . [b,a] is V35() real ext-real Element of REAL
q . [b,a] is V35() real ext-real Element of REAL
min (1,(q . [b,a])) is V35() real ext-real set
b is Element of the carrier of [:T,T:]
a is Element of the carrier of [:T,T:]
n . a is Element of bool the carrier of [:T,T:]
k . b is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:], the carrier of R^1)
(k . b) . b is set
k . a is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:], the carrier of R^1)
(k . a) . b is set
min (1,s) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
Un is set
(() /") . Un is set
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
UX is set
() . UX is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
UXk is set
k is set
[UXk,k] is set
{UXk,k} is finite set
{UXk} is non empty trivial finite 1 -element set
{{UXk,k},{UXk}} is finite V49() set
TPM . k is set
TPM . UXk is set
UXk9 is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
nm is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
n is 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
m is 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
[n,m] is Element of [:NAT,NAT:]
{n,m} is finite V49() V76() V77() V78() V79() V80() V81() set
{n} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{n,m},{n}} is finite V49() set
TPM . m is set
TPM . n is set
Unn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
[:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):] is non empty non trivial non finite set
Un is Relation-like NAT -defined Funcs ( the carrier of [:T,T:],REAL) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs ( the carrier of [:T,T:],REAL)):]
UX is 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
Un . UX is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
dom Un is V76() V77() V78() V79() V80() V81() Element of bool NAT
PFuncs ([: the carrier of T, the carrier of T:],REAL) is set
[:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is set
bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):] is non empty set
UX is Relation-like NAT -defined PFuncs ([: the carrier of T, the carrier of T:],REAL) -valued Function-like quasi_total Element of bool [:NAT,(PFuncs ([: the carrier of T, the carrier of T:],REAL)):]
UXk is Element of the carrier of T
k is non empty Element of bool the carrier of T
k ` is Element of bool the carrier of T
the carrier of T \ k is set
nm is Element of bool the carrier of T
Cl nm is closed Element of bool the carrier of T
the topology of T is non empty Element of bool (bool the carrier of T)
n is open Element of bool the carrier of T
m is 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
TPM . m is Element of bool (bool the carrier of T)
Unn is Element of bool the carrier of T
Cl Unn is closed Element of bool the carrier of T
B is open Element of bool the carrier of T
B1 is 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
TPM . B1 is Element of bool (bool the carrier of T)
[m,B1] is Element of [:NAT,NAT:]
{m,B1} is finite V49() V76() V77() V78() V79() V80() V81() set
{m} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{m,B1},{m}} is finite V49() set
() . [m,B1] is 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
Un . (() . [m,B1]) is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(() /") . (() . [m,B1]) is Element of [:NAT,NAT:]
q is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
s is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
( the carrier of T,s,UXk) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
[: the carrier of T,REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [: the carrier of T,REAL:] is non empty non trivial non finite set
( the carrier of T,s,UXk) .: k is V76() V77() V78() Element of bool REAL
b is V35() real ext-real set
dom ( the carrier of T,s,UXk) is Element of bool the carrier of T
a is set
( the carrier of T,s,UXk) . a is V35() real ext-real Element of REAL
b is Element of the carrier of T
s . (UXk,b) is V35() real ext-real Element of REAL
[UXk,b] is set
{UXk,b} is finite set
{UXk} is non empty trivial finite 1 -element set
{{UXk,b},{UXk}} is finite V49() set
s . [UXk,b] is V35() real ext-real set
( the carrier of T,s,UXk) . b is V35() real ext-real Element of REAL
Cl n is closed Element of bool the carrier of T
UX . (() . [m,B1]) is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
dom ( the carrier of T,s,UXk) is Element of bool the carrier of T
lower_bound (( the carrier of T,s,UXk) .: k) is V35() real ext-real Element of REAL
b is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
( the carrier of T,b,k) is Relation-like the carrier of T -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of T,REAL:]
( the carrier of T,b,k) . UXk is V35() real ext-real Element of REAL
UXk is 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
UX . UXk is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
Un . UXk is Relation-like Function-like Element of Funcs ( the carrier of [:T,T:],REAL)
(() /") . UXk is Element of [:NAT,NAT:]
k is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
UXk9 is set
() . UXk9 is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
nm is set
n is set
[nm,n] is set
{nm,n} is finite set
{nm} is non empty trivial finite 1 -element set
{{nm,n},{nm}} is finite V49() set
TPM . n is set
TPM . nm is set
m is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
Unn is Element of [: the carrier of T, the carrier of T:]
m . Unn is V35() real ext-real Element of REAL
B is set
B1 is set
[B,B1] is set
{B,B1} is finite set
{B} is non empty trivial finite 1 -element set
{{B,B1},{B}} is finite V49() set
Unn is Relation-like the carrier of [:T,T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [: the carrier of [:T,T:],REAL:]
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
the topology of T is non empty Element of bool (bool the carrier of T)
bbcT is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,bbcT) is strict Reflexive discerning symmetric triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of T,bbcT)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,bbcT)))
the carrier of (SpaceMetr ( the carrier of T,bbcT)) is set
bool the carrier of (SpaceMetr ( the carrier of T,bbcT)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,bbcT))) is non empty set
PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of PM is non empty set
TPM is Element of bool (bool the carrier of T)
bool the carrier of PM is non empty set
Un is Relation-like set
Un |_2 TPM is Relation-like set
UX is Relation-like set
3 / 2 is V35() real ext-real non negative Element of REAL
{ (union { (Ball (b2,(1 / 2))) where b2 is Element of the carrier of PM : ( b2 in b1 \ (PartUnion (b1,UX)) & Ball (b2,(3 / 2)) c= b1 ) } ) where b1 is Element of bool the carrier of PM : b1 in TPM } is set
bool the carrier of PM is non empty Element of bool (bool the carrier of PM)
bool (bool the carrier of PM) is non empty set
k is set
UXk9 is Element of bool the carrier of PM
PartUnion (UXk9,UX) is set
UXk9 \ (PartUnion (UXk9,UX)) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in UXk9 \ (PartUnion (UXk9,UX)) & Ball (b1,(3 / 2)) c= UXk9 ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in UXk9 \ (PartUnion (UXk9,UX)) & Ball (b1,(3 / 2)) c= UXk9 ) } is set
nm is set
n is set
m is Element of the carrier of PM
Ball (m,(1 / 2)) is Element of bool the carrier of PM
Ball (m,(3 / 2)) is Element of bool the carrier of PM
bool (bool the carrier of PM) is non empty Element of bool (bool (bool the carrier of PM))
bool (bool the carrier of PM) is non empty set
bool (bool (bool the carrier of PM)) is non empty set
[:NAT,(bool (bool the carrier of PM)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of PM)):] is non empty non trivial non finite set
k is Element of bool (bool the carrier of PM)
UXk9 is Relation-like NAT -defined bool (bool the carrier of PM) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of PM)):]
UXk9 . 0 is Element of bool (bool the carrier of PM)
nm is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union nm is Element of bool (bool the carrier of T)
n is Element of bool the carrier of T
m is 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
UXk9 . m is Element of bool (bool the carrier of PM)
Unn is Element of bool the carrier of PM
PartUnion (Unn,UX) is set
Unn \ (PartUnion (Unn,UX)) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in Unn \ (PartUnion (Unn,UX)) & Ball (b1,(3 / 2)) c= Unn ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in Unn \ (PartUnion (Unn,UX)) & Ball (b1,(3 / 2)) c= Unn ) } is set
B1 is set
k is Element of the carrier of PM
Ball (k,(1 / 2)) is Element of bool the carrier of PM
Ball (k,(3 / 2)) is Element of bool the carrier of PM
B1 is Element of bool (bool the carrier of PM)
Family_open_set PM is Element of bool (bool the carrier of PM)
k is set
q is Element of the carrier of PM
Ball (q,(1 / 2)) is Element of bool the carrier of PM
Ball (q,(3 / 2)) is Element of bool the carrier of PM
Unn is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
Unn + 1 is 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
B is 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
B + 1 is 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
2 |^ (B + 1) is 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
1 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
3 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
{ (union (UXk9 . b1)) where b1 is 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 : b1 <= B } is set
union { (union (UXk9 . b1)) where b1 is 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 : b1 <= B } is set
{ (union { H1(b2,B) where b2 is Element of the carrier of PM : ( S2[b2,b1,B] & not b2 in union { (union (UXk9 . b1)) where b3 is 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 : b1 <= B } ) } ) where b1 is Element of bool the carrier of PM : S1[b1] } is set
B1 is Element of bool the carrier of PM
PartUnion (B1,UX) is set
B1 \ (PartUnion (B1,UX)) is Element of bool the carrier of PM
{ H1(b1,B) where b1 is Element of the carrier of PM : ( S2[b1,B1,B] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= B } ) } is set
union { H1(b1,B) where b1 is Element of the carrier of PM : ( S2[b1,B1,B] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= B } ) } is set
q is set
s is Element of the carrier of PM
Ball (s,(1 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
Ball (s,(3 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
q is Element of bool (bool the carrier of PM)
Family_open_set PM is Element of bool (bool the carrier of PM)
s is set
b is Element of the carrier of PM
Ball (b,(1 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
Ball (b,(3 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
[#] T is non empty non proper open closed Element of bool the carrier of T
union (Union nm) is Element of bool the carrier of T
n is set
Unn is Element of bool the carrier of T
Unn is set
B is set
B1 is 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
nm . B1 is Element of bool (bool the carrier of T)
Union UXk9 is Element of bool (bool the carrier of PM)
B is 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
nm . B is Element of bool (bool the carrier of T)
union (nm . B) is Element of bool the carrier of T
B1 is set
B is Element of bool the carrier of T
Family_open_set PM is Element of bool (bool the carrier of PM)
m is Element of the carrier of PM
B1 is Element of bool the carrier of PM
k is V35() real ext-real Element of REAL
Ball (m,k) is Element of bool the carrier of PM
q is 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
2 |^ q is V35() real ext-real Element of REAL
3 / (2 |^ q) is V35() real ext-real Element of REAL
q is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
2 |^ q is V35() real ext-real Element of REAL
3 / (2 |^ q) is V35() real ext-real Element of REAL
q + 1 is 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
2 |^ (q + 1) is 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
1 / (2 |^ (q + 1)) is V35() real ext-real non negative Element of REAL
PartUnion (B1,UX) is set
B1 \ (PartUnion (B1,UX)) is Element of bool the carrier of PM
3 / (2 |^ (q + 1)) is V35() real ext-real non negative Element of REAL
{ (union (UXk9 . b1)) where b1 is 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 : b1 <= q } is set
union { (union (UXk9 . b1)) where b1 is 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 : b1 <= q } is set
{ H1(b1,q) where b1 is Element of the carrier of PM : ( S2[b1,B1,q] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= q } ) } is set
union { H1(b1,q) where b1 is Element of the carrier of PM : ( S2[b1,B1,q] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= q } ) } is set
(2 |^ q) * 2 is V35() real ext-real Element of REAL
UX -Seg B1 is set
union (UX -Seg B1) is set
b is set
[b,B1] is set
{b,B1} is finite set
{b} is non empty trivial finite 1 -element set
{{b,B1},{b}} is finite V49() set
field UX is set
[B1,b] is set
{B1,b} is finite set
{B1} is non empty trivial finite 1 -element set
{{B1,b},{B1}} is finite V49() set
Ball (m,(1 / (2 |^ (q + 1)))) is Element of bool the carrier of PM
{ (union (nm . b1)) where b1 is 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 : b1 <= q } is set
union { (union (nm . b1)) where b1 is 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 : b1 <= q } is set
a is set
b is 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
nm . b is Element of bool (bool the carrier of T)
union (nm . b) is Element of bool the carrier of T
Ball (m,(3 / (2 |^ (q + 1)))) is Element of bool the carrier of PM
{ H1(b1,q) where b1 is Element of the carrier of PM : ( S2[b1,B1,q] & not b1 in union { (union (nm . b1)) where b2 is 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 : b1 <= q } ) } is set
{ (union { H1(b2,q) where b2 is Element of the carrier of PM : ( S2[b2,b1,q] & not b2 in union { (union (UXk9 . b1)) where b3 is 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 : b1 <= q } ) } ) where b1 is Element of bool the carrier of PM : b1 in TPM } is set
nm . (q + 1) is Element of bool (bool the carrier of T)
n is set
m is 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
UXk9 . m is Element of bool (bool the carrier of PM)
Unn is Element of bool the carrier of PM
PartUnion (Unn,UX) is set
Unn \ (PartUnion (Unn,UX)) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in Unn \ (PartUnion (Unn,UX)) & Ball (b1,(3 / 2)) c= Unn ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in Unn \ (PartUnion (Unn,UX)) & Ball (b1,(3 / 2)) c= Unn ) } is set
B1 is set
k is Element of the carrier of PM
Ball (k,(1 / 2)) is Element of bool the carrier of PM
Ball (k,(3 / 2)) is Element of bool the carrier of PM
B1 is Element of bool (bool the carrier of PM)
k is set
q is Element of the carrier of PM
Ball (q,(1 / 2)) is Element of bool the carrier of PM
Ball (q,(3 / 2)) is Element of bool the carrier of PM
Unn is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
Unn + 1 is 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
B is 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
B + 1 is 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
2 |^ (B + 1) is 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
1 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
3 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
{ (union (UXk9 . b1)) where b1 is 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 : b1 <= B } is set
union { (union (UXk9 . b1)) where b1 is 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 : b1 <= B } is set
{ (union { H1(b2,B) where b2 is Element of the carrier of PM : ( S2[b2,b1,B] & not b2 in union { (union (UXk9 . b1)) where b3 is 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 : b1 <= B } ) } ) where b1 is Element of bool the carrier of PM : S1[b1] } is set
B1 is Element of bool the carrier of PM
PartUnion (B1,UX) is set
B1 \ (PartUnion (B1,UX)) is Element of bool the carrier of PM
{ H1(b1,B) where b1 is Element of the carrier of PM : ( S2[b1,B1,B] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= B } ) } is set
union { H1(b1,B) where b1 is Element of the carrier of PM : ( S2[b1,B1,B] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= B } ) } is set
q is set
s is Element of the carrier of PM
Ball (s,(1 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
Ball (s,(3 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
q is Element of bool (bool the carrier of PM)
s is set
b is Element of the carrier of PM
Ball (b,(1 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
Ball (b,(3 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
B + 1 is 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
2 |^ (B + 1) is 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
3 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
1 / (2 |^ (B + 1)) is V35() real ext-real non negative Element of REAL
Ball (b,(3 / (2 |^ (B + 1)))) is Element of bool the carrier of PM
n is 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
nm . n is Element of bool (bool the carrier of T)
m is Element of the carrier of T
Unn is Element of the carrier of PM
n + 2 is 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
2 |^ (n + 2) is 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
1 / (2 |^ (n + 2)) is V35() real ext-real non negative Element of REAL
Ball (Unn,(1 / (2 |^ (n + 2)))) is Element of bool the carrier of PM
Family_open_set PM is Element of bool (bool the carrier of PM)
B1 is open Element of bool the carrier of T
k is Element of bool the carrier of T
q is Element of bool the carrier of T
s is set
b is set
b is Element of the carrier of PM
dist (Unn,b) is V35() real ext-real Element of REAL
a is Element of the carrier of PM
dist (a,b) is V35() real ext-real Element of REAL
dist (a,Unn) is V35() real ext-real Element of REAL
(dist (a,Unn)) + (dist (Unn,b)) is V35() real ext-real Element of REAL
n + 1 is 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
(n + 1) + 1 is 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
2 |^ ((n + 1) + 1) is 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
2 |^ (n + 1) is 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
(2 |^ (n + 1)) * 2 is 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
dist (Unn,a) is V35() real ext-real Element of REAL
(1 / (2 |^ (n + 2))) + (1 / (2 |^ (n + 2))) is V35() real ext-real non negative Element of REAL
2 * (2 |^ (n + 1)) is 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
1 / (2 * (2 |^ (n + 1))) is V35() real ext-real non negative Element of REAL
2 * (1 / (2 * (2 |^ (n + 1)))) is V35() real ext-real non negative Element of REAL
2 * 1 is 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
(2 * 1) / (2 * (2 |^ (n + 1))) is V35() real ext-real non negative Element of REAL
2 / 2 is V35() real ext-real non negative Element of REAL
(2 / 2) * 1 is V35() real ext-real non negative Element of REAL
((2 / 2) * 1) / (2 |^ (n + 1)) is V35() real ext-real non negative Element of REAL
m is Element of bool the carrier of PM
PartUnion (m,UX) is set
m \ (PartUnion (m,UX)) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in m \ (PartUnion (m,UX)) & Ball (b1,(3 / 2)) c= m ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in m \ (PartUnion (m,UX)) & Ball (b1,(3 / 2)) c= m ) } is set
r is set
m is Element of the carrier of PM
Ball (m,(1 / 2)) is Element of bool the carrier of PM
Ball (m,(3 / 2)) is Element of bool the carrier of PM
dist (m,a) is V35() real ext-real Element of REAL
(1 / 2) + (1 / 2) is V35() real ext-real non negative Element of REAL
(dist (m,a)) + (dist (a,b)) is V35() real ext-real Element of REAL
dist (m,b) is V35() real ext-real Element of REAL
V is Element of bool the carrier of PM
PartUnion (V,UX) is set
V \ (PartUnion (V,UX)) is Element of bool the carrier of PM
{ (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in V \ (PartUnion (V,UX)) & Ball (b1,(3 / 2)) c= V ) } is set
union { (Ball (b1,(1 / 2))) where b1 is Element of the carrier of PM : ( b1 in V \ (PartUnion (V,UX)) & Ball (b1,(3 / 2)) c= V ) } is set
Ba is set
ca is Element of the carrier of PM
Ball (ca,(1 / 2)) is Element of bool the carrier of PM
Ball (ca,(3 / 2)) is Element of bool the carrier of PM
dist (m,ca) is V35() real ext-real Element of REAL
dist (b,ca) is V35() real ext-real Element of REAL
(dist (m,b)) + (dist (b,ca)) is V35() real ext-real Element of REAL
dist (ca,b) is V35() real ext-real Element of REAL
1 + (1 / 2) is non empty V35() real ext-real positive non negative Element of REAL
[m,V] is Element of [:(bool the carrier of PM),(bool the carrier of PM):]
[:(bool the carrier of PM),(bool the carrier of PM):] is non empty set
{m,V} is finite set
{m} is non empty trivial finite 1 -element set
{{m,V},{m}} is finite V49() set
[V,m] is Element of [:(bool the carrier of PM),(bool the carrier of PM):]
{V,m} is finite set
{V} is non empty trivial finite 1 -element set
{{V,m},{V}} is finite V49() set
UX -Seg V is set
UX -Seg m is set
union (UX -Seg V) is set
union (UX -Seg m) is set
m is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal set
m + 1 is 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
2 |^ n is 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
1 / (2 |^ n) is V35() real ext-real non negative Element of REAL
3 * (1 / (2 |^ n)) is V35() real ext-real non negative Element of REAL
3 * 1 is 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
(3 * 1) / (2 |^ n) is V35() real ext-real non negative Element of REAL
(2 |^ n) * 2 is 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
1 / (2 |^ (n + 1)) is V35() real ext-real non negative Element of REAL
m is 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
m + 1 is 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
2 |^ (m + 1) is 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
1 / (2 |^ (m + 1)) is V35() real ext-real non negative Element of REAL
3 / (2 |^ (m + 1)) is V35() real ext-real non negative Element of REAL
{ (union (UXk9 . b1)) where b1 is 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 : b1 <= m } is set
union { (union (UXk9 . b1)) where b1 is 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 : b1 <= m } is set
{ (union { H1(b2,m) where b2 is Element of the carrier of PM : ( S2[b2,b1,m] & not b2 in union { (union (UXk9 . b1)) where b3 is 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 : b1 <= m } ) } ) where b1 is Element of bool the carrier of PM : S1[b1] } is set
V is Element of bool the carrier of PM
PartUnion (V,UX) is set
V \ (PartUnion (V,UX)) is Element of bool the carrier of PM
{ H1(b1,m) where b1 is Element of the carrier of PM : ( S2[b1,V,m] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= m } ) } is set
union { H1(b1,m) where b1 is Element of the carrier of PM : ( S2[b1,V,m] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= m } ) } is set
Ba is set
ca is Element of the carrier of PM
Ball (ca,(1 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
Ball (ca,(3 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
dist (ca,a) is V35() real ext-real Element of REAL
(1 / (2 |^ n)) + (1 / (2 |^ n)) is V35() real ext-real non negative Element of REAL
(dist (ca,a)) + (dist (a,b)) is V35() real ext-real Element of REAL
dist (ca,b) is V35() real ext-real Element of REAL
W is Element of bool the carrier of PM
PartUnion (W,UX) is set
W \ (PartUnion (W,UX)) is Element of bool the carrier of PM
{ H1(b1,m) where b1 is Element of the carrier of PM : ( S2[b1,W,m] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= m } ) } is set
union { H1(b1,m) where b1 is Element of the carrier of PM : ( S2[b1,W,m] & not b1 in union { (union (UXk9 . b1)) where b2 is 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 : b1 <= m } ) } is set
Bb is set
cb is Element of the carrier of PM
Ball (cb,(1 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
Ball (cb,(3 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
dist (ca,cb) is V35() real ext-real Element of REAL
dist (b,cb) is V35() real ext-real Element of REAL
(dist (ca,b)) + (dist (b,cb)) is V35() real ext-real Element of REAL
dist (cb,b) is V35() real ext-real Element of REAL
((1 / (2 |^ n)) + (1 / (2 |^ n))) + (1 / (2 |^ n)) is V35() real ext-real non negative Element of REAL
m + 1 is 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
2 |^ (m + 1) is 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
3 / (2 |^ (m + 1)) is V35() real ext-real non negative Element of REAL
Ball (cb,(3 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
Ball (ca,(3 / (2 |^ (m + 1)))) is Element of bool the carrier of PM
[V,W] is Element of [:(bool the carrier of PM),(bool the carrier of PM):]
[:(bool the carrier of PM),(bool the carrier of PM):] is non empty set
{V,W} is finite set
{V} is non empty trivial finite 1 -element set
{{V,W},{V}} is finite V49() set
[W,V] is Element of [:(bool the carrier of PM),(bool the carrier of PM):]
{W,V} is finite set
{W} is non empty trivial finite 1 -element set
{{W,V},{W}} is finite V49() set
UX -Seg W is set
UX -Seg V is set
union (UX -Seg W) is set
union (UX -Seg V) is set
k is Element of bool the carrier of T
q is Element of bool the carrier of T
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
[: the carrier of T, the carrier of T:] is non empty set
[:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite complex-valued ext-real-valued real-valued set
bool [:[: the carrier of T, the carrier of T:],REAL:] is non empty non trivial non finite set
the topology of T is non empty Element of bool (bool the carrier of T)
Bn is Relation-like [: the carrier of T, the carrier of T:] -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:[: the carrier of T, the carrier of T:],REAL:]
SpaceMetr ( the carrier of T,Bn) is strict Reflexive discerning symmetric triangle MetrStruct
Family_open_set (SpaceMetr ( the carrier of T,Bn)) is Element of bool (bool the carrier of (SpaceMetr ( the carrier of T,Bn)))
the carrier of (SpaceMetr ( the carrier of T,Bn)) is set
bool the carrier of (SpaceMetr ( the carrier of T,Bn)) is non empty set
bool (bool the carrier of (SpaceMetr ( the carrier of T,Bn))) is non empty set
bool the carrier of T is non empty Element of bool (bool the carrier of T)
bool (bool the carrier of T) is non empty Element of bool (bool (bool the carrier of T))
bool (bool the carrier of T) is non empty set
bool (bool (bool the carrier of T)) is non empty set
PM is non empty Reflexive discerning symmetric triangle Discerning MetrStruct
the carrier of PM is non empty set
{ (Ball (b1,(1 / (2 |^ (In (a1,NAT)))))) where b1 is Element of the carrier of PM : b1 is Element of the carrier of PM } is set
FB is set
In (FB,NAT) is 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
2 |^ (In (FB,NAT)) is 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
1 / (2 |^ (In (FB,NAT))) is V35() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ (In (FB,NAT)))))) where b1 is Element of the carrier of PM : b1 is Element of the carrier of PM } is set
TPM is 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
In (TPM,NAT) is 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
2 |^ (In (TPM,NAT)) is 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
1 / (2 |^ (In (TPM,NAT))) is V35() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ (In (TPM,NAT)))))) where b1 is Element of the carrier of PM : b1 is Element of the carrier of PM } is set
Un is set
2 |^ TPM is 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
1 / (2 |^ TPM) is V35() real ext-real non negative Element of REAL
Family_open_set PM is Element of bool (bool the carrier of PM)
bool the carrier of PM is non empty set
bool (bool the carrier of PM) is non empty set
UX is Element of the carrier of PM
Ball (UX,(1 / (2 |^ TPM))) is Element of bool the carrier of PM
FB is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
TopSpaceMetr PM is TopStruct
Family_open_set PM is Element of bool (bool the carrier of PM)
bool the carrier of PM is non empty set
bool (bool the carrier of PM) is non empty set
TopStruct(# the carrier of PM,(Family_open_set PM) #) is non empty strict TopStruct
[#] T is non empty non proper open closed Element of bool the carrier of T
[#] (TopSpaceMetr PM) is non proper Element of bool the carrier of (TopSpaceMetr PM)
the carrier of (TopSpaceMetr PM) is set
bool the carrier of (TopSpaceMetr PM) is non empty set
Funcs (NAT,(bool (bool the carrier of T))) is functional non empty FUNCTION_DOMAIN of NAT , bool (bool the carrier of T)
Un is 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
FB . Un is set
In (Un,NAT) is 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
UX is Element of bool the carrier of T
FB . Un is Element of bool (bool the carrier of T)
2 |^ (In (Un,NAT)) is 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
1 / (2 |^ (In (Un,NAT))) is V35() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ (In (Un,NAT)))))) where b1 is Element of the carrier of PM : b1 is Element of the carrier of PM } is set
2 |^ Un is 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
1 / (2 |^ Un) is V35() real ext-real non negative Element of REAL
UXk is Element of the carrier of PM
Ball (UXk,(1 / (2 |^ Un))) is Element of bool the carrier of PM
union (FB . Un) is Element of bool the carrier of T
UX is set
UXk is Element of the carrier of PM
Ball (UXk,(1 / (2 |^ Un))) is Element of bool the carrier of PM
UX is set
UXk is set
k is Element of the carrier of PM
Ball (k,(1 / (2 |^ Un))) is Element of bool the carrier of PM
UX is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union UX is Element of bool (bool the carrier of T)
[:NAT,(Funcs (NAT,(bool (bool the carrier of T)))):] is non empty non trivial non finite set
bool [:NAT,(Funcs (NAT,(bool (bool the carrier of T)))):] is non empty non trivial non finite set
Un is Relation-like NAT -defined Funcs (NAT,(bool (bool the carrier of T))) -valued Function-like non empty total quasi_total Element of bool [:NAT,(Funcs (NAT,(bool (bool the carrier of T)))):]
UX is set
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
UXk is 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
k is set
() . k is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
UXk9 is set
nm is set
[UXk9,nm] is set
{UXk9,nm} is finite set
{UXk9} is non empty trivial finite 1 -element set
{{UXk9,nm},{UXk9}} is finite V49() set
Un . UXk9 is Relation-like Function-like set
n is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
n . nm is set
m is set
dom n is V76() V77() V78() V79() V80() V81() Element of bool NAT
rng n is Element of bool (bool (bool the carrier of T))
bool (bool (bool the carrier of T)) is non empty set
Unn is 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
B is 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
[Unn,B] is Element of [:NAT,NAT:]
{Unn,B} is finite V49() V76() V77() V78() V79() V80() V81() set
{Unn} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{Unn,B},{Unn}} is finite V49() set
() . [Unn,B] is 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
B1 is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Un . Unn is Relation-like Function-like Element of Funcs (NAT,(bool (bool the carrier of T)))
B1 . B is Element of bool (bool the carrier of T)
B1 is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
B1 . B is Element of bool (bool the carrier of T)
Unn is 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
B is 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
[Unn,B] is Element of [:NAT,NAT:]
{Unn,B} is finite V49() V76() V77() V78() V79() V80() V81() set
{Unn} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{Unn,B},{Unn}} is finite V49() set
() . [Unn,B] is 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
B1 is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Un . Unn is Relation-like Function-like Element of Funcs (NAT,(bool (bool the carrier of T)))
B1 . B is Element of bool (bool the carrier of T)
[:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
UX is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union UX is Element of bool (bool the carrier of T)
UXk is Element of bool the carrier of T
k is Element of the carrier of T
UXk9 is Element of the carrier of PM
nm is V35() real ext-real Element of REAL
Ball (UXk9,nm) is Element of bool the carrier of PM
n is 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
2 |^ n is 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
1 / (2 |^ n) is V35() real ext-real non negative Element of REAL
n + 1 is 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
Un . (n + 1) is Relation-like Function-like Element of Funcs (NAT,(bool (bool the carrier of T)))
FB . (n + 1) is Element of bool (bool the carrier of T)
m is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union m is Element of bool (bool the carrier of T)
union (Union m) is Element of bool the carrier of T
Unn is set
B is Element of bool the carrier of PM
B1 is set
k is 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
m . k is Element of bool (bool the carrier of T)
In ((n + 1),NAT) is 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
2 |^ (In ((n + 1),NAT)) is 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
1 / (2 |^ (In ((n + 1),NAT))) is V35() real ext-real non negative Element of REAL
{ (Ball (b1,(1 / (2 |^ (In ((n + 1),NAT)))))) where b1 is Element of the carrier of PM : b1 is Element of the carrier of PM } is set
2 |^ (n + 1) is 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
1 / (2 |^ (n + 1)) is V35() real ext-real non negative Element of REAL
q is Element of the carrier of PM
Ball (q,(1 / (2 |^ (n + 1)))) is Element of bool the carrier of PM
s is Element of the carrier of PM
dist (q,s) is V35() real ext-real Element of REAL
dist (q,UXk9) is V35() real ext-real Element of REAL
dist (UXk9,s) is V35() real ext-real Element of REAL
(dist (q,UXk9)) + (dist (q,s)) is V35() real ext-real Element of REAL
(1 / (2 |^ (n + 1))) + (1 / (2 |^ (n + 1))) is V35() real ext-real non negative Element of REAL
2 * (1 / (2 |^ (n + 1))) is V35() real ext-real non negative Element of REAL
(2 |^ n) * 2 is 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
1 / ((2 |^ n) * 2) is V35() real ext-real non negative Element of REAL
(1 / ((2 |^ n) * 2)) * 2 is V35() real ext-real non negative Element of REAL
[(n + 1),k] is Element of [:NAT,NAT:]
{(n + 1),k} is finite V49() V76() V77() V78() V79() V80() V81() set
{(n + 1)} is non empty trivial finite V49() 1 -element V76() V77() V78() V79() V80() V81() set
{{(n + 1),k},{(n + 1)}} is finite V49() set
() . [(n + 1),k] is 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
UX . (() . [(n + 1),k]) is Element of bool (bool the carrier of T)
UXk is 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
UX . UXk is Element of bool (bool the carrier of T)
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
k is set
() . k is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
UXk9 is set
nm is set
[UXk9,nm] is set
{UXk9,nm} is finite set
{UXk9} is non empty trivial finite 1 -element set
{{UXk9,nm},{UXk9}} is finite V49() set
Un . UXk9 is Relation-like Function-like set
FB . UXk9 is set
n is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union n is Element of bool (bool the carrier of T)
dom n is V76() V77() V78() V79() V80() V81() Element of bool NAT
n . nm is set
rng n is Element of bool (bool (bool the carrier of T))
bool (bool (bool the carrier of T)) is non empty set
m is Element of bool (bool the carrier of T)
UXk is set
k is 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
UX . k is Element of bool (bool the carrier of T)
rng () is V76() V77() V78() V79() V80() V81() Element of bool NAT
dom () is Relation-like NAT -defined NAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
bool [:NAT,NAT:] is non empty non trivial non finite set
nm is set
() . nm is epsilon-transitive epsilon-connected ordinal natural V35() real ext-real non negative finite cardinal Element of REAL
n is set
m is set
[n,m] is set
{n,m} is finite set
{n} is non empty trivial finite 1 -element set
{{n,m},{n}} is finite V49() set
Un . n is Relation-like Function-like set
Unn is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Unn . m is set
Union Unn is Element of bool (bool the carrier of T)
FB . n is set
UXk9 is Element of bool the carrier of T
B is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union B is Element of bool (bool the carrier of T)
T is non empty TopSpace-like TopStruct
the carrier of T is non empty set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
[:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
bool [:NAT,(bool (bool the carrier of T)):] is non empty non trivial non finite set
Bn is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Bn is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]
Union Bn is Element of bool (bool the carrier of T)
Bn is Relation-like NAT -defined bool (bool the carrier of T) -valued Function-like non empty total quasi_total Element of bool [:NAT,(bool (bool the carrier of T)):]