:: JORDAN13 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

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

RAT is set

INT is set

K6(K7(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like V110() V156() V157() V158() V159() V160() V161() V162() strict add-continuous Mult-continuous 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

C is non empty connected bounded V189( TOP-REAL 2) non horizontal non vertical being_simple_closed_curve 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

Gauge (C,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) *

X-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Y-SpanStart (C,n) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(X-SpanStart (C,n)) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

len (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

2 |^ n is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(2 |^ n) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

<*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n))))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((X-SpanStart (C,n)),(Y-SpanStart (C,n)))),((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(Y-SpanStart (C,n))))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (1,1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (1,1))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

the topology of (TOP-REAL 2) is Element of K6(K6( the carrier of (TOP-REAL 2)))

K6(K6( the carrier of (TOP-REAL 2))) is set

TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) is strict TopStruct

TopSpaceMetr (Euclid 2) is TopStruct

[(X-SpanStart (C,n)),(Y-SpanStart (C,n))] is set

{(X-SpanStart (C,n)),(Y-SpanStart (C,n))} is V26() set

{(X-SpanStart (C,n))} is V26() set

{{(X-SpanStart (C,n)),(Y-SpanStart (C,n))},{(X-SpanStart (C,n))}} is V26() V30() set

Indices (Gauge (C,n)) is set

width (Gauge (C,n)) is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

F is set

k 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 k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len k) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

k ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

k 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 k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len k) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

k ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

k 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 k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len k) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

((len k) -' 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

((len k) -' 1) + (1 + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

(len k) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

dom k is V26() Element of K6(NAT)

k /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

k /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

k is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[k,m] is set

{k,m} is V26() set

{k} is V26() set

{{k,m},{k}} is V26() V30() set

(Gauge (C,n)) * (k,m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f 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

[f,f] is set

{f,f} is V26() set

{f} is V26() set

{{f,f},{f}} is V26() V30() set

(Gauge (C,n)) * (f,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

f -' 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

front_right_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

(Gauge (C,n)) * ((f -' 1),f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((f -' 1),f))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * ((f -' 1),f))*> is non empty 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)

g is non empty 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)

1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

cell ((Gauge (C,n)),(1 -' 1),m) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),m) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(1 -' 1))) /\ (h_strip ((Gauge (C,n)),m)) is Element of K6( the carrier of (TOP-REAL 2))

cell ((Gauge (C,n)),0,m) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),0)) /\ (h_strip ((Gauge (C,n)),m)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() 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

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() 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

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * (f,(f + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (f,(f + 1)))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (f,(f + 1)))*> is non empty 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)

g is non empty 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 (Gauge (C,n))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

cell ((Gauge (C,n)),k,(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),k) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),k)) /\ (h_strip ((Gauge (C,n)),(len (Gauge (C,n))))) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() 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

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() 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

g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * (f,(f -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (f,(f -' 1)))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (f,(f -' 1)))*> is non empty 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)

g is non empty 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)

1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

cell ((Gauge (C,n)),f,(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),f) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),f)) /\ (h_strip ((Gauge (C,n)),(1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))

cell ((Gauge (C,n)),f,0) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),f)) /\ (h_strip ((Gauge (C,n)),0)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() 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

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() 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

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * ((f + 1),f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((f + 1),f))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * ((f + 1),f))*> is non empty 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)

g is non empty 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 (Gauge (C,n))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

cell ((Gauge (C,n)),(len (Gauge (C,n))),f) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),f) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(len (Gauge (C,n))))) /\ (h_strip ((Gauge (C,n)),f)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() 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

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g 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

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

front_right_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

(Gauge (C,n)) * (f,(f + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (f,(f + 1)))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (f,(f + 1)))*> is non empty 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)

g is non empty 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 (Gauge (C,n))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

k -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

cell ((Gauge (C,n)),(k -' 1),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(k -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(k -' 1))) /\ (h_strip ((Gauge (C,n)),(len (Gauge (C,n))))) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() 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

g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * ((f + 1),f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((f + 1),f))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * ((f + 1),f))*> is non empty 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)

g is non empty 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 (Gauge (C,n))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

