REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K6(REAL)
K6(REAL) is set
omega is non empty epsilon-transitive epsilon-connected ordinal set
K6(omega) is set
K6(NAT) is set
COMPLEX is set
RAT is set
INT is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
K7(1,1) is Relation-like set
K6(K7(1,1)) is set
K7(K7(1,1),1) is Relation-like set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is Relation-like set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is Relation-like set
K7(K7(REAL,REAL),REAL) is Relation-like set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
K7(2,2) is Relation-like set
K7(K7(2,2),REAL) is Relation-like set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V118() V143() V144() V145() V146() V147() V148() V149() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K7( the carrier of (TOP-REAL 2),REAL) is Relation-like set
K6(K7( the carrier of (TOP-REAL 2),REAL)) is set
K6( the carrier of (TOP-REAL 2)) is set
the carrier of (TOP-REAL 2) * is non empty functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V26() V27() V30() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V26() V27() V30() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
the carrier of (Euclid 2) is non empty set
card {} is cardinal set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(n -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
n + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
(n + 2) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(n + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
((n + 1) + 1) - 1 is V11() real ext-real Element of REAL
n is non empty TopSpace-like TopStruct
the carrier of n is non empty set
K6( the carrier of n) is set
C is Element of K6( the carrier of n)
f is Element of K6( the carrier of n)
f is Element of K6( the carrier of n)
G is Element of K6( the carrier of n)
n is non empty set
C is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
f is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f | (len f) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
C | (len f) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
C | (len C) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
f | (len C) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
C | (len C) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
f | (len f) is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is non empty set
f is Relation-like NAT -defined C -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
dom f is V26() Element of K6(NAT)
Rev f is Relation-like NAT -defined C -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
dom (Rev f) is V26() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f /. n is Element of C
((len f) + 1) -' n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(Rev f) /. G is Element of C
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(G + 1) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(G + n) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is non empty set
f is Relation-like NAT -defined C -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
Rev f is Relation-like NAT -defined C -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of C
dom (Rev f) is V26() Element of K6(NAT)
dom f is V26() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
(Rev f) /. n is Element of C
f /. n is Element of C
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(Rev f) /. G is Element of C
f /. G is Element of C
n is non empty set
n * is non empty functional FinSequence-membered M11(n)
C is Relation-like NAT -defined n * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of n *
f is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
Rev f is Relation-like NAT -defined n -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of n
dom (Rev f) is V26() Element of K6(NAT)
Indices C is set
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
(Rev f) /. G is Element of n
(Rev f) /. (G + 1) is Element of n
dom f is V26() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. f is Element of n
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[S,N] is set
{S,N} is V26() set
{S} is V26() set
{{S,N},{S}} is V26() V30() set
C * (W,E) is Element of n
C * (S,N) is Element of n
W - S is V11() real ext-real set
abs (W - S) is V11() real ext-real Element of REAL
E - N is V11() real ext-real set
abs (E - N) is V11() real ext-real Element of REAL
(abs (W - S)) + (abs (E - N)) is V11() real ext-real Element of REAL
S - W is V11() real ext-real set
abs (S - W) is V11() real ext-real Element of REAL
N - E is V11() real ext-real set
abs (N - E) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(G + 1) + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f /. k is Element of n
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + (1 + k) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(Rev f) /. G is Element of n
dom f is V26() Element of K6(NAT)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. f is Element of n
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is Element of n
dom f is V26() Element of K6(NAT)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f /. G is Element of n
f /. (G + 1) is Element of n
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(Rev f) /. f is Element of n
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[S,N] is set
{S,N} is V26() set
{S} is V26() set
{{S,N},{S}} is V26() V30() set
C * (W,E) is Element of n
C * (S,N) is Element of n
W - S is V11() real ext-real set
abs (W - S) is V11() real ext-real Element of REAL
E - N is V11() real ext-real set
abs (E - N) is V11() real ext-real Element of REAL
(abs (W - S)) + (abs (E - N)) is V11() real ext-real Element of REAL
S - W is V11() real ext-real set
abs (S - W) is V11() real ext-real Element of REAL
N - E is V11() real ext-real set
abs (N - E) is V11() real ext-real Element of REAL
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(G + 1) + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
(Rev f) /. k is Element of n
1 + k is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + (1 + k) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. G is Element of n
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(len f) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(Rev f) /. f is Element of n
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is Element of n
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of (TOP-REAL 2) *
Values C is V26() set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
dom f is V26() Element of K6(NAT)
f . n is set
rng f is V26() set
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
Indices C is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
dom f is V26() Element of K6(NAT)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C /^ n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (C /^ n) is closed compact Element of K6( the carrier of (TOP-REAL 2))
f is set
len (C /^ n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
LSeg ((C /^ n),G) is closed Element of K6( the carrier of (TOP-REAL 2))
(len C) - n is V11() real ext-real Element of REAL
n + (G + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
n + G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(n + G) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
LSeg (C,(n + G)) is closed Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
left_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,n) is closed Element of K6( the carrier of (TOP-REAL 2))
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
LSeg ((f /. n),(f /. (n + 1))) is closed compact Element of K6( the carrier of (TOP-REAL 2))
(left_cell (f,n,C)) /\ (right_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
left_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
W + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,W) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
left_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
W + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,W) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
left_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
Cl (Int (left_cell (f,n,C))) is Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
Cl (Int (right_cell (f,n,C))) is Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
W + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,W) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg (f,n) is closed Element of K6( the carrier of (TOP-REAL 2))
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
C * (1,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(C * (1,f)) `2 is V11() real ext-real Element of REAL
W is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W `2 is V11() real ext-real Element of REAL
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(f /. n) `2 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C * (1,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(C * (1,1)) `2 is V11() real ext-real Element of REAL
G is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G `2 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
LSeg (f,n) is closed Element of K6( the carrier of (TOP-REAL 2))
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
C * (G,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(C * (G,1)) `1 is V11() real ext-real Element of REAL
W is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W `1 is V11() real ext-real Element of REAL
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
(f /. n) `1 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C * (1,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(C * (1,1)) `1 is V11() real ext-real Element of REAL
G is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G `1 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (f,n) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (f,C) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
G is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ G is closed compact Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (f,n)) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (f,n))) /\ (Int (h_strip (f,C))) is Element of K6( the carrier of (TOP-REAL 2))
f is set
len G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
{ (LSeg (G,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : ( 1 <= b1 & b1 + 1 <= len G ) } is set
union { (LSeg (G,b1)) where b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : ( 1 <= b1 & b1 + 1 <= len G ) } is set
W is set
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
LSeg (G,E) is closed Element of K6( the carrier of (TOP-REAL 2))
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f * (1,N) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,N)) `2 is V11() real ext-real Element of REAL
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
S is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,C)) `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f * (N,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (N,1)) `1 is V11() real ext-real Element of REAL
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
S is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,1)) `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
S `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
left_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
L~ f is closed compact Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,n,C)) is Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
W + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),f) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(f -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,(f -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,f) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,f)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,W) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,W,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,(E -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,W)) /\ (h_strip (C,(E -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,(G -' 1),E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,(G -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,E) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,(G -' 1))) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
cell (C,G,E) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,G) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,G)) /\ (h_strip (C,E)) is Element of K6( the carrier of (TOP-REAL 2))
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,(C + 1))) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),(C + 1))) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,1)) `1 is V11() real ext-real Element of REAL
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,C)) `2 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL
n is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
C `1 is V11() real ext-real Element of REAL
C `2 is V11() real ext-real Element of REAL
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
cell (n,f,G) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (n,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (n,G) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (n,f)) /\ (h_strip (n,G)) is Element of K6( the carrier of (TOP-REAL 2))
n * (f,G) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(n * (f,G)) `1 is V11() real ext-real Element of REAL
n * ((f + 1),G) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(n * ((f + 1),G)) `1 is V11() real ext-real Element of REAL
(n * (f,G)) `2 is V11() real ext-real Element of REAL
n * (f,(G + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(n * (f,(G + 1))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (n * (f,G)) `2 <= b2 & b2 <= (n * (f,(G + 1))) `2 ) } is set
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (n * (f,G)) `1 <= b1 & b1 <= (n * ((f + 1),G)) `1 ) } is set
f is V11() real ext-real Element of REAL
W is V11() real ext-real Element of REAL
|[f,W]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of (TOP-REAL 2)
f is V11() real ext-real Element of REAL
W is V11() real ext-real Element of REAL
|[f,W]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of (TOP-REAL 2)
|[(C `1),(C `2)]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of (TOP-REAL 2)
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (f,n) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (f,C) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V11() real ext-real Element of REAL : ( (f * (n,C)) `1 <= b1 & b1 <= (f * ((n + 1),C)) `1 & (f * (n,C)) `2 <= b2 & b2 <= (f * (n,(C + 1))) `2 ) } is set
f is set
W is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W `2 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
|[(W `1),(W `2)]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of (TOP-REAL 2)
f is set
W is V11() real ext-real Element of REAL
E is V11() real ext-real Element of REAL
|[W,E]| is non empty Relation-like NAT -defined Function-like V26() 2 -element FinSequence-like FinSubsequence-like V86() Element of the carrier of (TOP-REAL 2)
S is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
S `1 is V11() real ext-real Element of REAL
S `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Values f is V26() set
cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (f,n) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (f,C) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
Indices f is set
{ (f * (b1,b2)) where b1, b2 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT : [b1,b2] in Indices f } is set
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f * (f,W) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
[f,W] is set
{f,W} is V26() set
{f} is V26() set
{{f,W},{f}} is V26() V30() set
f * (f,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (f,C)) `2 is V11() real ext-real Element of REAL
(f * (f,W)) `2 is V11() real ext-real Element of REAL
f * (1,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,C)) `2 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
(f * (f,W)) `2 is V11() real ext-real Element of REAL
f * (f,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (f,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (1,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (1,(C + 1))) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
f * (n,W) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,W)) `1 is V11() real ext-real Element of REAL
(f * (f,W)) `1 is V11() real ext-real Element of REAL
f * (n,1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,1)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `1 is V11() real ext-real Element of REAL
(f * (f,W)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),W) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),W)) `1 is V11() real ext-real Element of REAL
f * ((n + 1),1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),1)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (f,n) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (f,C) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,C)) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
(f * (n,C)) `2 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `1 is V11() real ext-real Element of REAL
(f * (n,(C + 1))) `1 is V11() real ext-real Element of REAL
(f * ((n + 1),(C + 1))) `2 is V11() real ext-real Element of REAL
(f * ((n + 1),C)) `2 is V11() real ext-real Element of REAL
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
C + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
Values f is V26() set
cell (f,n,C) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (f,n) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (f,C) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (f,n)) /\ (h_strip (f,C)) is Element of K6( the carrier of (TOP-REAL 2))
G is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
LSeg (f,W) is closed compact Element of K6( the carrier of (TOP-REAL 2))
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W `2 is V11() real ext-real Element of REAL
G `2 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,C)) `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G `1 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * ((n + 1),C)) `1 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
G `2 is V11() real ext-real Element of REAL
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,(C + 1))) `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G `2 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
(f * (n,C)) `2 is V11() real ext-real Element of REAL
W `2 is V11() real ext-real Element of REAL
f `1 is V11() real ext-real Element of REAL
G `1 is V11() real ext-real Element of REAL
W `1 is V11() real ext-real Element of REAL
f `2 is V11() real ext-real Element of REAL
f * (n,C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * (n,(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),(C + 1)) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f * ((n + 1),C) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
n + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of the carrier of (TOP-REAL 2) *
len C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
width C is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
LSeg (f,n) is closed Element of K6( the carrier of (TOP-REAL 2))
Indices C is set
f /. n is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f /. (n + 1) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
G is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[G,f] is set
{G,f} is V26() set
{G} is V26() set
{{G,f},{G}} is V26() V30() set
C * (G,f) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
W is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
[W,E] is set
{W,E} is V26() set
{W} is V26() set
{{W,E},{W}} is V26() V30() set
C * (W,E) is 2 -element FinSequence-like V86() Element of the carrier of (TOP-REAL 2)
f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
G + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
W + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
LSeg ((f /. n),(f /. (n + 1))) is closed compact Element of K6( the carrier of (TOP-REAL 2))
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,S,N) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,S) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,N) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,S)) /\ (h_strip (C,N)) is Element of K6( the carrier of (TOP-REAL 2))
G -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
2 - 1 is V11() real ext-real Element of REAL
2 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
cell (C,S,N) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,S) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,N) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,S)) /\ (h_strip (C,N)) is Element of K6( the carrier of (TOP-REAL 2))
k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
k + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
i is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT
i + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT
cell (C,k,i) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (C,k) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (C,i) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (C,k)) /\ (h_strip (C,i)) is Element of K6( the carrier of (TOP-REAL 2))
N is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of