REAL is non empty non trivial non finite non empty-membered V69() V70() V71() V75() set
NAT is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
COMPLEX is non empty non trivial non finite non empty-membered V69() V75() set
omega is non empty non trivial ordinal non finite cardinal limit_cardinal non empty-membered V69() V70() V71() V72() V73() V74() V75() set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
RAT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V75() set
INT is non empty non trivial non finite non empty-membered V69() V70() V71() V72() V73() V75() set
[:REAL,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set
{} is set
the empty ordinal natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Function-yielding V81() FinSequence-yielding finite-support set is empty ordinal natural V11() real Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional integer finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V59() V60() V61() V62() V69() V70() V71() V72() V73() V74() V75() Function-yielding V81() FinSequence-yielding finite-support set
1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
{{},1} is finite set
K386() is set
bool K386() is set
K387() is Element of bool K386()
[:1,1:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set
bool [:1,1:] is finite V32() set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set
bool [:[:1,1:],1:] is finite V32() set
[:[:1,1:],REAL:] is Relation-like V59() V60() V61() set
bool [:[:1,1:],REAL:] is set
[:[:REAL,REAL:],REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite non empty-membered set
2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[:2,2:] is Relation-like RAT -valued INT -valued finite V59() V60() V61() V62() set
[:[:2,2:],REAL:] is Relation-like V59() V60() V61() set
bool [:[:2,2:],REAL:] is set
TOP-REAL 2 is non empty non trivial TopSpace-like T_2 V156() V181() V182() V183() V184() V185() V186() V187() strict add-continuous Mult-continuous RLTopStruct
the carrier of (TOP-REAL 2) is non empty non trivial functional non empty-membered set
the carrier of (TOP-REAL 2) * is non empty functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
[: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [: the carrier of (TOP-REAL 2),REAL:] is non empty non trivial non finite non empty-membered set
bool the carrier of (TOP-REAL 2) is set
[:COMPLEX,COMPLEX:] is non empty non trivial Relation-like non finite non empty-membered V59() set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite non empty-membered set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial Relation-like non finite non empty-membered V59() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite non empty-membered set
[:RAT,RAT:] is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set
bool [:RAT,RAT:] is non empty non trivial non finite non empty-membered set
[:[:RAT,RAT:],RAT:] is non empty non trivial Relation-like RAT -valued non finite non empty-membered V59() V60() V61() set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite non empty-membered set
[:INT,INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set
bool [:INT,INT:] is non empty non trivial non finite non empty-membered set
[:[:INT,INT:],INT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite non empty-membered set
[:NAT,NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set
[:[:NAT,NAT:],NAT:] is non empty non trivial Relation-like RAT -valued INT -valued non finite non empty-membered V59() V60() V61() V62() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite non empty-membered set
[:COMPLEX,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:COMPLEX,REAL:] is non empty non trivial non finite non empty-membered set
K567() is Relation-like NAT -defined Function-like total set
3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
4 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V43( the carrier of (TOP-REAL 2), REAL ) V59() V60() V61() Element of bool [: the carrier of (TOP-REAL 2),REAL:]
proj2 is Relation-like the carrier of (TOP-REAL 2) -defined REAL -valued Function-like V43( the carrier of (TOP-REAL 2), REAL ) V59() V60() V61() Element of bool [: the carrier of (TOP-REAL 2),REAL:]
dom {} is set
rng {} is set
C is non empty non empty-membered set
C * is non empty functional FinSequence-membered FinSequenceSet of C
n is non empty set
<*n*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like finite-support set
<*<*n*>*> is non empty trivial Relation-like NAT -defined Function-like constant finite 1 -element FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support set
rng <*<*n*>*> is non empty trivial finite 1 -element set
{<*n*>} is non empty trivial functional finite V32() 1 -element with_non-empty_elements non empty-membered set
G is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *
rng G is functional finite FinSequence-membered Element of bool (C *)
bool (C *) is set
C is Relation-like non-empty Function-like Function-yielding V81() set
rngs C is Relation-like Function-like set
n is set
dom (rngs C) is set
dom C is set
(rngs C) . n is set
C . n is Relation-like Function-like set
rng (C . n) is set
C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
LSeg (C,n) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C) + (b1 * n)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{C,n} is functional finite V32() set
(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of (TOP-REAL 2)
Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of (TOP-REAL 2)
Euclid 2 is non empty strict Reflexive discerning symmetric triangle MetrStruct
REAL 2 is non empty functional FinSequence-membered FinSequenceSet of REAL
2 -tuples_on REAL is functional FinSequence-membered FinSequenceSet of REAL
Pitag_dist 2 is Relation-like [:(REAL 2),(REAL 2):] -defined REAL -valued Function-like V43([:(REAL 2),(REAL 2):], REAL ) V59() V60() V61() Element of bool [:[:(REAL 2),(REAL 2):],REAL:]
[:(REAL 2),(REAL 2):] is Relation-like set
[:[:(REAL 2),(REAL 2):],REAL:] is Relation-like V59() V60() V61() set
bool [:[:(REAL 2),(REAL 2):],REAL:] is set
MetrStruct(# (REAL 2),(Pitag_dist 2) #) is strict MetrStruct
the carrier of (Euclid 2) is non empty set
i1 is functional Element of bool the carrier of (TOP-REAL 2)
the topology of (TOP-REAL 2) is Element of bool (bool the carrier of (TOP-REAL 2))
bool (bool 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
the carrier of (TopSpaceMetr (Euclid 2)) is set
bool the carrier of (TopSpaceMetr (Euclid 2)) is set
j2 is Element of bool the carrier of (TopSpaceMetr (Euclid 2))
G is Element of the carrier of (Euclid 2)
j2 is V11() real ext-real set
Ball (G,j2) is Element of bool the carrier of (Euclid 2)
bool the carrier of (Euclid 2) is set
j4 is V11() real ext-real Element of REAL
j4 / 2 is V11() real ext-real Element of REAL
f is Element of the carrier of (Euclid 2)
dist (G,f) is V11() real ext-real Element of REAL
(dist (G,f)) / 2 is V11() real ext-real Element of REAL
min ((j4 / 2),((dist (G,f)) / 2)) is V11() real ext-real set
(min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)) is V11() real ext-real Element of REAL
1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
i0 is Element of the carrier of (Euclid 2)
j0 is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2
n is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2
j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
j - i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K268(i1) is Relation-like Function-like V59() set
K38(1) is V11() real integer ext-real non positive set
K38(1) * i1 is Relation-like Function-like set
K239(j,K268(i1)) is Relation-like Function-like set
dist (G,i0) is V11() real ext-real Element of REAL
i is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2
j0 - i is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2
K268(i) is Relation-like Function-like V59() set
K38(1) * i is Relation-like Function-like set
K239(j0,K268(i)) is Relation-like Function-like set
|.(j0 - i).| is V11() real ext-real non negative Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) is Relation-like Function-like V59() set
K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like Function-like set
K239(j,K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)) is Relation-like Function-like V59() set
K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like Function-like set
K239((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.((j - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
1 * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239((1 * j),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j))) is Relation-like Function-like set
((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 * j) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL
((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 * j) + (((- 1) * (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) * j)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) is V11() real ext-real Element of REAL
1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))))) is V11() real ext-real Element of REAL
(1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
K239(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1))) is Relation-like Function-like set
|.(((1 + (- (1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))))) * j) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * i1)).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((- 1) * ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * i1)).| is V11() real ext-real non negative Element of REAL
(- 1) * i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * j) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL
j + ((- 1) * i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + ((- 1) * i1))).| is V11() real ext-real non negative Element of REAL
- i1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
j + (- i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j + (- i1))).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of 2 -tuples_on REAL
|.(((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (j - i1)).| is V11() real ext-real non negative Element of REAL
abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
j1 is Relation-like NAT -defined REAL -valued Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of REAL 2
|.j1.| is V11() real ext-real non negative Element of REAL
(abs ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * |.j1.| is V11() real ext-real Element of REAL
|.(j - i1).| is V11() real ext-real non negative Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * |.(j - i1).| is V11() real ext-real Element of REAL
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * (dist (G,f)) is V11() real ext-real Element of REAL
j4 / 1 is V11() real ext-real Element of REAL
Ball (G,j4) is Element of bool the carrier of (Euclid 2)
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) is V11() real ext-real Element of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(dist (G,f)) / 1 is V11() real ext-real Element of REAL
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) + ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) is Relation-like Function-like V59() set
K38(1) * (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n) is Relation-like Function-like set
K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268((((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n))) is Relation-like Function-like set
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)) - ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C)) is Relation-like Function-like V59() set
K38(1) * ((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) is Relation-like Function-like set
K239((((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C) + (((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f))) * n)),K268(((1 - ((min ((j4 / 2),((dist (G,f)) / 2))) / (dist (G,f)))) * C))) is Relation-like Function-like set
C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
LSeg (C,n) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * C) + (b1 * n)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{C,n} is functional finite V32() set
(LSeg (C,n)) \ {C,n} is functional Element of bool the carrier of (TOP-REAL 2)
Cl ((LSeg (C,n)) \ {C,n}) is functional Element of bool the carrier of (TOP-REAL 2)
Cl (LSeg (C,n)) is functional connected bounded convex Element of bool the carrier of (TOP-REAL 2)
G is set
((LSeg (C,n)) \ {C,n}) \/ {C,n} is set
C is functional Element of bool the carrier of (TOP-REAL 2)
Cl C is functional Element of bool the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
LSeg (n,G) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * n) + (b1 * G)) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{n,G} is functional finite V32() set
(LSeg (n,G)) \ {n,G} is functional Element of bool the carrier of (TOP-REAL 2)
Cl ((LSeg (n,G)) \ {n,G}) is functional Element of bool the carrier of (TOP-REAL 2)
{ [b1,b2] where b1, b2 is V11() real ext-real Element of REAL : b1 <= b2 } is set
n is set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
[G,f] is set
{G,f} is finite V69() V70() V71() set
{G} is non empty trivial finite 1 -element V69() V70() V71() set
{{G,f},{G}} is finite V32() set
() is Relation-like REAL -defined REAL -valued V59() V60() V61() Element of bool [:REAL,REAL:]
C is V11() real ext-real Element of REAL
n is V11() real ext-real Element of REAL
[C,n] is set
{C,n} is finite V69() V70() V71() set
{C} is non empty trivial finite 1 -element V69() V70() V71() set
{{C,n},{C}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
[G,f] is set
{G,f} is finite V69() V70() V71() set
{G} is non empty trivial finite 1 -element V69() V70() V71() set
{{G,f},{G}} is finite V32() set
C is set
[C,C] is set
{C,C} is finite set
{C} is non empty trivial finite 1 -element set
{{C,C},{C}} is finite V32() set
n is V11() real ext-real Element of REAL
C is set
n is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,C] is set
{n,C} is finite set
{n} is non empty trivial finite 1 -element set
{{n,C},{n}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
C is set
n is set
G is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,G] is set
{n,G} is finite set
{n} is non empty trivial finite 1 -element set
{{n,G},{n}} is finite V32() set
[C,G] is set
{C,G} is finite set
{{C,G},{C}} is finite V32() set
f is V11() real ext-real Element of REAL
i1 is V11() real ext-real Element of REAL
j2 is V11() real ext-real Element of REAL
C is set
n is set
[C,n] is set
{C,n} is finite set
{C} is non empty trivial finite 1 -element set
{{C,n},{C}} is finite V32() set
[n,C] is set
{n,C} is finite set
{n} is non empty trivial finite 1 -element set
{{n,C},{n}} is finite V32() set
G is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
field () is set
dom () is set
rng () is V69() V70() V71() set
(dom ()) \/ (rng ()) is set
REAL \/ REAL is V69() V70() V71() set
dom () is V69() V70() V71() Element of bool REAL
C is set
n is V11() real ext-real Element of REAL
[n,n] is set
{n,n} is finite V69() V70() V71() set
{n} is non empty trivial finite 1 -element V69() V70() V71() set
{{n,n},{n}} is finite V32() set
C is finite V69() V70() V71() Element of bool REAL
SgmX ((),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom (SgmX ((),C)) is finite set
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(SgmX ((),C)) . f is V11() real ext-real Element of REAL
(SgmX ((),C)) . G is V11() real ext-real Element of REAL
dom (SgmX ((),C)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(SgmX ((),C)) /. G is V11() real ext-real Element of REAL
(SgmX ((),C)) /. f is V11() real ext-real Element of REAL
[((SgmX ((),C)) . G),((SgmX ((),C)) . f)] is set
{((SgmX ((),C)) . G),((SgmX ((),C)) . f)} is finite V69() V70() V71() set
{((SgmX ((),C)) . G)} is non empty trivial finite 1 -element V69() V70() V71() set
{{((SgmX ((),C)) . G),((SgmX ((),C)) . f)},{((SgmX ((),C)) . G)}} is finite V32() set
C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
rng C is finite V69() V70() V71() Element of bool REAL
Incr C is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
n is finite V69() V70() V71() Element of bool REAL
SgmX ((),n) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
rng (SgmX ((),n)) is finite V69() V70() V71() Element of bool REAL
G is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
len G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
card (rng C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is finite V69() V70() V71() Element of bool REAL
SgmX ((),C) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
C is non empty set
bool C is set
[:C,C:] is Relation-like set
bool [:C,C:] is set
n is finite Element of bool C
card n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
G is Relation-like C -defined C -valued total reflexive antisymmetric transitive being_linear-order Element of bool [:C,C:]
SgmX (G,n) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of C
len (SgmX (G,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
field G is set
dom G is set
rng G is set
(dom G) \/ (rng G) is set
C is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
X_axis C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
proj1 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
len (X_axis C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom (X_axis C) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
G is ordinal natural V11() real integer finite cardinal ext-real non negative set
(X_axis C) . G is V11() real ext-real Element of REAL
n . G is V11() real ext-real Element of REAL
C /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
C . G is Relation-like Function-like set
(C /. G) `1 is V11() real ext-real Element of REAL
(C /. G) . 1 is V11() real ext-real Element of REAL
proj1 . (C . G) is V11() real ext-real Element of REAL
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
C is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
Y_axis C is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
proj2 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
len (Y_axis C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom (Y_axis C) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
n is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
G is ordinal natural V11() real integer finite cardinal ext-real non negative set
(Y_axis C) . G is V11() real ext-real Element of REAL
n . G is V11() real ext-real Element of REAL
C /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
C . G is Relation-like Function-like set
(C /. G) `2 is V11() real ext-real Element of REAL
(C /. G) . 2 is V11() real ext-real Element of REAL
proj2 . (C . G) is V11() real ext-real Element of REAL
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
C is non empty set
C * is non empty functional FinSequence-membered FinSequenceSet of C
n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *
Values n is finite set
bool C is set
rng n is functional finite FinSequence-membered Element of bool (C *)
bool (C *) is set
{ (rng b1) where b1 is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of C * : b1 in rng n } is set
f is set
i1 is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of C *
rng i1 is finite Element of bool C
union { (rng b1) where b1 is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of C * : b1 in rng n } is set
C is non empty with_non-empty_elements non empty-membered set
C * is non empty functional FinSequence-membered FinSequenceSet of C
n is non empty Relation-like non-empty NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() FinSequence-yielding finite-support FinSequence of C *
(C,n) is finite Element of bool C
bool C is set
rngs n is Relation-like non-empty Function-like set
dom (rngs n) is set
dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng (rngs n) is with_non-empty_elements set
Union (rngs n) is set
G is non empty with_non-empty_elements non empty-membered set
union G is non empty set
C is non empty set
C * is non empty functional FinSequence-membered FinSequenceSet of C
n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular FinSequence-yielding finite-support FinSequence of C *
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (width n) is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
(C,n) is finite Element of bool C
bool C is set
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Col (n,G) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len n) -tuples_on C
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len n) -tuples_on C is functional FinSequence-membered FinSequenceSet of C
rng (Col (n,G)) is finite Element of bool C
f is set
dom (Col (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
i1 is set
(Col (n,G)) . i1 is set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Col (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,G] is set
{j2,G} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,G},{j2}} is finite V32() set
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(Col (n,G)) . j2 is set
n * (j2,G) is Element of C
C is non empty set
C * is non empty functional FinSequence-membered FinSequenceSet of C
n is Relation-like NAT -defined C * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular FinSequence-yielding finite-support FinSequence of C *
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(C,n) is finite Element of bool C
bool C is set
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Line (n,G) is Relation-like NAT -defined C -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width n) -tuples_on C
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(width n) -tuples_on C is functional FinSequence-membered FinSequenceSet of C
rng (Line (n,G)) is finite Element of bool C
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is set
dom (Line (n,G)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
i1 is set
(Line (n,G)) . i1 is set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Line (n,G)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[G,j2] is set
{G,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,j2},{G}} is finite V32() set
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
Seg (width n) is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
(Line (n,G)) . j2 is set
n * (G,j2) is Element of C
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Seg (width C) is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT
Col (C,1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support Element of (len C) -tuples_on the carrier of (TOP-REAL 2)
(len C) -tuples_on the carrier of (TOP-REAL 2) is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
X_axis (Col (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
n is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
rng n is finite V69() V70() V71() Element of bool REAL
card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Col (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
proj1 * (Col (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
rng (proj1 * (Col (C,1))) is finite V69() V70() V71() Element of bool REAL
rng (Col (C,1)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: (rng (Col (C,1))) is finite V69() V70() V71() Element of bool REAL
C is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng n is finite set
G is set
Indices C is set
{ (C * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices C } is set
f is set
proj1 . f is V11() real ext-real Element of REAL
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 `1 is V11() real ext-real Element of REAL
j2 . 1 is V11() real ext-real Element of REAL
C * (i1,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(C * (i1,1)) `1 is V11() real ext-real Element of REAL
(C * (i1,1)) . 1 is V11() real ext-real Element of REAL
proj1 . (C * (i1,1)) is V11() real ext-real Element of REAL
n . i1 is set
card (dom C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_increasing-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Line (C,1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support Element of (width C) -tuples_on the carrier of (TOP-REAL 2)
(width C) -tuples_on the carrier of (TOP-REAL 2) is functional FinSequence-membered FinSequenceSet of the carrier of (TOP-REAL 2)
Y_axis (Line (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
n is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
rng n is finite V69() V70() V71() Element of bool REAL
card (rng n) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Line (C,1)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
proj2 * (Line (C,1)) is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
rng (proj2 * (Line (C,1))) is finite V69() V70() V71() Element of bool REAL
rng (Line (C,1)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: (rng (Line (C,1))) is finite V69() V70() V71() Element of bool REAL
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_equal-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Seg (width C) is finite width C -element V69() V70() V71() V72() V73() V74() Element of bool NAT
rng n is finite set
G is set
Indices C is set
{ (C * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices C } is set
f is set
proj2 . f is V11() real ext-real Element of REAL
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 `2 is V11() real ext-real Element of REAL
j2 . 2 is V11() real ext-real Element of REAL
C * (1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(C * (1,j2)) `2 is V11() real ext-real Element of REAL
(C * (1,j2)) . 2 is V11() real ext-real Element of REAL
proj2 . (C * (1,j2)) is V11() real ext-real Element of REAL
n . j2 is set
card (Seg (width C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular Y_equal-in-column Y_increasing-in-line FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),C) is finite V69() V70() V71() Element of bool REAL
card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg (n,G) is functional Element of bool the carrier of (TOP-REAL 2)
left_cell (n,G,C) is functional Element of bool the carrier of (TOP-REAL 2)
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Indices C is set
n /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}} is finite V32() set
C * (f,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n /. (G + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j2] is set
{j2,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j2},{j2}} is finite V32() set
C * (j2,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,(f -' 1),i1) is functional Element of bool the carrier of (TOP-REAL 2)
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,f,i1) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,j2,(j2 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,f,j2) is functional Element of bool the carrier of (TOP-REAL 2)
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f - j2 is V11() real integer ext-real Element of REAL
abs (f - j2) is V11() real ext-real Element of REAL
i1 - j2 is V11() real integer ext-real Element of REAL
abs (i1 - j2) is V11() real ext-real Element of REAL
(abs (f - j2)) + (abs (i1 - j2)) is V11() real ext-real Element of REAL
(f -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(j2 -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
GoB n is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
left_cell (n,C,(GoB n)) is functional Element of bool the carrier of (TOP-REAL 2)
left_cell (n,C) is functional Element of bool the carrier of (TOP-REAL 2)
Indices (GoB n) is set
n /. C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n /. (C + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}} is finite V32() set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j2] is set
{j2,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j2},{j2}} is finite V32() set
(GoB n) * (f,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(GoB n) * (j2,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),(f -' 1),i1) is functional Element of bool the carrier of (TOP-REAL 2)
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),f,i1) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),j2,(j2 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),f,j2) is functional Element of bool the carrier of (TOP-REAL 2)
f - j2 is V11() real integer ext-real Element of REAL
abs (f - j2) is V11() real ext-real Element of REAL
i1 - j2 is V11() real integer ext-real Element of REAL
abs (i1 - j2) is V11() real ext-real Element of REAL
(abs (f - j2)) + (abs (i1 - j2)) is V11() real ext-real Element of REAL
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg (n,G) is functional Element of bool the carrier of (TOP-REAL 2)
right_cell (n,G,C) is functional Element of bool the carrier of (TOP-REAL 2)
dom n is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Indices C is set
n /. G is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}} is finite V32() set
C * (f,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n /. (G + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j2] is set
{j2,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j2},{j2}} is finite V32() set
C * (j2,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,f,i1) is functional Element of bool the carrier of (TOP-REAL 2)
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,f,(i1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell (C,(f -' 1),j2) is functional Element of bool the carrier of (TOP-REAL 2)
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f - j2 is V11() real integer ext-real Element of REAL
abs (f - j2) is V11() real ext-real Element of REAL
i1 - j2 is V11() real integer ext-real Element of REAL
abs (i1 - j2) is V11() real ext-real Element of REAL
(abs (f - j2)) + (abs (i1 - j2)) is V11() real ext-real Element of REAL
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(i1 -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(f -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg ((n /. G),(n /. (G + 1))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * (n /. G)) + (b1 * (n /. (G + 1)))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
GoB n is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
right_cell (n,C,(GoB n)) is functional Element of bool the carrier of (TOP-REAL 2)
right_cell (n,C) is functional Element of bool the carrier of (TOP-REAL 2)
Indices (GoB n) is set
n /. C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n /. (C + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j4] is set
{j2,j4} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j4},{j2}} is finite V32() set
(GoB n) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(GoB n) * (j2,j4) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),i1,j2) is functional Element of bool the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),i1,(j2 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),j2,j4) is functional Element of bool the carrier of (TOP-REAL 2)
j4 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB n),(i1 -' 1),j4) is functional Element of bool the carrier of (TOP-REAL 2)
i1 - j2 is V11() real integer ext-real Element of REAL
abs (i1 - j2) is V11() real ext-real Element of REAL
j2 - j4 is V11() real integer ext-real Element of REAL
abs (j2 - j4) is V11() real ext-real Element of REAL
(abs (i1 - j2)) + (abs (j2 - j4)) is V11() real ext-real Element of REAL
C is functional Element of bool the carrier of (TOP-REAL 2)
n is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
L~ n is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(L~ n) ` is functional Element of bool the carrier of (TOP-REAL 2)
RightComp n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LeftComp n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(TOP-REAL 2) | ((L~ n) `) is strict T_2 SubSpace of TOP-REAL 2
the carrier of ((TOP-REAL 2) | ((L~ n) `)) is set
bool the carrier of ((TOP-REAL 2) | ((L~ n) `)) is set
G is Element of bool the carrier of ((TOP-REAL 2) | ((L~ n) `))
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
n is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
RightComp n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LeftComp n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
right_cell (n,G,C) is functional Element of bool the carrier of (TOP-REAL 2)
Int (right_cell (n,G,C)) is functional Element of bool the carrier of (TOP-REAL 2)
left_cell (n,G,C) is functional Element of bool the carrier of (TOP-REAL 2)
Int (left_cell (n,G,C)) is functional Element of bool the carrier of (TOP-REAL 2)
L~ n is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(right_cell (n,G,C)) \ (L~ n) is functional Element of bool the carrier of (TOP-REAL 2)
(left_cell (n,G,C)) \ (L~ n) is functional Element of bool the carrier of (TOP-REAL 2)
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[C,n] is set
{C,n} is finite V32() V69() V70() V71() V72() V73() V74() set
{C} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{C,n},{C}} is finite V32() set
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[G,f] is set
{G,f} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,f},{G}} is finite V32() set
i1 is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices i1 is set
i1 * (C,n) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 * (G,f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
width i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 * (C,f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(i1 * (C,f)) `2 is V11() real ext-real Element of REAL
(i1 * (C,f)) . 2 is V11() real ext-real Element of REAL
i1 * (1,f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(i1 * (1,f)) `2 is V11() real ext-real Element of REAL
(i1 * (1,f)) . 2 is V11() real ext-real Element of REAL
(i1 * (C,n)) `2 is V11() real ext-real Element of REAL
(i1 * (C,n)) . 2 is V11() real ext-real Element of REAL
(i1 * (C,f)) `1 is V11() real ext-real Element of REAL
(i1 * (C,f)) . 1 is V11() real ext-real Element of REAL
i1 * (C,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(i1 * (C,1)) `1 is V11() real ext-real Element of REAL
(i1 * (C,1)) . 1 is V11() real ext-real Element of REAL
(i1 * (C,n)) `1 is V11() real ext-real Element of REAL
(i1 * (C,n)) . 1 is V11() real ext-real Element of REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
mid (G,C,n) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
f is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
C -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G /^ (C -' 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
n -' C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n -' C) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(G /^ (C -' 1)) | ((n -' C) + 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
n -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G /^ (n -' 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
C -' n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(C -' n) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(G /^ (n -' 1)) | ((C -' n) + 1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
Rev ((G /^ (n -' 1)) | ((C -' n) + 1)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
C is Relation-like non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
rng C is functional finite FinSequence-membered Element of bool ( the carrier of (TOP-REAL 2) *)
bool ( the carrier of (TOP-REAL 2) *) is set
n is ordinal natural V11() real integer finite cardinal ext-real non negative set
len C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom C is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f is set
C . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
card (C . f) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
i1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),n) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),n) is finite V69() V70() V71() Element of bool REAL
SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),n))) is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
(SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),n)))) . C is V11() real ext-real Element of REAL
n * (C,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (C,1)) `1 is V11() real ext-real Element of REAL
(n * (C,1)) . 1 is V11() real ext-real Element of REAL
dom n is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
Seg (len n) is non empty finite len n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom f is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng f is finite V69() V70() V71() Element of bool REAL
G is finite V69() V70() V71() Element of bool REAL
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
i1 is set
j2 is V11() real ext-real Element of REAL
j2 is set
f . j2 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j4,1] is set
{j4,1} is finite V32() V69() V70() V71() V72() V73() V74() set
{j4} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j4,1},{j4}} is finite V32() set
n * (j4,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (j4,1)) `1 is V11() real ext-real Element of REAL
(n * (j4,1)) . 1 is V11() real ext-real Element of REAL
proj1 . (n * (j4,1)) is V11() real ext-real Element of REAL
i1 is set
j2 is V11() real ext-real Element of REAL
j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
proj1 . j2 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i5 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (j4,i5) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j4,i5] is set
{j4,i5} is finite V32() V69() V70() V71() V72() V73() V74() set
{j4} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j4,i5},{j4}} is finite V32() set
j2 `1 is V11() real ext-real Element of REAL
j2 . 1 is V11() real ext-real Element of REAL
n * (j4,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (j4,1)) `1 is V11() real ext-real Element of REAL
(n * (j4,1)) . 1 is V11() real ext-real Element of REAL
f . j4 is V11() real ext-real Element of REAL
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative set
f /. i1 is V11() real ext-real Element of REAL
f /. j2 is V11() real ext-real Element of REAL
[(f /. i1),(f /. j2)] is set
{(f /. i1),(f /. j2)} is finite V69() V70() V71() set
{(f /. i1)} is non empty trivial finite 1 -element V69() V70() V71() set
{{(f /. i1),(f /. j2)},{(f /. i1)}} is finite V32() set
f . i1 is V11() real ext-real Element of REAL
f . j2 is V11() real ext-real Element of REAL
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (j2,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (j2,1)) `1 is V11() real ext-real Element of REAL
(n * (j2,1)) . 1 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (j4,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (j4,1)) `1 is V11() real ext-real Element of REAL
(n * (j4,1)) . 1 is V11() real ext-real Element of REAL
f . j4 is V11() real ext-real Element of REAL
f . j2 is V11() real ext-real Element of REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),n) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),n) is finite V69() V70() V71() Element of bool REAL
SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),n))) is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
(SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),n)))) . C is V11() real ext-real Element of REAL
n * (1,C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,C)) `2 is V11() real ext-real Element of REAL
(n * (1,C)) . 2 is V11() real ext-real Element of REAL
Seg (width n) is finite width n -element V69() V70() V71() V72() V73() V74() Element of bool NAT
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom f is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rng f is finite V69() V70() V71() Element of bool REAL
G is finite V69() V70() V71() Element of bool REAL
Indices n is set
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
i1 is set
j2 is V11() real ext-real Element of REAL
j2 is set
f . j2 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[1,j4] is set
{1,j4} is finite V32() V69() V70() V71() V72() V73() V74() set
{1} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{1,j4},{1}} is finite V32() set
n * (1,j4) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,j4)) `2 is V11() real ext-real Element of REAL
(n * (1,j4)) . 2 is V11() real ext-real Element of REAL
proj2 . (n * (1,j4)) is V11() real ext-real Element of REAL
i1 is set
j2 is V11() real ext-real Element of REAL
j2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
proj2 . j2 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i5 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (j4,i5) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j4,i5] is set
{j4,i5} is finite V32() V69() V70() V71() V72() V73() V74() set
{j4} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j4,i5},{j4}} is finite V32() set
j2 `2 is V11() real ext-real Element of REAL
j2 . 2 is V11() real ext-real Element of REAL
n * (1,i5) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,i5)) `2 is V11() real ext-real Element of REAL
(n * (1,i5)) . 2 is V11() real ext-real Element of REAL
f . i5 is V11() real ext-real Element of REAL
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative set
f /. i1 is V11() real ext-real Element of REAL
f /. j2 is V11() real ext-real Element of REAL
[(f /. i1),(f /. j2)] is set
{(f /. i1),(f /. j2)} is finite V69() V70() V71() set
{(f /. i1)} is non empty trivial finite 1 -element V69() V70() V71() set
{{(f /. i1),(f /. j2)},{(f /. i1)}} is finite V32() set
f . i1 is V11() real ext-real Element of REAL
f . j2 is V11() real ext-real Element of REAL
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,j2)) `2 is V11() real ext-real Element of REAL
(n * (1,j2)) . 2 is V11() real ext-real Element of REAL
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (1,j4) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,j4)) `2 is V11() real ext-real Element of REAL
(n * (1,j4)) . 2 is V11() real ext-real Element of REAL
f . j4 is V11() real ext-real Element of REAL
f . j2 is V11() real ext-real Element of REAL
C is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
rng C is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices n is set
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),n) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),n) is finite V69() V70() V71() Element of bool REAL
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[1,G] is set
{1,G} is finite V32() V69() V70() V71() V72() V73() V74() set
{1} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{1,G},{1}} is finite V32() set
n * (1,G) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom C is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f is set
C . f is Relation-like Function-like set
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(len n),j2] is set
{(len n),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(len n)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(len n),j2},{(len n)}} is finite V32() set
n * ((len n),j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is set
C . j2 is Relation-like Function-like set
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
mid (C,i1,j4) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j4 -' i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j4 -' i1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(i1 -' j4) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
rng (mid (C,i1,j4)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: (rng (mid (C,i1,j4))) is finite V69() V70() V71() Element of bool REAL
j5 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
proj1 . p is V11() real ext-real Element of REAL
i0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (i0,j0) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i0,j0] is set
{i0,j0} is finite V32() V69() V70() V71() V72() V73() V74() set
{i0} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i0,j0},{i0}} is finite V32() set
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . n is Relation-like Function-like set
n + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . (n + 1) is Relation-like Function-like set
i is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i,j] is set
{i,j} is finite V32() V69() V70() V71() V72() V73() V74() set
{i} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i,j},{i}} is finite V32() set
n * (i,j) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom (mid (C,i1,j4)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(mid (C,i1,j4)) /. (n + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom proj1 is functional Element of bool the carrier of (TOP-REAL 2)
p `1 is V11() real ext-real Element of REAL
p . 1 is V11() real ext-real Element of REAL
n * (i0,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (i0,1)) `1 is V11() real ext-real Element of REAL
(n * (i0,1)) . 1 is V11() real ext-real Element of REAL
(n * (i,j)) `1 is V11() real ext-real Element of REAL
(n * (i,j)) . 1 is V11() real ext-real Element of REAL
proj1 . ((mid (C,i1,j4)) /. (n + 1)) is V11() real ext-real Element of REAL
(mid (C,i1,j4)) /. n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j1] is set
{i1,j1} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j1},{i1}} is finite V32() set
n * (i1,j1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 - i is V11() real integer ext-real Element of REAL
abs (i1 - i) is V11() real ext-real Element of REAL
j1 - j is V11() real integer ext-real Element of REAL
abs (j1 - j) is V11() real ext-real Element of REAL
(abs (i1 - i)) + (abs (j1 - j)) is V11() real ext-real Element of REAL
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . (len (mid (C,i1,j4))) is Relation-like Function-like set
(mid (C,i1,j4)) . 0 is Relation-like Function-like set
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[n,i] is set
{n,i} is finite V32() V69() V70() V71() V72() V73() V74() set
{n} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{n,i},{n}} is finite V32() set
n * (n,i) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
C is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
rng C is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices n is set
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
( the carrier of (TOP-REAL 2),n) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),n) is finite V69() V70() V71() Element of bool REAL
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[G,1] is set
{G,1} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,1},{G}} is finite V32() set
n * (G,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom C is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
f is set
C . f is Relation-like Function-like set
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,(width n)] is set
{j2,(width n)} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,(width n)},{j2}} is finite V32() set
n * (j2,(width n)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is set
C . j2 is Relation-like Function-like set
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len C is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
mid (C,i1,j4) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j4 -' i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j4 -' i1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(i1 -' j4) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (mid (C,i1,j4)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
{ (n * (b1,b2)) where b1, b2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT : [b1,b2] in Indices n } is set
rng (mid (C,i1,j4)) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: (rng (mid (C,i1,j4))) is finite V69() V70() V71() Element of bool REAL
j5 is V11() real ext-real Element of REAL
p is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
proj2 . p is V11() real ext-real Element of REAL
i0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n * (i0,j0) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i0,j0] is set
{i0,j0} is finite V32() V69() V70() V71() V72() V73() V74() set
{i0} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i0,j0},{i0}} is finite V32() set
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . n is Relation-like Function-like set
n + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . (n + 1) is Relation-like Function-like set
i is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i,j] is set
{i,j} is finite V32() V69() V70() V71() V72() V73() V74() set
{i} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i,j},{i}} is finite V32() set
n * (i,j) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom (mid (C,i1,j4)) is finite V69() V70() V71() V72() V73() V74() Element of bool NAT
(mid (C,i1,j4)) /. (n + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
dom proj2 is functional Element of bool the carrier of (TOP-REAL 2)
p `2 is V11() real ext-real Element of REAL
p . 2 is V11() real ext-real Element of REAL
n * (1,j0) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(n * (1,j0)) `2 is V11() real ext-real Element of REAL
(n * (1,j0)) . 2 is V11() real ext-real Element of REAL
(n * (i,j)) `2 is V11() real ext-real Element of REAL
(n * (i,j)) . 2 is V11() real ext-real Element of REAL
proj2 . ((mid (C,i1,j4)) /. (n + 1)) is V11() real ext-real Element of REAL
(mid (C,i1,j4)) /. n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j1] is set
{i1,j1} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j1},{i1}} is finite V32() set
n * (i1,j1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 - i is V11() real integer ext-real Element of REAL
abs (i1 - i) is V11() real ext-real Element of REAL
j1 - j is V11() real integer ext-real Element of REAL
abs (j1 - j) is V11() real ext-real Element of REAL
(abs (i1 - i)) + (abs (j1 - j)) is V11() real ext-real Element of REAL
j1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(mid (C,i1,j4)) . (len (mid (C,i1,j4))) is Relation-like Function-like set
(mid (C,i1,j4)) . 0 is Relation-like Function-like set
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[n,i] is set
{n,i} is finite V32() V69() V70() V71() V72() V73() V74() set
{n} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{n,i},{n}} is finite V32() set
n * (n,i) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
C is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
( the carrier of (TOP-REAL 2),C) is functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
dom C is non empty finite V69() V70() V71() V72() V73() V74() Element of bool NAT
rngs C is Relation-like non-empty Function-like set
n is non empty Relation-like non-empty Function-like set
Union n is non empty set
C is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
( the carrier of (TOP-REAL 2),C) is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),C) is non empty finite V69() V70() V71() Element of bool REAL
SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),C))) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
proj2 .: ( the carrier of (TOP-REAL 2),C) is non empty finite V69() V70() V71() Element of bool REAL
SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),C))) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
GoB ((SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),C)))),(SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),C))))) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
width C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
card (proj2 .: ( the carrier of (TOP-REAL 2),C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len (SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),C)))) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Indices C is set
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),C)))) . f is V11() real ext-real Element of REAL
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}} is finite V32() set
C * (f,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),C)))) . i1 is V11() real ext-real Element of REAL
|[((SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),C)))) . f),((SgmX ((),(proj2 .: ( the carrier of (TOP-REAL 2),C)))) . i1)]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
len C is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C * (f,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(C * (f,1)) `1 is V11() real ext-real Element of REAL
(C * (f,1)) . 1 is V11() real ext-real Element of REAL
(C * (f,i1)) `1 is V11() real ext-real Element of REAL
(C * (f,i1)) . 1 is V11() real ext-real Element of REAL
C * (1,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(C * (1,i1)) `2 is V11() real ext-real Element of REAL
(C * (1,i1)) . 2 is V11() real ext-real Element of REAL
(C * (f,i1)) `2 is V11() real ext-real Element of REAL
(C * (f,i1)) . 2 is V11() real ext-real Element of REAL
len C is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
card (proj1 .: ( the carrier of (TOP-REAL 2),C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of omega
len (SgmX ((),(proj1 .: ( the carrier of (TOP-REAL 2),C)))) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
rng C is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
proj2 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
GoB C is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
( the carrier of (TOP-REAL 2),n) is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj1 .: ( the carrier of (TOP-REAL 2),n) is non empty finite V69() V70() V71() Element of bool REAL
proj2 .: ( the carrier of (TOP-REAL 2),n) is non empty finite V69() V70() V71() Element of bool REAL
X_axis C is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
proj1 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
[:NAT,REAL:] is non empty non trivial Relation-like non finite non empty-membered V59() V60() V61() set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
rng (X_axis C) is non empty finite V69() V70() V71() Element of bool REAL
Incr (X_axis C) is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
SgmX ((),(proj1 .: (rng C))) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
Y_axis C is non empty Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V59() V60() V61() finite-support FinSequence of REAL
proj2 * C is Relation-like NAT -defined REAL -valued Function-like finite V59() V60() V61() finite-support Element of bool [:NAT,REAL:]
rng (Y_axis C) is non empty finite V69() V70() V71() Element of bool REAL
Incr (Y_axis C) is Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
SgmX ((),(proj2 .: (rng C))) is non empty Relation-like NAT -defined REAL -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like V59() V60() V61() increasing V65() finite-support FinSequence of REAL
GoB ((Incr (X_axis C)),(Incr (Y_axis C))) is Relation-like NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
C is non empty Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
rng C is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
GoB C is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
n is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices n is set
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[1,G] is set
{1,G} is finite V32() V69() V70() V71() V72() V73() V74() set
{1} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{1,G},{1}} is finite V32() set
n * (1,G) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,1] is set
{f,1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,1},{f}} is finite V32() set
n * (f,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(len n),i1] is set
{(len n),i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{(len n)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(len n),i1},{(len n)}} is finite V32() set
n * ((len n),i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,(width n)] is set
{j2,(width n)} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,(width n)},{j2}} is finite V32() set
n * (j2,(width n)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
proj2 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
( the carrier of (TOP-REAL 2),n) is non empty functional finite closed bounded compact Element of bool the carrier of (TOP-REAL 2)
proj2 .: ( the carrier of (TOP-REAL 2),n) is non empty finite V69() V70() V71() Element of bool REAL
proj1 .: (rng C) is non empty finite V69() V70() V71() Element of bool REAL
proj1 .: ( the carrier of (TOP-REAL 2),n) is non empty finite V69() V70() V71() Element of bool REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C - 2 is V11() real integer ext-real Element of REAL
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n -' G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n -' G) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(C - 2) / (2 |^ (n -' G)) is V11() real ext-real Element of REAL
((C - 2) / (2 |^ (n -' G))) + 2 is V11() real ext-real Element of REAL
[\(((C - 2) / (2 |^ (n -' G))) + 2)/] is V11() real integer ext-real set
(((C - 2) / (2 |^ (n -' G))) + 2) - 1 is V11() real ext-real Element of REAL
2 - 1 is V11() real integer ext-real Element of REAL
((C - 2) / (2 |^ (n -' G))) + (2 - 1) is V11() real ext-real Element of REAL
((C - 2) / (2 |^ (n -' G))) + 1 is V11() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n -' G) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) / 1 is V11() real ext-real non positive Element of REAL
(- 1) / (2 |^ (n -' G)) is V11() real ext-real non positive Element of REAL
1 - 2 is V11() real integer ext-real Element of REAL
(- 1) + 1 is V11() real integer ext-real Element of REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n -' C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n -' C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G - 2 is V11() real integer ext-real Element of REAL
(G - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + 2 is V11() real ext-real Element of REAL
[\(((G - 2) / (2 |^ (n -' C))) + 2)/] is V11() real integer ext-real set
[\(((G - 2) / (2 |^ (n -' C))) + 2)/] + 1 is V11() real integer ext-real Element of REAL
f is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Gauge (f,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (f,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (f,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (f,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n -' C) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ n) + (2 + 1) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ n) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
((2 |^ n) + 2) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C + (n -' C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (C + (n -' C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(G - 2) * 1 is V11() real integer ext-real Element of REAL
2 |^ C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ C) * (2 |^ (n -' C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ C) / 1 is V11() real ext-real non negative Element of REAL
((G - 2) / (2 |^ (n -' C))) + 3 is V11() real ext-real Element of REAL
(2 |^ C) + 3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(((G - 2) / (2 |^ (n -' C))) + 2) - 1 is V11() real ext-real Element of REAL
2 - 1 is V11() real integer ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + (2 - 1) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + 1 is V11() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) / 1 is V11() real ext-real non positive Element of REAL
(- 1) / (2 |^ (n -' C)) is V11() real ext-real non positive Element of REAL
1 - 2 is V11() real integer ext-real Element of REAL
(- 1) + 1 is V11() real integer ext-real Element of REAL
1 + 0 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(((G - 2) / (2 |^ (n -' C))) + 2) + 1 is V11() real ext-real Element of REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n -' C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n -' C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G - 2 is V11() real integer ext-real Element of REAL
(G - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + 2 is V11() real ext-real Element of REAL
[\(((G - 2) / (2 |^ (n -' C))) + 2)/] is V11() real integer ext-real set
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f - 2 is V11() real integer ext-real Element of REAL
(f - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
((f - 2) / (2 |^ (n -' C))) + 2 is V11() real ext-real Element of REAL
[\(((f - 2) / (2 |^ (n -' C))) + 2)/] is V11() real integer ext-real set
i1 is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Gauge (i1,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (i1,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (i1,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (i1,n)),G,f) is functional Element of bool the carrier of (TOP-REAL 2)
Gauge (i1,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (i1,C)),j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
j5 is set
p is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
p `2 is V11() real ext-real Element of REAL
p . 2 is V11() real ext-real Element of REAL
(Gauge (i1,n)) * (G,(f + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,n)) * (G,(f + 1))) `2 is V11() real ext-real Element of REAL
((Gauge (i1,n)) * (G,(f + 1))) . 2 is V11() real ext-real Element of REAL
[G,f] is set
{G,f} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,f},{G}} is finite V32() set
Indices (Gauge (i1,n)) is set
(Gauge (i1,n)) * (G,f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
W-bound i1 is V11() real ext-real Element of REAL
E-bound i1 is V11() real ext-real Element of REAL
(E-bound i1) - (W-bound i1) is V11() real ext-real Element of REAL
2 |^ n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
((E-bound i1) - (W-bound i1)) / (2 |^ n) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (G - 2) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (G - 2)) is V11() real ext-real Element of REAL
S-bound i1 is V11() real ext-real Element of REAL
N-bound i1 is V11() real ext-real Element of REAL
(N-bound i1) - (S-bound i1) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) / (2 |^ n) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (f - 2) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (f - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (G - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (f - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,n)) * (G,f)) `1 is V11() real ext-real Element of REAL
((Gauge (i1,n)) * (G,f)) . 1 is V11() real ext-real Element of REAL
(G - 2) / 1 is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ n)) * ((G - 2) / 1) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * ((G - 2) / 1)) is V11() real ext-real Element of REAL
((E-bound i1) - (W-bound i1)) / 1 is V11() real ext-real Element of REAL
(G - 2) / (2 |^ n) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / 1) * ((G - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / 1) * ((G - 2) / (2 |^ n))) is V11() real ext-real Element of REAL
p `1 is V11() real ext-real Element of REAL
p . 1 is V11() real ext-real Element of REAL
((Gauge (i1,n)) * (G,f)) `2 is V11() real ext-real Element of REAL
((Gauge (i1,n)) * (G,f)) . 2 is V11() real ext-real Element of REAL
(f - 2) / 1 is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ n)) * ((f - 2) / 1) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * ((f - 2) / 1)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) / 1 is V11() real ext-real Element of REAL
(f - 2) / (2 |^ n) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / 1) * ((f - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / 1) * ((f - 2) / (2 |^ n))) is V11() real ext-real Element of REAL
(Gauge (i1,n)) * ((G + 1),f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,n)) * ((G + 1),f)) `1 is V11() real ext-real Element of REAL
((Gauge (i1,n)) * ((G + 1),f)) . 1 is V11() real ext-real Element of REAL
(W-bound i1) + 0 is V11() real ext-real Element of REAL
[G,(f + 1)] is set
{G,(f + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{G,(f + 1)},{G}} is finite V32() set
(f + 1) - 2 is V11() real integer ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ n)) * ((f + 1) - 2) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * ((f + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (G - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * ((f + 1) - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((f + 1) - 2) / 1 is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (((f + 1) - 2) / 1) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (((f + 1) - 2) / 1)) is V11() real ext-real Element of REAL
((f + 1) - 2) / (2 |^ n) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / 1) * (((f + 1) - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / 1) * (((f + 1) - 2) / (2 |^ n))) is V11() real ext-real Element of REAL
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n -' C) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
- 1 is V11() real integer ext-real non positive Element of REAL
(- 1) / 1 is V11() real ext-real non positive Element of REAL
(- 1) / (2 |^ (n -' C)) is V11() real ext-real non positive Element of REAL
[(G + 1),f] is set
{(G + 1),f} is finite V32() V69() V70() V71() V72() V73() V74() set
{(G + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(G + 1),f},{(G + 1)}} is finite V32() set
(G + 1) - 2 is V11() real integer ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ n)) * ((G + 1) - 2) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * ((G + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * ((G + 1) - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ n)) * (f - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((G + 1) - 2) / 1 is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (((G + 1) - 2) / 1) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ n)) * (((G + 1) - 2) / 1)) is V11() real ext-real Element of REAL
((G + 1) - 2) / (2 |^ n) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / 1) * (((G + 1) - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / 1) * (((G + 1) - 2) / (2 |^ n))) is V11() real ext-real Element of REAL
(((G - 2) / (2 |^ (n -' C))) + 2) - 1 is V11() real ext-real Element of REAL
2 - 1 is V11() real integer ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + (2 - 1) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + 1 is V11() real ext-real Element of REAL
1 - 2 is V11() real integer ext-real Element of REAL
(- 1) + 1 is V11() real integer ext-real Element of REAL
1 + 0 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(S-bound i1) + 0 is V11() real ext-real Element of REAL
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j2 + 1) - 2 is V11() real integer ext-real Element of REAL
(G - 2) + 1 is V11() real integer ext-real Element of REAL
((j2 + 1) - 2) * (2 |^ (n -' C)) is V11() real integer ext-real Element of REAL
((G + 1) - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
2 |^ C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(((G + 1) - 2) / (2 |^ (n -' C))) / (2 |^ C) is V11() real ext-real Element of REAL
((j2 + 1) - 2) / (2 |^ C) is V11() real ext-real Element of REAL
(2 |^ (n -' C)) * (2 |^ C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
((G + 1) - 2) / ((2 |^ (n -' C)) * (2 |^ C)) is V11() real ext-real Element of REAL
(n -' C) + C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ ((n -' C) + C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
((G + 1) - 2) / (2 |^ ((n -' C) + C)) is V11() real ext-real Element of REAL
((E-bound i1) - (W-bound i1)) * (((G + 1) - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
((E-bound i1) - (W-bound i1)) * (((j2 + 1) - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
j2 - 2 is V11() real integer ext-real Element of REAL
(j2 - 2) / (2 |^ C) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) / (2 |^ C) is V11() real ext-real Element of REAL
(G - 2) / ((2 |^ (n -' C)) * (2 |^ C)) is V11() real ext-real Element of REAL
(G - 2) / (2 |^ ((n -' C) + C)) is V11() real ext-real Element of REAL
((E-bound i1) - (W-bound i1)) * ((j2 - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
((E-bound i1) - (W-bound i1)) * ((G - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
j2 - 2 is V11() real integer ext-real Element of REAL
(j2 - 2) / (2 |^ C) is V11() real ext-real Element of REAL
((f - 2) / (2 |^ (n -' C))) / (2 |^ C) is V11() real ext-real Element of REAL
(f - 2) / ((2 |^ (n -' C)) * (2 |^ C)) is V11() real ext-real Element of REAL
(f - 2) / (2 |^ ((n -' C) + C)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) * ((j2 - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) * ((f - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
(((f - 2) / (2 |^ (n -' C))) + 2) - 1 is V11() real ext-real Element of REAL
((f - 2) / (2 |^ (n -' C))) + (2 - 1) is V11() real ext-real Element of REAL
((f - 2) / (2 |^ (n -' C))) + 1 is V11() real ext-real Element of REAL
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j2 + 1) - 2 is V11() real integer ext-real Element of REAL
(f - 2) + 1 is V11() real integer ext-real Element of REAL
((j2 + 1) - 2) * (2 |^ (n -' C)) is V11() real integer ext-real Element of REAL
((f + 1) - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
(((f + 1) - 2) / (2 |^ (n -' C))) / (2 |^ C) is V11() real ext-real Element of REAL
((j2 + 1) - 2) / (2 |^ C) is V11() real ext-real Element of REAL
((f + 1) - 2) / ((2 |^ (n -' C)) * (2 |^ C)) is V11() real ext-real Element of REAL
((f + 1) - 2) / (2 |^ ((n -' C) + C)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) * (((f + 1) - 2) / (2 |^ n)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) * (((j2 + 1) - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
len (Gauge (i1,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (i1,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,(j2 + 1)] is set
{j2,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,(j2 + 1)},{j2}} is finite V32() set
Indices (Gauge (i1,C)) is set
(Gauge (i1,C)) * (j2,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((E-bound i1) - (W-bound i1)) / (2 |^ C) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (j2 - 2) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (j2 - 2)) is V11() real ext-real Element of REAL
((N-bound i1) - (S-bound i1)) / (2 |^ C) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (j2 - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,C)) * (j2,(j2 + 1))) `2 is V11() real ext-real Element of REAL
((Gauge (i1,C)) * (j2,(j2 + 1))) . 2 is V11() real ext-real Element of REAL
((j2 + 1) - 2) / 1 is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (((j2 + 1) - 2) / 1) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (((j2 + 1) - 2) / 1)) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / 1) * (((j2 + 1) - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / 1) * (((j2 + 1) - 2) / (2 |^ C))) is V11() real ext-real Element of REAL
[j2,j2] is set
{j2,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{{j2,j2},{j2}} is finite V32() set
(Gauge (i1,C)) * (j2,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (j2 - 2) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (j2 - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (j2 - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (j2 - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,C)) * (j2,j2)) `1 is V11() real ext-real Element of REAL
((Gauge (i1,C)) * (j2,j2)) . 1 is V11() real ext-real Element of REAL
(j2 - 2) / 1 is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ C)) * ((j2 - 2) / 1) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * ((j2 - 2) / 1)) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / 1) * ((j2 - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / 1) * ((j2 - 2) / (2 |^ C))) is V11() real ext-real Element of REAL
((Gauge (i1,C)) * (j2,j2)) `2 is V11() real ext-real Element of REAL
((Gauge (i1,C)) * (j2,j2)) . 2 is V11() real ext-real Element of REAL
(j2 - 2) / 1 is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / (2 |^ C)) * ((j2 - 2) / 1) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * ((j2 - 2) / 1)) is V11() real ext-real Element of REAL
(((N-bound i1) - (S-bound i1)) / 1) * ((j2 - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
(S-bound i1) + ((((N-bound i1) - (S-bound i1)) / 1) * ((j2 - 2) / (2 |^ C))) is V11() real ext-real Element of REAL
[(j2 + 1),j2] is set
{(j2 + 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(j2 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(j2 + 1),j2},{(j2 + 1)}} is finite V32() set
(Gauge (i1,C)) * ((j2 + 1),j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(((E-bound i1) - (W-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2)) is V11() real ext-real Element of REAL
|[((W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * ((j2 + 1) - 2))),((S-bound i1) + ((((N-bound i1) - (S-bound i1)) / (2 |^ C)) * (j2 - 2)))]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((Gauge (i1,C)) * ((j2 + 1),j2)) `1 is V11() real ext-real Element of REAL
((Gauge (i1,C)) * ((j2 + 1),j2)) . 1 is V11() real ext-real Element of REAL
((j2 + 1) - 2) / 1 is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (((j2 + 1) - 2) / 1) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / (2 |^ C)) * (((j2 + 1) - 2) / 1)) is V11() real ext-real Element of REAL
(((E-bound i1) - (W-bound i1)) / 1) * (((j2 + 1) - 2) / (2 |^ C)) is V11() real ext-real Element of REAL
(W-bound i1) + ((((E-bound i1) - (W-bound i1)) / 1) * (((j2 + 1) - 2) / (2 |^ C))) is V11() real ext-real Element of REAL
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Gauge (i1,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (i1,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (i1,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (i1,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (i1,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (i1,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (i1,n)),G,f) is functional Element of bool the carrier of (TOP-REAL 2)
G - 2 is V11() real integer ext-real Element of REAL
n -' C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n -' C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(G - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
((G - 2) / (2 |^ (n -' C))) + 2 is V11() real ext-real Element of REAL
[\(((G - 2) / (2 |^ (n -' C))) + 2)/] is V11() real integer ext-real set
f - 2 is V11() real integer ext-real Element of REAL
(f - 2) / (2 |^ (n -' C)) is V11() real ext-real Element of REAL
((f - 2) / (2 |^ (n -' C))) + 2 is V11() real ext-real Element of REAL
[\(((f - 2) / (2 |^ (n -' C))) + 2)/] is V11() real integer ext-real set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (i1,C)),j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is functional Element of bool the carrier of (TOP-REAL 2)
UBD C is functional Element of bool the carrier of (TOP-REAL 2)
C is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
n is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
Rotate (n,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
len n is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n /. 1 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n /. f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
G is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
Rotate (G,(n /. 1)) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
C is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
LeftComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
L~ C is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
UBD (L~ C) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
N-min (L~ C) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
Rotate (C,(N-min (L~ C))) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
Rev (Rotate (C,(N-min (L~ C)))) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
L~ (Rotate (C,(N-min (L~ C)))) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
L~ (Rev (Rotate (C,(N-min (L~ C))))) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
UBD (L~ (Rev (Rotate (C,(N-min (L~ C)))))) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LeftComp (Rev (Rotate (C,(N-min (L~ C))))) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
RightComp (Rotate (C,(N-min (L~ C)))) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
RightComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
C is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
LeftComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (LeftComp C) is functional Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp C)) ` is functional Element of bool the carrier of (TOP-REAL 2)
RightComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp C)) \/ (RightComp C) is functional Element of bool the carrier of (TOP-REAL 2)
L~ C is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(L~ C) \/ (LeftComp C) is functional Element of bool the carrier of (TOP-REAL 2)
((L~ C) \/ (LeftComp C)) \/ (RightComp C) is functional Element of bool the carrier of (TOP-REAL 2)
(L~ C) \/ (RightComp C) is functional Element of bool the carrier of (TOP-REAL 2)
((L~ C) \/ (RightComp C)) \/ (LeftComp C) is functional Element of bool the carrier of (TOP-REAL 2)
(LeftComp C) \/ (L~ C) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard finite-support FinSequence of the carrier of (TOP-REAL 2)
RightComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (RightComp C) is functional Element of bool the carrier of (TOP-REAL 2)
(Cl (RightComp C)) ` is functional Element of bool the carrier of (TOP-REAL 2)
LeftComp C is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(Cl (RightComp C)) \/ (LeftComp C) is functional Element of bool the carrier of (TOP-REAL 2)
L~ C is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(L~ C) \/ (RightComp C) is functional Element of bool the carrier of (TOP-REAL 2)
((L~ C) \/ (RightComp C)) \/ (LeftComp C) is functional Element of bool the carrier of (TOP-REAL 2)
(RightComp C) \/ (L~ C) is functional Element of bool the carrier of (TOP-REAL 2)
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Cage (n,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
GoB (Cage (n,C)) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Gauge (n,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
L~ (Cage (n,C)) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
S-max (L~ (Cage (n,C))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
rng (Cage (n,C)) is non empty non trivial functional finite non empty-membered closed bounded compact Element of bool the carrier of (TOP-REAL 2)
E-max (L~ (Cage (n,C))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
width (Gauge (n,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
W-min (L~ (Cage (n,C))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * (1,G) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
N-min (L~ (Cage (n,C))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * ((len (Gauge (n,C))),f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[(len (Gauge (n,C))),f] is set
{(len (Gauge (n,C))),f} is finite V32() V69() V70() V71() V72() V73() V74() set
{(len (Gauge (n,C)))} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(len (Gauge (n,C))),f},{(len (Gauge (n,C)))}} is finite V32() set
Indices (Gauge (n,C)) is set
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * (i1,1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,1] is set
{i1,1} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,1},{i1}} is finite V32() set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * (j2,(width (Gauge (n,C)))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j2,(width (Gauge (n,C)))] is set
{j2,(width (Gauge (n,C)))} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,(width (Gauge (n,C)))},{j2}} is finite V32() set
[1,G] is set
{1,G} is finite V32() V69() V70() V71() V72() V73() V74() set
{1} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{1,G},{1}} is finite V32() set
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
N-min n is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
Cage (n,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
right_cell ((Cage (n,C)),1) is functional Element of bool the carrier of (TOP-REAL 2)
Gauge (n,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Cage (n,C)) /. 1 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
width (Gauge (n,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Cage (n,C)) /. 2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(width (Gauge (n,C))) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * (G,(width (Gauge (n,C)))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(Gauge (n,C)) * ((G + 1),(width (Gauge (n,C)))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
cell ((Gauge (n,C)),G,((width (Gauge (n,C))) -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
(Gauge (n,C)) * (G,((width (Gauge (n,C))) -' 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
GoB (Cage (n,C)) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (GoB (Cage (n,C))) is set
1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Cage (n,C)) /. (1 + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[f,i1] is set
{f,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{f} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{f,i1},{f}} is finite V32() set
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j2] is set
{j2,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j2},{j2}} is finite V32() set
(GoB (Cage (n,C))) * (f,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
(GoB (Cage (n,C))) * (j2,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (n,C))),f,i1) is functional Element of bool the carrier of (TOP-REAL 2)
f + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (n,C))),f,(i1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (n,C))),j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (n,C))),(f -' 1),j2) is functional Element of bool the carrier of (TOP-REAL 2)
[(G + 1),(width (Gauge (n,C)))] is set
{(G + 1),(width (Gauge (n,C)))} is finite V32() V69() V70() V71() V72() V73() V74() set
{(G + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(G + 1),(width (Gauge (n,C)))},{(G + 1)}} is finite V32() set
Indices (Gauge (n,C)) is set
[G,(width (Gauge (n,C)))] is set
{G,(width (Gauge (n,C)))} is finite V32() V69() V70() V71() V72() V73() V74() set
{G} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{G,(width (Gauge (n,C)))},{G}} is finite V32() set
len (Cage (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Cage (G,n) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
L~ (Cage (G,n)) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Cage (G,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
Gauge (G,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
GoB (Cage (G,C)) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Gauge (G,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
f is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
len (Cage (G,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
LSeg ((Cage (G,n)),i1) is functional Element of bool the carrier of (TOP-REAL 2)
GoB (Cage (G,n)) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
right_cell ((Cage (G,n)),i1,(Gauge (G,n))) is functional Element of bool the carrier of (TOP-REAL 2)
right_cell ((Cage (G,n)),i1) is functional Element of bool the carrier of (TOP-REAL 2)
len (Gauge (G,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (G,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
dom (Cage (G,n)) is non empty non trivial finite non empty-membered V69() V70() V71() V72() V73() V74() Element of bool NAT
Indices (Gauge (G,n)) is set
(Cage (G,n)) /. i1 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j4 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,j4] is set
{j2,j4} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,j4},{j2}} is finite V32() set
(Gauge (G,n)) * (j2,j4) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
width (Gauge (G,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Gauge (G,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Cage (G,n)) /. (i1 + 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i5 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j5 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i5,j5] is set
{i5,j5} is finite V32() V69() V70() V71() V72() V73() V74() set
{i5} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i5,j5},{i5}} is finite V32() set
(Gauge (G,n)) * (i5,j5) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j4 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (G,n))),j2,j4) is functional Element of bool the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j4 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (G,n))),j2,(j4 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
i5 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (G,n))),i5,j5) is functional Element of bool the carrier of (TOP-REAL 2)
j5 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((GoB (Cage (G,n))),(j2 -' 1),j5) is functional Element of bool the carrier of (TOP-REAL 2)
j2 - i5 is V11() real integer ext-real Element of REAL
abs (j2 - i5) is V11() real ext-real Element of REAL
j4 - j5 is V11() real integer ext-real Element of REAL
abs (j4 - j5) is V11() real ext-real Element of REAL
(abs (j2 - i5)) + (abs (j4 - j5)) is V11() real ext-real Element of REAL
1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j4 -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j2 -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (G,C)),j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (G,C)),j2,j2) is functional Element of bool the carrier of (TOP-REAL 2)
Int (right_cell ((Cage (G,n)),i1)) is functional Element of bool the carrier of (TOP-REAL 2)
Int (cell ((Gauge (G,C)),j2,j2)) is functional Element of bool the carrier of (TOP-REAL 2)
L~ (Cage (G,C)) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(L~ (Cage (G,C))) ` is functional Element of bool the carrier of (TOP-REAL 2)
LeftComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (LeftComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp (Cage (G,C)))) \/ (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
(L~ (Cage (G,C))) \/ (LeftComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
((L~ (Cage (G,C))) \/ (LeftComp (Cage (G,C)))) \/ (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
(L~ (Cage (G,C))) \/ (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
((L~ (Cage (G,C))) \/ (RightComp (Cage (G,C)))) \/ (LeftComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
Cl (Int (cell ((Gauge (G,C)),j2,j2))) is functional Element of bool the carrier of (TOP-REAL 2)
Cl (Int (right_cell ((Cage (G,n)),i1))) is functional Element of bool the carrier of (TOP-REAL 2)
(LeftComp (Cage (G,C))) \/ (L~ (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
j2 is functional Element of bool the carrier of (TOP-REAL 2)
(LeftComp (Cage (G,C))) \/ (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Cage (G,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cage (G,n) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
LeftComp (Cage (G,n)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(Cage (G,n)) /. 1 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
L~ (Cage (G,n)) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
N-min (L~ (Cage (G,n))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
L~ (Cage (G,C)) is non empty functional closed boundary bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
E-bound (L~ (Cage (G,C))) is V11() real ext-real Element of REAL
E-bound (L~ (Cage (G,n))) is V11() real ext-real Element of REAL
(E-bound (L~ (Cage (G,C)))) + 1 is V11() real ext-real Element of REAL
|[((E-bound (L~ (Cage (G,C)))) + 1),0]| is non empty Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
RightComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
|[((E-bound (L~ (Cage (G,C)))) + 1),0]| `1 is V11() real ext-real Element of REAL
|[((E-bound (L~ (Cage (G,C)))) + 1),0]| . 1 is V11() real ext-real Element of REAL
(Cage (G,C)) /. 1 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
N-min (L~ (Cage (G,C))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
Cl (RightComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
(RightComp (Cage (G,C))) \/ (L~ (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
(L~ (Cage (G,n))) ` is functional Element of bool the carrier of (TOP-REAL 2)
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
Cage (G,n) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (G,n)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cage (G,C) is non empty non trivial Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non constant finite FinSequence-like FinSubsequence-like non empty-membered Function-yielding V81() circular special unfolded s.c.c. standard clockwise_oriented finite-support FinSequence of the carrier of (TOP-REAL 2)
RightComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
LeftComp (Cage (G,C)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (LeftComp (Cage (G,C))) is functional Element of bool the carrier of (TOP-REAL 2)
LeftComp (Cage (G,n)) is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
Cl (LeftComp (Cage (G,n))) is functional Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp (Cage (G,C)))) ` is functional Element of bool the carrier of (TOP-REAL 2)
(Cl (LeftComp (Cage (G,n)))) ` is functional Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (n -' 1) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ (n -' 1)) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(n,C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (C -' 1) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ (C -' 1)) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (n,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
(n,C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (C -' 1) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ (C -' 1)) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n,C) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (n,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
((n,C) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
n is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
2 |^ 0 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (n,C) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
width (Gauge (n,C)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n,C) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (C -' 1) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ (C -' 1)) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n,C) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
BDD n is functional open Element of bool the carrier of (TOP-REAL 2)
G is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (n,C)),((n,C) -' 1),G) is functional Element of bool the carrier of (TOP-REAL 2)
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (n,C)),((n,C) -' 1),0) is functional Element of bool the carrier of (TOP-REAL 2)
UBD n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
UBD n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
n ` is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (n,C)),((n,C) -' 1),1) is functional Element of bool the carrier of (TOP-REAL 2)
0 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (n,C)),((n,C) -' 1),0) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (n,C)),((n,C) -' 1),(0 + 1)) is functional Element of bool the carrier of (TOP-REAL 2)
(cell ((Gauge (n,C)),((n,C) -' 1),0)) /\ (cell ((Gauge (n,C)),((n,C) -' 1),(0 + 1))) is functional Element of bool the carrier of (TOP-REAL 2)
(Gauge (n,C)) * (((n,C) -' 1),(0 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((n,C) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * ((((n,C) -' 1) + 1),(0 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (((n,C) -' 1),(0 + 1))),((Gauge (n,C)) * ((((n,C) -' 1) + 1),(0 + 1)))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * ((Gauge (n,C)) * (((n,C) -' 1),(0 + 1)))) + (b1 * ((Gauge (n,C)) * ((((n,C) -' 1) + 1),(0 + 1))))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
2 |^ C is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ C) + 3 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
3 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
G + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Gauge (n,C)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (n,C)),((n,C) -' 1),(width (Gauge (n,C)))) is functional Element of bool the carrier of (TOP-REAL 2)
UBD n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
(width (Gauge (n,C))) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (n,C)),((n,C) -' 1),((width (Gauge (n,C))) -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
n ` is functional Element of bool the carrier of (TOP-REAL 2)
(width (Gauge (n,C))) - 1 is V11() real integer ext-real Element of REAL
UBD n is non empty functional open connected V199( TOP-REAL 2) Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (n,C)),((n,C) -' 1),(width (Gauge (n,C)))) is functional Element of bool the carrier of (TOP-REAL 2)
((width (Gauge (n,C))) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(cell ((Gauge (n,C)),((n,C) -' 1),(width (Gauge (n,C))))) /\ (cell ((Gauge (n,C)),((n,C) -' 1),((width (Gauge (n,C))) -' 1))) is functional Element of bool the carrier of (TOP-REAL 2)
(Gauge (n,C)) * (((n,C) -' 1),(width (Gauge (n,C)))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((n,C) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(Gauge (n,C)) * ((((n,C) -' 1) + 1),(width (Gauge (n,C)))) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
LSeg (((Gauge (n,C)) * (((n,C) -' 1),(width (Gauge (n,C))))),((Gauge (n,C)) * ((((n,C) -' 1) + 1),(width (Gauge (n,C)))))) is non empty functional closed closed boundary connected bounded bounded compact compact convex Element of bool the carrier of (TOP-REAL 2)
{ (((1 - b1) * ((Gauge (n,C)) * (((n,C) -' 1),(width (Gauge (n,C)))))) + (b1 * ((Gauge (n,C)) * ((((n,C) -' 1) + 1),(width (Gauge (n,C))))))) where b1 is V11() real ext-real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
(n,0) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
0 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
2 |^ (0 -' 1) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(2 |^ (0 -' 1)) + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n,0) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(n,0) - 1 is V11() real integer ext-real Element of REAL
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 -' 1),(j2 + 1)] is set
{(i1 -' 1),(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 -' 1)} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{(i1 -' 1),(j2 + 1)},{(i1 -' 1)}} is finite V32() set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(1 -' 1),j2) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),0,j2) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),j2] is set
{(i1 + 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),j2},{(i1 + 1)}} is finite V32() set
(Gauge (C,n)) * ((i1 + 1),j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),(j2 + 1)] is set
{(i1 + 1),(j2 + 1)} is finite V32() with_non-empty_elements V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),(j2 + 1)},{(i1 + 1)}} is finite V32() set
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),i1,(len (Gauge (C,n)))) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(j2 + 1),i1] is set
{(j2 + 1),i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{(j2 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(j2 + 1),i1},{(j2 + 1)}} is finite V32() set
(Gauge (C,n)) * ((j2 + 1),i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j2,i1] is set
{j2,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,i1},{j2}} is finite V32() set
(Gauge (C,n)) * (j2,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,(i1 -' 1)] is set
{j2,(i1 -' 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{j2,(i1 -' 1)},{j2}} is finite V32() set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),j2,(1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),j2,0) is functional Element of bool the carrier of (TOP-REAL 2)
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),j2] is set
{(i1 + 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),j2},{(i1 + 1)}} is finite V32() set
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(len (Gauge (C,n))),j2) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 2)] is set
{i1,(j2 + 2)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 2)},{i1}} is finite V32() set
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(j2 + 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(i1 -' 1),(len (Gauge (C,n)))) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),j2] is set
{(i1 + 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),j2},{(i1 + 1)}} is finite V32() set
(Gauge (C,n)) * ((i1 + 1),j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 2 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 2),j2] is set
{(i1 + 2),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 + 2)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 2),j2},{(i1 + 2)}} is finite V32() set
(i1 + 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(len (Gauge (C,n))),j2) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(j2 + 1),i1] is set
{(j2 + 1),i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{(j2 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(j2 + 1),i1},{(j2 + 1)}} is finite V32() set
(Gauge (C,n)) * ((j2 + 1),i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j2,i1] is set
{j2,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,i1},{j2}} is finite V32() set
(Gauge (C,n)) * (j2,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(j2 -' 1),i1] is set
{(j2 -' 1),i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{(j2 -' 1)} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{(j2 -' 1),i1},{(j2 -' 1)}} is finite V32() set
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(1 -' 1),(i1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),0,(i1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_left_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 -' 1)] is set
{i1,(j2 -' 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,(j2 -' 1)},{i1}} is finite V32() set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),i1,(1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),i1,0) is functional Element of bool the carrier of (TOP-REAL 2)
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_right_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),(j2 + 1)] is set
{(i1 + 1),(j2 + 1)} is finite V32() with_non-empty_elements V69() V70() V71() V72() V73() V74() set
{(i1 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),(j2 + 1)},{(i1 + 1)}} is finite V32() set
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(len (Gauge (C,n))),(j2 + 1)) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_right_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),j2] is set
{(i1 + 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),j2},{(i1 + 1)}} is finite V32() set
(Gauge (C,n)) * ((i1 + 1),j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 + 1),(j2 -' 1)] is set
{(i1 + 1),(j2 -' 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{(i1 + 1),(j2 -' 1)},{(i1 + 1)}} is finite V32() set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(i1 + 1),(1 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),(i1 + 1),0) is functional Element of bool the carrier of (TOP-REAL 2)
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_right_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(j2 + 1),i1] is set
{(j2 + 1),i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{(j2 + 1)} is non empty trivial finite V32() 1 -element with_non-empty_elements non empty-membered V69() V70() V71() V72() V73() V74() set
{{(j2 + 1),i1},{(j2 + 1)}} is finite V32() set
(Gauge (C,n)) * ((j2 + 1),i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[j2,i1] is set
{j2,i1} is finite V32() V69() V70() V71() V72() V73() V74() set
{j2} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{j2,i1},{j2}} is finite V32() set
(Gauge (C,n)) * (j2,i1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[j2,(i1 + 1)] is set
{j2,(i1 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{{j2,(i1 + 1)},{j2}} is finite V32() set
(len (Gauge (C,n))) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(j2 -' 1),(len (Gauge (C,n)))) is functional Element of bool the carrier of (TOP-REAL 2)
C is non empty functional closed bounded compact non horizontal non vertical Element of bool the carrier of (TOP-REAL 2)
n is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
Gauge (C,n) is non empty Relation-like non-empty non empty-yielding NAT -defined the carrier of (TOP-REAL 2) * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence-yielding finite-support FinSequence of the carrier of (TOP-REAL 2) *
Indices (Gauge (C,n)) is set
len (Gauge (C,n)) is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
width (Gauge (C,n)) is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
f is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V81() finite-support FinSequence of the carrier of (TOP-REAL 2)
len f is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
(len f) -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
front_right_cell (f,((len f) -' 1),(Gauge (C,n))) is functional Element of bool the carrier of (TOP-REAL 2)
f /. ((len f) -' 1) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
f /. (len f) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
((len f) -' 1) + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
i1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 + 1 is non empty ordinal natural V11() real integer finite cardinal ext-real positive non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[i1,(j2 + 1)] is set
{i1,(j2 + 1)} is finite V32() V69() V70() V71() V72() V73() V74() set
{i1} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{i1,(j2 + 1)},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,(j2 + 1)) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
[i1,j2] is set
{i1,j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{{i1,j2},{i1}} is finite V32() set
(Gauge (C,n)) * (i1,j2) is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like V59() V60() V61() finite-support Element of the carrier of (TOP-REAL 2)
i1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
[(i1 -' 1),j2] is set
{(i1 -' 1),j2} is finite V32() V69() V70() V71() V72() V73() V74() set
{(i1 -' 1)} is non empty trivial finite V32() 1 -element V69() V70() V71() V72() V73() V74() set
{{(i1 -' 1),j2},{(i1 -' 1)}} is finite V32() set
1 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
j2 -' 1 is ordinal natural V11() real integer finite cardinal ext-real non negative V46() V69() V70() V71() V72() V73() V74() Element of NAT
cell ((Gauge (C,n)),(1 -' 1),(j2 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)
cell ((Gauge (C,n)),0,(j2 -' 1)) is functional Element of bool the carrier of (TOP-REAL 2)