cell ((Gauge (C,n)),(len (Gauge (C,n))),m) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),m) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(len (Gauge (C,n))))) /\ (h_strip ((Gauge (C,n)),m)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g 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

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * ((f -' 1),f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((f -' 1),f))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * ((f -' 1),f))*> is non empty 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)

g is non empty 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)

1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

cell ((Gauge (C,n)),(1 -' 1),(m -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),(m -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(1 -' 1))) /\ (h_strip ((Gauge (C,n)),(m -' 1))) is Element of K6( the carrier of (TOP-REAL 2))

cell ((Gauge (C,n)),0,(m -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),0)) /\ (h_strip ((Gauge (C,n)),(m -' 1))) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() 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

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

(Gauge (C,n)) * (f,(f -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (f,(f -' 1)))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (f,(f -' 1)))*> is non empty 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)

g is non empty 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)

1 -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

cell ((Gauge (C,n)),k,(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),k) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),(1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),k)) /\ (h_strip ((Gauge (C,n)),(1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))

cell ((Gauge (C,n)),k,0) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),0) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),k)) /\ (h_strip ((Gauge (C,n)),0)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive 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

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() 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

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,g))*> is non empty 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)

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)

len g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(len g) -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_right_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

front_left_cell (g,((len g) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

g ^ <*((Gauge (C,n)) * (1,1))*> is non empty 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)

g is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

Lg9 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

(Gauge (C,n)) * (g,Lg9) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,Lg9))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * (g,Lg9))*> is non empty 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)

front_right_cell (k,((len k) -' 1),(Gauge (C,n))) is Element of K6( the carrier of (TOP-REAL 2))

(Gauge (C,n)) * ((f + 1),f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * ((f + 1),f))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,n)) * ((f + 1),f))*> is non empty 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)

g is non empty 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 (Gauge (C,n))) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

cell ((Gauge (C,n)),(len (Gauge (C,n))),f) is Element of K6( the carrier of (TOP-REAL 2))

v_strip ((Gauge (C,n)),(len (Gauge (C,n)))) is Element of K6( the carrier of (TOP-REAL 2))

h_strip ((Gauge (C,n)),f) is Element of K6( the carrier of (TOP-REAL 2))

(v_strip ((Gauge (C,n)),(len (Gauge (C,n))))) /\ (h_strip ((Gauge (C,n)),f)) is Element of K6( the carrier of (TOP-REAL 2))

Lg9 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

[Lg9,f] is set

{Lg9,f} is V26() set

{Lg9} is V26() set

{{Lg9,f},{Lg9}} is V26() V30() set

f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,m] is set

{f,m} is V26() set

{f} is V26() set

{{f,m},{f}} is V26() V30() set

g /. ((len k) -' 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (Lg9,f) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g /. (((len k) -' 1) + 1) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * (f,m) is 2 -element FinSequence-like V136() 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

f + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[(f + 1),m] is set

{(f + 1),m} is V26() set

{(f + 1)} is V26() set

{{(f + 1),m},{(f + 1)}} is V26() V30() set

((len k) -' 1) + 2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

g /. (((len k) -' 1) + 2) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

(Gauge (C,n)) * ((f + 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

Lg9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

m -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[f,(m -' 1)] is set

{f,(m -' 1)} is V26() set

{{f,(m -' 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m -' 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative Element of NAT

[f,(m + 1)] is set

{f,(m + 1)} is V26() set

{{f,(m + 1)},{f}} is V26() V30() set

(Gauge (C,n)) * (f,(m + 1)) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

f -' 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative Element of NAT

[(f -' 1),m] is set

{(f -' 1),m} is V26() set

{(f -' 1)} is V26() set

{{(f -' 1),m},{(f -' 1)}} is V26() V30() set

(Gauge (C,n)) * ((f -' 1),m) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

g 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

(Gauge (C,n)) * (g,g) is 2 -element FinSequence-like V136() Element of the carrier of (TOP-REAL 2)

<*((Gauge (C,n)) * (g,g))*> is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V26() 1 -element FinSequence-like FinSubsequence-like special FinSequence of the carrier of (TOP-REAL 2)

k ^ <*((Gauge (C,