REAL is non empty V13() V36() V144() V145() V146() V150() non bounded_below non bounded_above interval set
NAT is non empty epsilon-transitive epsilon-connected ordinal V13() V144() V145() V146() V147() V148() V149() V150() left_end bounded_below Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V36() V144() V150() set
omega is non empty epsilon-transitive epsilon-connected ordinal V13() V144() V145() V146() V147() V148() V149() V150() left_end bounded_below set
bool omega is non empty set
[:NAT,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
RAT is non empty V36() V144() V145() V146() V147() V150() set
INT is non empty V36() V144() V145() V146() V147() V148() V150() set
[:COMPLEX,COMPLEX:] is non empty complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty V23( RAT ) complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V23( RAT ) complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty set
bool NAT is non empty set
K298() is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V62() V144() V145() V146() V147() V148() V149() left_end bounded_below Element of NAT
[:1,1:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued natural-valued set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V61() V62() V144() V145() V146() V147() V148() V149() left_end bounded_below Element of NAT
[:2,2:] is non empty V23( RAT ) V23( INT ) complex-valued ext-real-valued real-valued natural-valued set
[:[:2,2:],REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:[:2,2:],REAL:] is non empty set
K433() is non empty strict TopSpace-like V143() TopStruct
the carrier of K433() is non empty V144() V145() V146() set
RealSpace is strict V143() MetrStruct
R^1 is non empty strict TopSpace-like V143() TopStruct
ExtREAL is non empty V145() interval set
[:COMPLEX,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like T_0 T_1 T_2 V203() V228() V229() V230() V231() V232() V233() V234() strict V241() V242() L15()
the carrier of (TOP-REAL 2) is non empty functional set
[: the carrier of (TOP-REAL 2),REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty set
bool the carrier of (TOP-REAL 2) is non empty set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V144() V145() V146() V147() V148() V149() V150() bounded_below interval set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V144() V145() V146() V147() V148() V149() V150() bounded_below interval set
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
bool [:NAT,NAT:] is non empty set
the carrier of R^1 is non empty V144() V145() V146() set
bool the carrier of R^1 is non empty set
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
proj2 is non empty V19() V22( the carrier of (TOP-REAL 2)) V23( REAL ) Function-like V29( the carrier of (TOP-REAL 2)) V33( the carrier of (TOP-REAL 2), REAL ) complex-valued ext-real-valued real-valued continuous Element of bool [: the carrier of (TOP-REAL 2),REAL:]
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
F1() is non empty set
{ F2(b1) where b1 is Element of F1() : verum } is set
S is set
F2(S) is set
S is V11() real ext-real set
C is V11() real ext-real set
S + C is V11() real ext-real set
(S + C) / 2 is V11() real ext-real Element of REAL
r is V11() real ext-real set
x is V11() real ext-real set
[.r,x.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( r <= b1 & b1 <= x ) } is set
s is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
t + s is V11() real ext-real Element of REAL
p + p is V11() real ext-real Element of REAL
(t + s) / 2 is V11() real ext-real Element of REAL
(p + p) / 2 is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
P + P is V11() real ext-real Element of REAL
(P + P) / 2 is V11() real ext-real Element of REAL
S is V11() real ext-real set
C is V11() real ext-real set
S - C is V11() real ext-real set
abs (S - C) is V11() real ext-real Element of REAL
r is V11() real ext-real set
S - r is V11() real ext-real set
abs (S - r) is V11() real ext-real Element of REAL
x is V11() real ext-real set
r - x is V11() real ext-real set
abs (r - x) is V11() real ext-real Element of REAL
(abs (S - C)) - (abs (r - x)) is V11() real ext-real Element of REAL
abs ((abs (S - C)) - (abs (r - x))) is V11() real ext-real Element of REAL
C - x is V11() real ext-real set
abs (C - x) is V11() real ext-real Element of REAL
(abs (S - r)) + (abs (C - x)) is V11() real ext-real Element of REAL
(S - C) - (r - x) is V11() real ext-real set
(S - r) - (C - x) is V11() real ext-real set
abs ((S - C) - (r - x)) is V11() real ext-real Element of REAL
S is V11() real ext-real set
abs S is V11() real ext-real Element of REAL
C is V11() real ext-real set
abs C is V11() real ext-real Element of REAL
r is V11() real ext-real set
].C,r.[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= C & not r <= b1 ) } is set
abs r is V11() real ext-real Element of REAL
max ((abs C),(abs r)) is V11() real ext-real set
P is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
abs P is V11() real ext-real Element of REAL
abs p is V11() real ext-real Element of REAL
- P is V11() real ext-real Element of REAL
abs P is V11() real ext-real Element of REAL
- x is V11() real ext-real Element of REAL
abs x is V11() real ext-real Element of REAL
F1() is non empty set
F2() is non empty set
F3() is non empty set
[:F1(),F2():] is non empty set
bool [:F1(),F2():] is non empty set
[:F1(),F3():] is non empty set
bool [:F1(),F3():] is non empty set
[:F2(),F3():] is non empty set
S is Element of F1()
C is Element of F2()
r is Element of F3()
[C,r] is V30() set
{C,r} is set
{C} is set
{{C,r},{C}} is set
[C,r] `1 is set
[C,r] `2 is set
[:F1(),[:F2(),F3():]:] is non empty set
bool [:F1(),[:F2(),F3():]:] is non empty set
S is non empty V19() V22(F1()) V23([:F2(),F3():]) Function-like V29(F1()) V33(F1(),[:F2(),F3():]) Element of bool [:F1(),[:F2(),F3():]:]
pr1 S is non empty V19() V22(F1()) V23(F2()) Function-like V29(F1()) V33(F1(),F2()) Element of bool [:F1(),F2():]
pr2 S is non empty V19() V22(F1()) V23(F3()) Function-like V29(F1()) V33(F1(),F3()) Element of bool [:F1(),F3():]
C is Element of F1()
(pr1 S) . C is Element of F2()
(pr2 S) . C is Element of F3()
S . C is Element of [:F2(),F3():]
(S . C) `2 is set
(S . C) `1 is set
S is non empty TopSpace-like TopStruct
C is non empty TopSpace-like TopStruct
[:S,C:] is non empty strict TopSpace-like TopStruct
the carrier of [:S,C:] is non empty set
bool the carrier of [:S,C:] is non empty set
the carrier of S is non empty set
bool the carrier of S is non empty set
the carrier of C is non empty set
bool the carrier of C is non empty set
r is Element of bool the carrier of [:S,C:]
{ [:b1,b2:] where b1 is Element of bool the carrier of S, b2 is Element of bool the carrier of C : ( b1 is open & b2 is open & [:b1,b2:] c= r ) } is set
P is set
p is Element of bool the carrier of S
t is Element of bool the carrier of C
[:p,t:] is Element of bool the carrier of [:S,C:]
bool (bool the carrier of [:S,C:]) is non empty set
P is Element of bool (bool the carrier of [:S,C:])
p is Element of bool (bool the carrier of [:S,C:])
t is set
s is Element of bool the carrier of S
sa is Element of bool the carrier of C
[:s,sa:] is Element of bool the carrier of [:S,C:]
s is set
sa is Element of bool the carrier of S
sb is Element of bool the carrier of C
[:sa,sb:] is Element of bool the carrier of [:S,C:]
union p is set
t is set
s is Element of bool the carrier of S
sa is Element of bool the carrier of C
[:s,sa:] is Element of bool the carrier of [:S,C:]
S is V144() V145() V146() compact Element of bool REAL
C is V144() V145() V146() compact Element of bool REAL
S /\ C is V144() V145() V146() Element of bool REAL
r is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
proj2 r is V144() V145() V146() set
rng r is V144() V145() V146() Element of bool REAL
x is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim x is V11() real ext-real Element of REAL
rng x is V144() V145() V146() Element of bool REAL
P is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim P is V11() real ext-real Element of REAL
S is non empty TopSpace-like TopStruct
the carrier of S is non empty set
[: the carrier of S,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of S,REAL:] is non empty set
bool the carrier of S is non empty set
C is non empty V19() V22( the carrier of S) V23( REAL ) Function-like V29( the carrier of S) V33( the carrier of S, REAL ) complex-valued ext-real-valued real-valued continuous Element of bool [: the carrier of S,REAL:]
r is Element of bool the carrier of S
C .: r is V144() V145() V146() Element of bool REAL
x is ext-real set
P is ext-real set
[.x,P.] is interval set
C " (C .: r) is Element of bool the carrier of S
p is Element of the carrier of S
C . p is V11() real ext-real Element of REAL
t is Element of the carrier of S
C . t is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
sa is V11() real ext-real Element of REAL
[.s,sa.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( s <= b1 & b1 <= sa ) } is set
sb is V11() real ext-real Element of REAL
gb is V11() real ext-real Element of REAL
left_open_halfline gb is V144() V145() V146() open Element of bool REAL
].-infty,gb.[ is non left_end non right_end interval set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= -infty & not gb <= b1 ) } is set
C " (left_open_halfline gb) is Element of bool the carrier of S
right_open_halfline gb is V144() V145() V146() open Element of bool REAL
].gb,+infty.[ is non left_end non right_end interval set
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= gb & not +infty <= b1 ) } is set
C " (right_open_halfline gb) is Element of bool the carrier of S
(C " (left_open_halfline gb)) /\ r is Element of bool the carrier of S
(C " (right_open_halfline gb)) /\ r is Element of bool the carrier of S
(left_open_halfline gb) \/ (right_open_halfline gb) is V144() V145() V146() Element of bool REAL
Nseq is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not b1 <= gb } is set
{} S is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative closed compact V144() V145() V146() V147() V148() V149() V150() bounded_below interval Element of bool the carrier of S
(left_open_halfline gb) /\ (right_open_halfline gb) is V144() V145() V146() Element of bool REAL
].gb,gb.[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= gb & not gb <= b1 ) } is set
(C " (left_open_halfline gb)) /\ (C " (right_open_halfline gb)) is Element of bool the carrier of S
((C " (left_open_halfline gb)) /\ r) \/ ((C " (right_open_halfline gb)) /\ r) is Element of bool the carrier of S
{gb} is V144() V145() V146() Element of bool REAL
ff is V144() V145() V146() Element of bool REAL
ff ` is V144() V145() V146() Element of bool REAL
REAL \ ff is V144() V145() V146() set
[.gb,gb.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( gb <= b1 & b1 <= gb ) } is set
REAL \ [.gb,gb.] is V144() V145() V146() Element of bool REAL
C " ff is Element of bool the carrier of S
(C " ff) ` is Element of bool the carrier of S
the carrier of S \ (C " ff) is set
C " ((left_open_halfline gb) \/ (right_open_halfline gb)) is Element of bool the carrier of S
(C " (left_open_halfline gb)) \/ (C " (right_open_halfline gb)) is Element of bool the carrier of S
C " {gb} is Element of bool the carrier of S
r /\ ((C " (left_open_halfline gb)) \/ (C " (right_open_halfline gb))) is Element of bool the carrier of S
ga is V11() real ext-real Element of REAL
{ b1 where b1 is V11() real ext-real Element of REAL : not gb <= b1 } is set
S is V144() V145() V146() Element of bool REAL
C is V144() V145() V146() Element of bool REAL
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in S & b2 in C ) } is set
x is set
P is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
abs (P - p) is V11() real ext-real Element of REAL
x is V144() V145() V146() Element of bool REAL
lower_bound x is V11() real ext-real Element of REAL
P is V144() V145() V146() Element of bool REAL
r is V11() real ext-real set
lower_bound P is V11() real ext-real Element of REAL
p is V144() V145() V146() Element of bool REAL
x is V11() real ext-real set
lower_bound p is V11() real ext-real Element of REAL
r is V11() real ext-real set
x is V144() V145() V146() Element of bool REAL
P is V144() V145() V146() Element of bool REAL
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in x & b2 in P ) } is set
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in P & b2 in x ) } is set
p is V144() V145() V146() Element of bool REAL
lower_bound p is V11() real ext-real Element of REAL
s is set
sa is V11() real ext-real Element of REAL
sb is V11() real ext-real Element of REAL
sa - sb is V11() real ext-real Element of REAL
abs (sa - sb) is V11() real ext-real Element of REAL
s is V144() V145() V146() Element of bool REAL
lower_bound s is V11() real ext-real Element of REAL
sa is set
sb is V11() real ext-real Element of REAL
ga is V11() real ext-real Element of REAL
sb - ga is V11() real ext-real Element of REAL
abs (sb - ga) is V11() real ext-real Element of REAL
ga - sb is V11() real ext-real Element of REAL
abs (ga - sb) is V11() real ext-real Element of REAL
sa is set
sb is V11() real ext-real Element of REAL
ga is V11() real ext-real Element of REAL
sb - ga is V11() real ext-real Element of REAL
abs (sb - ga) is V11() real ext-real Element of REAL
ga - sb is V11() real ext-real Element of REAL
abs (ga - sb) is V11() real ext-real Element of REAL
S is V144() V145() V146() Element of bool REAL
C is V144() V145() V146() Element of bool REAL
(S,C) is V11() real ext-real set
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in S & b2 in C ) } is set
x is V11() real ext-real set
P is V11() real ext-real set
x - P is V11() real ext-real set
abs (x - P) is V11() real ext-real Element of REAL
p is set
t is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
t - s is V11() real ext-real Element of REAL
abs (t - s) is V11() real ext-real Element of REAL
p is V144() V145() V146() Element of bool REAL
t is ext-real set
s is V11() real ext-real Element of REAL
sa is V11() real ext-real Element of REAL
s - sa is V11() real ext-real Element of REAL
abs (s - sa) is V11() real ext-real Element of REAL
lower_bound p is V11() real ext-real Element of REAL
S is V144() V145() V146() Element of bool REAL
C is V144() V145() V146() Element of bool REAL
(S,C) is V11() real ext-real set
r is non empty V144() V145() V146() Element of bool REAL
x is non empty V144() V145() V146() Element of bool REAL
(r,x) is V11() real ext-real set
P is set
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in r & b2 in x ) } is set
t is set
s is set
sa is V11() real ext-real Element of REAL
sb is V11() real ext-real Element of REAL
sa - sb is V11() real ext-real Element of REAL
abs (sa - sb) is V11() real ext-real Element of REAL
s is V11() real ext-real set
sa is V11() real ext-real set
s - sa is V11() real ext-real set
abs (s - sa) is V11() real ext-real Element of REAL
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in S & b2 in C ) } is set
Nseq is set
gb is V11() real ext-real Element of REAL
fb is V11() real ext-real Element of REAL
gb - fb is V11() real ext-real Element of REAL
abs (gb - fb) is V11() real ext-real Element of REAL
sb is non empty V144() V145() V146() Element of bool REAL
Nseq is V144() V145() V146() Element of bool REAL
gb is set
fb is V11() real ext-real Element of REAL
Nseq1 is V11() real ext-real Element of REAL
fb - Nseq1 is V11() real ext-real Element of REAL
abs (fb - Nseq1) is V11() real ext-real Element of REAL
gb is ext-real set
fb is V11() real ext-real Element of REAL
Nseq1 is V11() real ext-real Element of REAL
fb - Nseq1 is V11() real ext-real Element of REAL
abs (fb - Nseq1) is V11() real ext-real Element of REAL
lower_bound sb is V11() real ext-real Element of REAL
lower_bound Nseq is V11() real ext-real Element of REAL
S is non empty V144() V145() V146() compact Element of bool REAL
C is non empty V144() V145() V146() compact Element of bool REAL
(S,C) is V11() real ext-real set
x is non empty compact V144() V145() V146() Element of bool the carrier of R^1
R^1 | x is non empty strict TopSpace-like compact V143() pseudocompact SubSpace of R^1
the carrier of (R^1 | x) is non empty V144() V145() V146() set
r is non empty compact V144() V145() V146() Element of bool the carrier of R^1
R^1 | r is non empty strict TopSpace-like compact V143() pseudocompact SubSpace of R^1
[:(R^1 | r),(R^1 | x):] is non empty strict TopSpace-like compact pseudocompact TopStruct
the carrier of (R^1 | r) is non empty V144() V145() V146() set
P is non empty TopSpace-like compact pseudocompact TopStruct
the carrier of P is non empty set
p is Element of the carrier of P
[:S,C:] is non empty V19() V22( REAL ) V23( REAL ) complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
t is set
s is set
[t,s] is V30() set
{t,s} is set
{t} is set
{{t,s},{t}} is set
sa is V11() real ext-real Element of REAL
sb is V11() real ext-real Element of REAL
sa - sb is V11() real ext-real Element of REAL
abs (sa - sb) is V11() real ext-real Element of REAL
ga is V11() real ext-real Element of REAL
[: the carrier of P,REAL:] is non empty complex-valued ext-real-valued real-valued set
bool [: the carrier of P,REAL:] is non empty set
p is non empty V19() V22( the carrier of P) V23( REAL ) Function-like V29( the carrier of P) V33( the carrier of P, REAL ) complex-valued ext-real-valued real-valued Element of bool [: the carrier of P,REAL:]
t is V144() V145() V146() Element of bool REAL
p " t is Element of bool the carrier of P
bool the carrier of P is non empty set
bool the carrier of (R^1 | r) is non empty set
bool the carrier of (R^1 | x) is non empty set
s is Element of the carrier of P
p . s is V11() real ext-real Element of REAL
sa is V11() real ext-real Element of REAL
sb is V11() real ext-real Element of REAL
[sa,sb] is V30() set
{sa,sb} is V144() V145() V146() set
{sa} is V144() V145() V146() set
{{sa,sb},{sa}} is set
sa - sb is V11() real ext-real Element of REAL
abs (sa - sb) is V11() real ext-real Element of REAL
ga is V144() V145() V146() Neighbourhood of p . s
Nseq is V11() real ext-real set
(p . s) - Nseq is V11() real ext-real Element of REAL
(p . s) + Nseq is V11() real ext-real Element of REAL
].((p . s) - Nseq),((p . s) + Nseq).[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= (p . s) - Nseq & not (p . s) + Nseq <= b1 ) } is set
Nseq / 2 is V11() real ext-real Element of REAL
sa - (Nseq / 2) is V11() real ext-real Element of REAL
sa + (Nseq / 2) is V11() real ext-real Element of REAL
sb - (Nseq / 2) is V11() real ext-real Element of REAL
sb + (Nseq / 2) is V11() real ext-real Element of REAL
gb is V11() real ext-real Element of REAL
fb is V11() real ext-real Element of REAL
].gb,fb.[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= gb & not fb <= b1 ) } is set
Nseq1 is V11() real ext-real Element of REAL
fa is V11() real ext-real Element of REAL
].Nseq1,fa.[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= Nseq1 & not fa <= b1 ) } is set
d0 is V144() V145() V146() Element of bool the carrier of R^1
d0 /\ C is V144() V145() V146() Element of bool REAL
r is V144() V145() V146() Element of bool the carrier of R^1
r /\ S is V144() V145() V146() Element of bool REAL
k0 is V144() V145() V146() Element of bool the carrier of (R^1 | r)
ff is V144() V145() V146() Element of bool the carrier of (R^1 | x)
[:k0,ff:] is complex-valued ext-real-valued real-valued Element of bool the carrier of [:(R^1 | r),(R^1 | x):]
the carrier of [:(R^1 | r),(R^1 | x):] is non empty set
bool the carrier of [:(R^1 | r),(R^1 | x):] is non empty set
p .: [:k0,ff:] is V144() V145() V146() Element of bool REAL
i is set
k is Element of the carrier of P
p . k is V11() real ext-real Element of REAL
j is V11() real ext-real Element of REAL
di is V11() real ext-real Element of REAL
[j,di] is V30() set
{j,di} is V144() V145() V146() set
{j} is V144() V145() V146() set
{{j,di},{j}} is set
j - di is V11() real ext-real Element of REAL
abs (j - di) is V11() real ext-real Element of REAL
(abs (j - di)) - (abs (sa - sb)) is V11() real ext-real Element of REAL
abs ((abs (j - di)) - (abs (sa - sb))) is V11() real ext-real Element of REAL
j - sa is V11() real ext-real Element of REAL
abs (j - sa) is V11() real ext-real Element of REAL
di - sb is V11() real ext-real Element of REAL
abs (di - sb) is V11() real ext-real Element of REAL
(abs (j - sa)) + (abs (di - sb)) is V11() real ext-real Element of REAL
].(sb - (Nseq / 2)),(sb + (Nseq / 2)).[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= sb - (Nseq / 2) & not sb + (Nseq / 2) <= b1 ) } is set
].(sa - (Nseq / 2)),(sa + (Nseq / 2)).[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= sa - (Nseq / 2) & not sa + (Nseq / 2) <= b1 ) } is set
(Nseq / 2) + (Nseq / 2) is V11() real ext-real Element of REAL
dom p is Element of bool the carrier of P
t is non empty V19() V22( the carrier of P) V23( REAL ) Function-like V29( the carrier of P) V33( the carrier of P, REAL ) complex-valued ext-real-valued real-valued with_max with_min continuous bounded Element of bool [: the carrier of P,REAL:]
t .: the carrier of P is non empty V144() V145() V146() Element of bool REAL
lower_bound (t .: the carrier of P) is V11() real ext-real Element of REAL
s is Element of the carrier of P
t . s is V11() real ext-real Element of REAL
sa is set
sb is set
[sa,sb] is V30() set
{sa,sb} is set
{sa} is set
{{sa,sb},{sa}} is set
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in S & b2 in C ) } is set
ga is set
Nseq is Element of the carrier of P
t . Nseq is V11() real ext-real Element of REAL
gb is V11() real ext-real Element of REAL
fb is V11() real ext-real Element of REAL
[gb,fb] is V30() set
{gb,fb} is V144() V145() V146() set
{gb} is V144() V145() V146() set
{{gb,fb},{gb}} is set
gb - fb is V11() real ext-real Element of REAL
abs (gb - fb) is V11() real ext-real Element of REAL
ga is set
Nseq is V11() real ext-real Element of REAL
gb is V11() real ext-real Element of REAL
Nseq - gb is V11() real ext-real Element of REAL
abs (Nseq - gb) is V11() real ext-real Element of REAL
[Nseq,gb] is V30() set
{Nseq,gb} is V144() V145() V146() set
{Nseq} is V144() V145() V146() set
{{Nseq,gb},{Nseq}} is set
fb is Element of the carrier of P
t . fb is V11() real ext-real Element of REAL
Nseq1 is V11() real ext-real Element of REAL
fa is V11() real ext-real Element of REAL
[Nseq1,fa] is V30() set
{Nseq1,fa} is V144() V145() V146() set
{Nseq1} is V144() V145() V146() set
{{Nseq1,fa},{Nseq1}} is set
Nseq1 - fa is V11() real ext-real Element of REAL
abs (Nseq1 - fa) is V11() real ext-real Element of REAL
ga is V11() real ext-real set
Nseq is V11() real ext-real set
ga - Nseq is V11() real ext-real set
abs (ga - Nseq) is V11() real ext-real Element of REAL
gb is V11() real ext-real Element of REAL
fb is V11() real ext-real Element of REAL
[gb,fb] is V30() set
{gb,fb} is V144() V145() V146() set
{gb} is V144() V145() V146() set
{{gb,fb},{gb}} is set
gb - fb is V11() real ext-real Element of REAL
abs (gb - fb) is V11() real ext-real Element of REAL
S is non empty V144() V145() V146() compact Element of bool REAL
C is non empty V144() V145() V146() compact Element of bool REAL
(S,C) is V11() real ext-real set
{ (abs (b1 - b2)) where b1, b2 is V11() real ext-real Element of REAL : ( b1 in S & b2 in C ) } is set
x is set
P is set
p is V11() real ext-real Element of REAL
t is V11() real ext-real Element of REAL
p - t is V11() real ext-real Element of REAL
abs (p - t) is V11() real ext-real Element of REAL
P is set
p is V11() real ext-real set
t is V11() real ext-real set
p - t is V11() real ext-real set
abs (p - t) is V11() real ext-real Element of REAL
s is non empty V144() V145() V146() Element of bool REAL
sa is V11() real ext-real set
sb is V11() real ext-real Element of REAL
ga is V11() real ext-real Element of REAL
sb - ga is V11() real ext-real Element of REAL
abs (sb - ga) is V11() real ext-real Element of REAL
lower_bound s is V11() real ext-real Element of REAL
S is non empty V144() V145() V146() compact Element of bool REAL
C is non empty V144() V145() V146() compact Element of bool REAL
(S,C) is V11() real ext-real set
r is V11() real ext-real set
x is V11() real ext-real set
r - x is V11() real ext-real set
abs (r - x) is V11() real ext-real Element of REAL
P is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
P - p is V11() real ext-real Element of REAL
abs (P - p) is V11() real ext-real Element of REAL
[:NAT,(bool REAL):] is non empty set
bool [:NAT,(bool REAL):] is non empty set
S is V11() real ext-real set
C is V11() real ext-real set
[.S,C.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( S <= b1 & b1 <= C ) } is set
r is V144() V145() V146() compact Element of bool REAL
x is V144() V145() V146() compact Element of bool REAL
r \/ x is V144() V145() V146() Element of bool REAL
P is non empty V19() V22( NAT ) V23( bool REAL) Function-like V29( NAT ) V33( NAT , bool REAL) Element of bool [:NAT,(bool REAL):]
p is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
P . p is set
P . p is V144() V145() V146() Element of bool REAL
t is set
s is set
sb is V11() real ext-real Element of REAL
sa is V11() real ext-real Element of REAL
[.sb,sa.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sb <= b1 & b1 <= sa ) } is set
sa is V11() real ext-real Element of REAL
sb is V11() real ext-real Element of REAL
[.sa,sb.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sa <= b1 & b1 <= sb ) } is set
sb is V11() real ext-real Element of REAL
sa is V11() real ext-real Element of REAL
p is non empty V19() V22( NAT ) V23( bool REAL) Function-like V29( NAT ) V33( NAT , bool REAL) Element of bool [:NAT,(bool REAL):]
p . 0 is V144() V145() V146() Element of bool REAL
t is non empty V19() V22( NAT ) V23( bool REAL) Function-like V29( NAT ) V33( NAT , bool REAL) Element of bool [:NAT,(bool REAL):]
s is non empty V19() V22( NAT ) V23( bool REAL) Function-like V29( NAT ) V33( NAT , bool REAL) Element of bool [:NAT,(bool REAL):]
sa is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
t . sa is V144() V145() V146() Element of bool REAL
s . sa is V144() V145() V146() Element of bool REAL
((t . sa),(s . sa)) is V11() real ext-real set
p . sa is V144() V145() V146() Element of bool REAL
sb is non empty V144() V145() V146() compact closed_interval bounded_below bounded_above real-bounded interval Element of bool REAL
sb /\ r is V144() V145() V146() Element of bool REAL
sb /\ x is V144() V145() V146() Element of bool REAL
ga is non empty V144() V145() V146() compact Element of bool REAL
Nseq is non empty V144() V145() V146() compact Element of bool REAL
(ga,Nseq) is V11() real ext-real set
gb is V11() real ext-real set
fb is V11() real ext-real set
gb - fb is V11() real ext-real set
abs (gb - fb) is V11() real ext-real Element of REAL
Nseq1 is V11() real ext-real Element of REAL
fa is V11() real ext-real Element of REAL
Nseq1 - fa is V11() real ext-real Element of REAL
abs (Nseq1 - fa) is V11() real ext-real Element of REAL
sa is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
sb is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng sa is V144() V145() V146() Element of bool REAL
ga is set
dom sa is V144() V145() V146() V147() V148() V149() bounded_below Element of bool NAT
Nseq is set
sa . Nseq is V11() real ext-real Element of REAL
gb is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
sa . gb is V11() real ext-real Element of REAL
t . gb is V144() V145() V146() Element of bool REAL
p . gb is V144() V145() V146() Element of bool REAL
(p . gb) /\ r is V144() V145() V146() Element of bool REAL
ga is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ga is V11() real ext-real Element of REAL
Nseq is non empty V19() V22( NAT ) V23( NAT ) Function-like V29( NAT ) V33( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
sa * Nseq is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of sa
sb * Nseq is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of sb
rng (sb * Nseq) is V144() V145() V146() Element of bool REAL
fb is set
dom (sb * Nseq) is V144() V145() V146() V147() V148() V149() bounded_below Element of bool NAT
Nseq1 is set
(sb * Nseq) . Nseq1 is V11() real ext-real Element of REAL
fa is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
(sb * Nseq) . fa is V11() real ext-real Element of REAL
Nseq . fa is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
sb . (Nseq . fa) is V11() real ext-real Element of REAL
s . (Nseq . fa) is V144() V145() V146() Element of bool REAL
p . (Nseq . fa) is V144() V145() V146() Element of bool REAL
(p . (Nseq . fa)) /\ x is V144() V145() V146() Element of bool REAL
fb is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim fb is V11() real ext-real Element of REAL
Nseq1 is non empty V19() V22( NAT ) V23( NAT ) Function-like V29( NAT ) V33( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
(sb * Nseq) * Nseq1 is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of sb * Nseq
ga * Nseq1 is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of ga
lim (ga * Nseq1) is V11() real ext-real Element of REAL
(lim (ga * Nseq1)) + (lim fb) is V11() real ext-real Element of REAL
((lim (ga * Nseq1)) + (lim fb)) / 2 is V11() real ext-real Element of REAL
(r,x) is V11() real ext-real set
(ga * Nseq1) + fb is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
1 / 2 is V11() real ext-real non negative Element of REAL
(1 / 2) (#) ((ga * Nseq1) + fb) is non empty V19() V22( NAT ) V23( REAL ) Function-like V29( NAT ) V33( NAT , REAL ) complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(r,x) / 2 is V11() real ext-real Element of REAL
(1 / 2) * ((lim (ga * Nseq1)) + (lim fb)) is V11() real ext-real Element of REAL
lim ((ga * Nseq1) + fb) is V11() real ext-real Element of REAL
(1 / 2) * (lim ((ga * Nseq1) + fb)) is V11() real ext-real Element of REAL
lim ((1 / 2) (#) ((ga * Nseq1) + fb)) is V11() real ext-real Element of REAL
k0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
Nseq1 . k0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
Nseq . (Nseq1 . k0) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
t . (Nseq . (Nseq1 . k0)) is V144() V145() V146() Element of bool REAL
s . (Nseq . (Nseq1 . k0)) is V144() V145() V146() Element of bool REAL
((t . (Nseq . (Nseq1 . k0))),(s . (Nseq . (Nseq1 . k0)))) is V11() real ext-real set
sa . (Nseq . (Nseq1 . k0)) is V11() real ext-real Element of REAL
sb . (Nseq . (Nseq1 . k0)) is V11() real ext-real Element of REAL
(sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0))) is V11() real ext-real Element of REAL
((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2 is V11() real ext-real Element of REAL
(((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
2 * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
abs 2 is V11() real ext-real V62() Element of REAL
(abs 2) * (abs ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (2 * ((((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
2 * (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (((sa . (Nseq . (Nseq1 . k0))) + (sb . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
(ga * Nseq1) . k0 is V11() real ext-real Element of REAL
ga . (Nseq1 . k0) is V11() real ext-real Element of REAL
p . (Nseq . (Nseq1 . k0)) is V144() V145() V146() Element of bool REAL
(p . (Nseq . (Nseq1 . k0))) /\ x is V144() V145() V146() Element of bool REAL
(p . (Nseq . (Nseq1 . k0))) /\ r is V144() V145() V146() Element of bool REAL
((t . (Nseq . (Nseq1 . k0))),(s . (Nseq . (Nseq1 . k0)))) / 2 is V11() real ext-real Element of REAL
(((t . (Nseq . (Nseq1 . k0))),(s . (Nseq . (Nseq1 . k0)))) / 2) + ((r,x) / 2) is V11() real ext-real Element of REAL
(((t . (Nseq . (Nseq1 . k0))),(s . (Nseq . (Nseq1 . k0)))) / 2) + (((t . (Nseq . (Nseq1 . k0))),(s . (Nseq . (Nseq1 . k0)))) / 2) is V11() real ext-real Element of REAL
((1 / 2) (#) ((ga * Nseq1) + fb)) . k0 is V11() real ext-real Element of REAL
((ga * Nseq1) + fb) . k0 is V11() real ext-real Element of REAL
(1 / 2) * (((ga * Nseq1) + fb) . k0) is V11() real ext-real Element of REAL
(((ga * Nseq1) + fb) . k0) / 2 is V11() real ext-real Element of REAL
fb . k0 is V11() real ext-real Element of REAL
((ga * Nseq1) . k0) + (fb . k0) is V11() real ext-real Element of REAL
(((ga * Nseq1) . k0) + (fb . k0)) / 2 is V11() real ext-real Element of REAL
((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
(sb * Nseq) . (Nseq1 . k0) is V11() real ext-real Element of REAL
2 * ((r,x) / 2) is V11() real ext-real Element of REAL
(sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0))) is V11() real ext-real Element of REAL
abs ((sb . (Nseq . (Nseq1 . k0))) - (sa . (Nseq . (Nseq1 . k0)))) is V11() real ext-real Element of REAL
[.(sa . (Nseq . (Nseq1 . k0))),(sb . (Nseq . (Nseq1 . k0))).] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sa . (Nseq . (Nseq1 . k0)) <= b1 & b1 <= sb . (Nseq . (Nseq1 . k0)) ) } is set
j is V11() real ext-real Element of REAL
di is V11() real ext-real Element of REAL
[.j,di.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( j <= b1 & b1 <= di ) } is set
(sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0))) is V11() real ext-real Element of REAL
abs ((sa . (Nseq . (Nseq1 . k0))) - (sb . (Nseq . (Nseq1 . k0)))) is V11() real ext-real Element of REAL
(sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0))) is V11() real ext-real Element of REAL
((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (((sb . (Nseq . (Nseq1 . k0))) + (sa . (Nseq . (Nseq1 . k0)))) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
[.(sb . (Nseq . (Nseq1 . k0))),(sa . (Nseq . (Nseq1 . k0))).] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sb . (Nseq . (Nseq1 . k0)) <= b1 & b1 <= sa . (Nseq . (Nseq1 . k0)) ) } is set
j is V11() real ext-real Element of REAL
di is V11() real ext-real Element of REAL
[.j,di.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( j <= b1 & b1 <= di ) } is set
((ga * Nseq1) . k0) - (fb . k0) is V11() real ext-real Element of REAL
(((ga * Nseq1) . k0) - (fb . k0)) / 2 is V11() real ext-real Element of REAL
abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2) is V11() real ext-real Element of REAL
abs (((ga * Nseq1) . k0) - (fb . k0)) is V11() real ext-real Element of REAL
(abs (((ga * Nseq1) . k0) - (fb . k0))) / (abs 2) is V11() real ext-real Element of REAL
(abs (((ga * Nseq1) . k0) - (fb . k0))) / 2 is V11() real ext-real Element of REAL
((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
((((ga * Nseq1) . k0) - (fb . k0)) / 2) + (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (((ga * Nseq1) . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
(abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + (abs (((((ga * Nseq1) . k0) + (fb . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
(abs ((((ga * Nseq1) . k0) - (fb . k0)) / 2)) + ((r,x) / 2) is V11() real ext-real Element of REAL
((abs (((ga * Nseq1) . k0) - (fb . k0))) / 2) + ((r,x) / 2) is V11() real ext-real Element of REAL
(fb . k0) - ((ga * Nseq1) . k0) is V11() real ext-real Element of REAL
((fb . k0) - ((ga * Nseq1) . k0)) / 2 is V11() real ext-real Element of REAL
abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2) is V11() real ext-real Element of REAL
abs ((fb . k0) - ((ga * Nseq1) . k0)) is V11() real ext-real Element of REAL
(abs ((fb . k0) - ((ga * Nseq1) . k0))) / (abs 2) is V11() real ext-real Element of REAL
(abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2 is V11() real ext-real Element of REAL
(fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
(fb . k0) + ((ga * Nseq1) . k0) is V11() real ext-real Element of REAL
((fb . k0) + ((ga * Nseq1) . k0)) / 2 is V11() real ext-real Element of REAL
(((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
(((fb . k0) - ((ga * Nseq1) . k0)) / 2) + ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs ((fb . k0) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
(abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + (abs ((((fb . k0) + ((ga * Nseq1) . k0)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
((ga * Nseq1) . k0) - (fb . k0) is V11() real ext-real Element of REAL
abs (((ga * Nseq1) . k0) - (fb . k0)) is V11() real ext-real Element of REAL
(abs (((fb . k0) - ((ga * Nseq1) . k0)) / 2)) + ((r,x) / 2) is V11() real ext-real Element of REAL
((abs ((fb . k0) - ((ga * Nseq1) . k0))) / 2) + ((r,x) / 2) is V11() real ext-real Element of REAL
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
max (k0,i) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
Nseq1 . (max (k0,i)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
Nseq . (Nseq1 . (max (k0,i))) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
j is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
P . j is V144() V145() V146() Element of bool REAL
fb . (max (k0,i)) is V11() real ext-real Element of REAL
(sb * Nseq) . (Nseq1 . (max (k0,i))) is V11() real ext-real Element of REAL
sb . j is V11() real ext-real Element of REAL
s . j is V144() V145() V146() Element of bool REAL
p . j is V144() V145() V146() Element of bool REAL
(p . j) /\ x is V144() V145() V146() Element of bool REAL
dom Nseq is V144() V145() V146() V147() V148() V149() bounded_below Element of bool NAT
(p . j) /\ r is V144() V145() V146() Element of bool REAL
t . j is V144() V145() V146() Element of bool REAL
Nseq . i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
((1 / 2) (#) ((ga * Nseq1) + fb)) . (max (k0,i)) is V11() real ext-real Element of REAL
((ga * Nseq1) + fb) . (max (k0,i)) is V11() real ext-real Element of REAL
(1 / 2) * (((ga * Nseq1) + fb) . (max (k0,i))) is V11() real ext-real Element of REAL
(((ga * Nseq1) + fb) . (max (k0,i))) / 2 is V11() real ext-real Element of REAL
(ga * Nseq1) . (max (k0,i)) is V11() real ext-real Element of REAL
((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i))) is V11() real ext-real Element of REAL
(((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2 is V11() real ext-real Element of REAL
((((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
abs (((((ga * Nseq1) . (max (k0,i))) + (fb . (max (k0,i)))) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
ga . (Nseq1 . (max (k0,i))) is V11() real ext-real Element of REAL
sa . j is V11() real ext-real Element of REAL
(sa . j) + (sb . j) is V11() real ext-real Element of REAL
((sa . j) + (sb . j)) / 2 is V11() real ext-real Element of REAL
(((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2) is V11() real ext-real Element of REAL
abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
2 * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
dom Nseq1 is V144() V145() V146() V147() V148() V149() bounded_below Element of bool NAT
Nseq1 . i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
Nseq . (Nseq1 . i) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V61() V62() V144() V145() V146() V147() V148() V149() bounded_below Element of NAT
((t . j),(s . j)) is V11() real ext-real set
(abs 2) * (abs ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (2 * ((((sa . j) + (sb . j)) / 2) - (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (((sa . j) + (sb . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
(sb . j) - (sa . j) is V11() real ext-real Element of REAL
abs ((sb . j) - (sa . j)) is V11() real ext-real Element of REAL
[.(sa . j),(sb . j).] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sa . j <= b1 & b1 <= sb . j ) } is set
c25 is V11() real ext-real Element of REAL
c26 is V11() real ext-real Element of REAL
[.c25,c26.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( c25 <= b1 & b1 <= c26 ) } is set
(sa . j) - (sb . j) is V11() real ext-real Element of REAL
abs ((sa . j) - (sb . j)) is V11() real ext-real Element of REAL
(sb . j) + (sa . j) is V11() real ext-real Element of REAL
((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2)) is V11() real ext-real Element of REAL
abs (((sb . j) + (sa . j)) - (2 * (((lim (ga * Nseq1)) + (lim fb)) / 2))) is V11() real ext-real Element of REAL
[.(sb . j),(sa . j).] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( sb . j <= b1 & b1 <= sa . j ) } is set
c25 is V11() real ext-real Element of REAL
c26 is V11() real ext-real Element of REAL
[.c25,c26.] is V144() V145() V146() compact interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( c25 <= b1 & b1 <= c26 ) } is set
S is closed Element of bool the carrier of (TOP-REAL 2)
proj2 .: S is V144() V145() V146() Element of bool REAL
Cl (proj2 .: S) is V144() V145() V146() closed Element of bool REAL
Cl S is Element of bool the carrier of (TOP-REAL 2)
proj2 .: (Cl S) is V144() V145() V146() Element of bool REAL
S is Element of bool the carrier of (TOP-REAL 2)
proj2 .: S is V144() V145() V146() Element of bool REAL
bool the carrier of (Euclid 2) is non empty set
C is bounded Element of bool the carrier of (Euclid 2)
r is V11() real ext-real Element of REAL
x is Element of the carrier of (Euclid 2)
Ball (x,r) is Element of bool the carrier of (Euclid 2)
p is V43(2) V65() real-valued Element of the carrier of (TOP-REAL 2)
p `2 is V11() real ext-real Element of REAL
(p `2) - r is V11() real ext-real Element of REAL
abs ((p `2) - r) is V11() real ext-real Element of REAL
(p `2) + r is V11() real ext-real Element of REAL
abs ((p `2) + r) is V11() real ext-real Element of REAL
max ((abs ((p `2) - r)),(abs ((p `2) + r))) is V11() real ext-real set
r - (p `2) is V11() real ext-real Element of REAL
abs (r - (p `2)) is V11() real ext-real Element of REAL
P is Element of bool the carrier of (TOP-REAL 2)
proj2 .: P is V144() V145() V146() Element of bool REAL
].((p `2) - r),((p `2) + r).[ is V144() V145() V146() non left_end non right_end interval Element of bool REAL
{ b1 where b1 is V11() real ext-real Element of REAL : ( not b1 <= (p `2) - r & not (p `2) + r <= b1 ) } is set
s is V11() real ext-real set
abs s is V11() real ext-real Element of REAL
S is closed compact bounded Element of bool the carrier of (TOP-REAL 2)
proj2 .: S is V144() V145() V146() Element of bool REAL