:: JORDAN9 semantic presentation

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,b

union { (LSeg (G,b

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

{ |[b

{ |[b

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

{ |[b

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 * (b

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