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,