:: GOBOARD9 semantic presentation

REAL is non empty V26() V92() V93() V94() V98() set
NAT is non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() Element of K6(REAL)
K6(REAL) is set
NAT is non empty V4() V5() V6() V92() V93() V94() V95() V96() V97() V98() set
K6(NAT) is set
K6(NAT) is set
COMPLEX is non empty V26() V92() V98() set
RAT is non empty V26() V92() V93() V94() V95() V98() set
INT is non empty V26() V92() V93() V94() V95() V96() V98() set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
K7(1,1) is set
K6(K7(1,1)) is set
K7(K7(1,1),1) is set
K6(K7(K7(1,1),1)) is set
K7(K7(1,1),REAL) is set
K6(K7(K7(1,1),REAL)) is set
K7(REAL,REAL) is set
K7(K7(REAL,REAL),REAL) is set
K6(K7(K7(REAL,REAL),REAL)) is set
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
K7(2,2) is set
K7(K7(2,2),REAL) is set
K6(K7(K7(2,2),REAL)) is set
K6(K7(REAL,REAL)) is set
TOP-REAL 2 is non empty TopSpace-like V130() V155() V156() V157() V158() V159() V160() V161() strict RLTopStruct
the carrier of (TOP-REAL 2) is non empty set
K247( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the carrier of (TOP-REAL 2))
K6( the carrier of (TOP-REAL 2)) is set
K7(COMPLEX,COMPLEX) is set
K6(K7(COMPLEX,COMPLEX)) is set
K7(COMPLEX,REAL) is set
K6(K7(COMPLEX,REAL)) is set
{} is set
the empty V4() V5() V6() V8() V9() V10() functional FinSequence-membered ext-real non positive non negative V92() V93() V94() V95() V96() V97() V98() set is empty V4() V5() V6() V8() V9() V10() functional FinSequence-membered ext-real non positive non negative V92() V93() V94() V95() V96() V97() V98() set
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
1 / 2 is V11() V12() ext-real Element of REAL
|[0,1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
|[1,0]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
|[1,1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
- 1 is V11() V12() ext-real Element of REAL
|[(- 1),1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
|[1,(- 1)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
4 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
1 / 2 is V11() Element of COMPLEX
K38(1) is V11() set
|[1,K38(1)]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
|[K38(1),1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
Seg 1 is non empty V26() 1 -element V92() V93() V94() V95() V96() V97() Element of K6(NAT)
{1} is V92() V93() V94() V95() V96() V97() set
Seg 2 is non empty V26() 2 -element V92() V93() V94() V95() V96() V97() Element of K6(NAT)
{1,2} is V92() V93() V94() V95() V96() V97() set
f is TopSpace-like TopStruct
the carrier of f is set
K6( the carrier of f) is set
j0 is Element of K6( the carrier of f)
k is Element of K6( the carrier of f)
i0 is Element of K6( the carrier of f)
f | j0 is strict TopSpace-like SubSpace of f
the carrier of (f | j0) is set
K6( the carrier of (f | j0)) is set
i1 is Element of K6( the carrier of (f | j0))
j1 is Element of K6( the carrier of (f | j0))
f is TopSpace-like TopStruct
the carrier of f is set
K6( the carrier of f) is set
i0 is Element of K6( the carrier of f)
f | i0 is strict TopSpace-like SubSpace of f
the carrier of (f | i0) is set
K6( the carrier of (f | i0)) is set
k is Element of K6( the carrier of f)
f | k is strict TopSpace-like SubSpace of f
j0 is Element of K6( the carrier of (f | i0))
(f | i0) | j0 is strict TopSpace-like SubSpace of f | i0
the carrier of (f | k) is set
[#] (f | k) is non proper V59(f | k) Element of K6( the carrier of (f | k))
K6( the carrier of (f | k)) is set
i1 is strict TopSpace-like SubSpace of f | i0
[#] i1 is non proper V59(i1) Element of K6( the carrier of i1)
the carrier of i1 is set
K6( the carrier of i1) is set
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K6( the carrier of f) is set
k is non empty Element of K6( the carrier of f)
i0 is non empty Element of K6( the carrier of f)
j0 is set
f | i0 is non empty strict TopSpace-like SubSpace of f
[#] (f | i0) is non empty non proper V59(f | i0) Element of K6( the carrier of (f | i0))
the carrier of (f | i0) is non empty set
K6( the carrier of (f | i0)) is set
i1 is Element of the carrier of (f | i0)
Component_of i1 is Element of K6( the carrier of (f | i0))
j1 is Element of K6( the carrier of f)
f | k is non empty strict TopSpace-like SubSpace of f
i2 is Element of K6( the carrier of (f | i0))
(f | i0) | i2 is strict TopSpace-like SubSpace of f | i0
i2 /\ (Component_of i1) is Element of K6( the carrier of (f | i0))
{} (f | i0) is empty V4() V5() V6() V8() V9() V10() functional FinSequence-membered V59(f | i0) ext-real non positive non negative V92() V93() V94() V95() V96() V97() V98() Element of K6( the carrier of (f | i0))
f is non empty TopSpace-like TopStruct
the carrier of f is non empty set
K6( the carrier of f) is set
i0 is Element of K6( the carrier of f)
i1 is Element of K6( the carrier of f)
j0 is Element of K6( the carrier of f)
k is Element of K6( the carrier of f)
i19 is non empty Element of K6( the carrier of f)
i2 is non empty Element of K6( the carrier of f)
i09 is Element of K6( the carrier of f)
j1 is non empty Element of K6( the carrier of f)
f | i19 is non empty strict TopSpace-like SubSpace of f
the carrier of (f | i19) is non empty set
K6( the carrier of (f | i19)) is set
j2 is non empty Element of K6( the carrier of f)
i29 is Element of K6( the carrier of (f | i19))
j19 is Element of K6( the carrier of (f | i19))
the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2), the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f is connected convex Element of K6( the carrier of (TOP-REAL 2))
k is connected convex Element of K6( the carrier of (TOP-REAL 2))
f /\ k is Element of K6( the carrier of (TOP-REAL 2))
i0 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
j0 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (i0,j0) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis f is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev (X_axis f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
X_axis (Rev f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
len (Rev (X_axis f)) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (X_axis f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (Rev f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom (X_axis f) is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom (Rev (X_axis f)) is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
(len f) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) + 1) -' k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) + 1) -' k) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
Rev (Rev (X_axis f)) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
(Rev (X_axis f)) . k is set
(Rev (X_axis f)) /. k is V11() V12() ext-real Element of REAL
(X_axis f) /. (((len f) + 1) -' k) is V11() V12() ext-real Element of REAL
(X_axis f) . (((len f) + 1) -' k) is set
f /. (((len f) + 1) -' k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(f /. (((len f) + 1) -' k)) `1 is V11() V12() ext-real Element of REAL
(Rev f) /. k is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((Rev f) /. k) `1 is V11() V12() ext-real Element of REAL
f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Y_axis f is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev (Y_axis f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev f is V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Y_axis (Rev f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
len (Rev (Y_axis f)) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (Y_axis f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (Rev f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom (Y_axis f) is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom (Rev (Y_axis f)) is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
(len f) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) + 1) -' k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) + 1) -' k) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
Rev (Rev (Y_axis f)) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
(Rev (Y_axis f)) . k is set
(Rev (Y_axis f)) /. k is V11() V12() ext-real Element of REAL
(Y_axis f) /. (((len f) + 1) -' k) is V11() V12() ext-real Element of REAL
(Y_axis f) . (((len f) + 1) -' k) is set
f /. (((len f) + 1) -' k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(f /. (((len f) + 1) -' k)) `2 is V11() V12() ext-real Element of REAL
(Rev f) /. k is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((Rev f) /. k) `2 is V11() V12() ext-real Element of REAL
k is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
GoB k is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
X_axis f is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev (X_axis f) is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
X_axis k is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (X_axis k) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like V84() FinSequence of REAL
rng (Incr (X_axis k)) is set
rng (X_axis k) is set
rng (X_axis f) is set
len (Incr (X_axis k)) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
card (rng (X_axis k)) is cardinal set
card (rng (X_axis f)) is cardinal set
Incr (X_axis f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like V84() FinSequence of REAL
Y_axis f is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Rev (Y_axis f) is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis k is non empty V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of REAL
Incr (Y_axis k) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like V84() FinSequence of REAL
rng (Incr (Y_axis k)) is set
rng (Y_axis k) is set
rng (Y_axis f) is set
len (Incr (Y_axis k)) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
card (rng (Y_axis k)) is cardinal set
card (rng (Y_axis f)) is cardinal set
Incr (Y_axis f) is V13() V16( NAT ) V17( REAL ) Function-like V26() FinSequence-like FinSubsequence-like V84() FinSequence of REAL
GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is V13() V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular FinSequence of K247( the carrier of (TOP-REAL 2))
<*1,2*> is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like set
dom <*1,2*> is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
<*1,2*> . 1 is set
<*1,2*> . 2 is set
f is V13() V16( NAT ) Function-like non constant V26() FinSequence-like FinSubsequence-like set
Rev f is V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f . k is set
f . i0 is set
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) - k is V11() V12() ext-real Element of REAL
(len f) - i0 is V11() V12() ext-real Element of REAL
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom (Rev f) is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
(Rev f) . j1 is set
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(Rev f) . i2 is set
j1 + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) - j1 is V11() V12() ext-real Element of REAL
((len f) - j1) + 1 is V11() V12() ext-real Element of REAL
f . (((len f) - j1) + 1) is set
0 + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f . (0 + k) is set
i2 + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) - i2 is V11() V12() ext-real Element of REAL
((len f) - i2) + 1 is V11() V12() ext-real Element of REAL
f . (((len f) - i2) + 1) is set
0 + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f . (0 + i0) is set
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
Rev f is non empty V13() V16( NAT ) Function-like V26() FinSequence-like FinSubsequence-like set
Rev f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
k is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
Rev k is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like V26() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
GoB k is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom k is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
(len f) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) + 1) -' i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) + 1) -' i0) + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
Indices (GoB f) is set
f /. (((len f) + 1) -' i0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i1,j1] is set
{i1,j1} is V92() V93() V94() V95() V96() V97() set
{i1} is V92() V93() V94() V95() V96() V97() set
{{i1,j1},{i1}} is set
(GoB f) * (i1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i2,j2] is set
{i2,j2} is V92() V93() V94() V95() V96() V97() set
{i2} is V92() V93() V94() V95() V96() V97() set
{{i2,j2},{i2}} is set
Indices (GoB k) is set
k /. i0 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB k) * (i2,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k /. i0 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
k /. (i0 + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((len f) + 1) -' (i0 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) + 1) -' (i0 + 1)) + (i0 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) + 1) -' (i0 + 1)) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((((len f) + 1) -' (i0 + 1)) + 1) + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i1,j1] is set
{i1,j1} is V92() V93() V94() V95() V96() V97() set
{i1} is V92() V93() V94() V95() V96() V97() set
{{i1,j1},{i1}} is set
(GoB k) * (i1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
K40(i1,i2) is set
abs K40(i1,i2) is V11() V12() ext-real Element of REAL
j2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i2,j2] is set
{i2,j2} is V92() V93() V94() V95() V96() V97() set
{i2} is V92() V93() V94() V95() V96() V97() set
{{i2,j2},{i2}} is set
(GoB k) * (i2,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
K40(j1,j2) is set
abs K40(j1,j2) is V11() V12() ext-real Element of REAL
K36((abs K40(i1,i2)),(abs K40(j1,j2))) is set
i2 - i1 is V11() V12() ext-real Element of REAL
abs (i2 - i1) is V11() V12() ext-real Element of REAL
i1 - i2 is V11() V12() ext-real Element of REAL
- (i1 - i2) is V11() V12() ext-real Element of REAL
abs (- (i1 - i2)) is V11() V12() ext-real Element of REAL
abs (i1 - i2) is V11() V12() ext-real Element of REAL
j2 - j1 is V11() V12() ext-real Element of REAL
abs (j2 - j1) is V11() V12() ext-real Element of REAL
j1 - j2 is V11() V12() ext-real Element of REAL
- (j1 - j2) is V11() V12() ext-real Element of REAL
abs (- (j1 - j2)) is V11() V12() ext-real Element of REAL
abs (j1 - j2) is V11() V12() ext-real Element of REAL
f /. (((len f) + 1) -' (i0 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. ((((len f) + 1) -' (i0 + 1)) + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(abs (i1 - i2)) + (abs (j1 - j2)) is V11() V12() ext-real Element of REAL
k /. 1 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. (len f) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. 1 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
k /. (len k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
LSeg (k,i0) is Element of K6( the carrier of (TOP-REAL 2))
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
LSeg (k,j0) is Element of K6( the carrier of (TOP-REAL 2))
(len f) -' i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) -' j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' j0) + j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' i0) + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i0 + 1) + ((len f) -' i0) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' j0) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(((len f) -' j0) + 1) + j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + ((len f) -' i0) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' i0) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
LSeg (f,((len f) -' i0)) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,((len f) -' j0)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,((len f) -' i0))) /\ (LSeg (f,((len f) -' j0))) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (k,i0)) /\ (LSeg (k,j0)) is Element of K6( the carrier of (TOP-REAL 2))
((len f) -' i0) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
LSeg (f,((len f) -' i0)) is Element of K6( the carrier of (TOP-REAL 2))
LSeg (f,((len f) -' j0)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (f,((len f) -' i0))) /\ (LSeg (f,((len f) -' j0))) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (k,i0)) /\ (LSeg (k,j0)) is Element of K6( the carrier of (TOP-REAL 2))
(LSeg (k,i0)) /\ (LSeg (k,j0)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell ((f),i0) is Element of K6( the carrier of (TOP-REAL 2))
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
GoB (f) is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[j0,i1] is set
{j0,i1} is V92() V93() V94() V95() V96() V97() set
{j0} is V92() V93() V94() V95() V96() V97() set
{{j0,i1},{j0}} is set
Indices (GoB f) is set
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[j1,i2] is set
{j1,i2} is V92() V93() V94() V95() V96() V97() set
{j1} is V92() V93() V94() V95() V96() V97() set
{{j1,i2},{j1}} is set
f /. k is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (j0,i1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. (k + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (j1,i2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
(k + 1) + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) /. i0 is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 + 1) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) /. (i0 + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
j0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j0 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i1 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 - j1 is V11() V12() ext-real Element of REAL
abs (j0 - j1) is V11() V12() ext-real Element of REAL
i1 - i2 is V11() V12() ext-real Element of REAL
abs (i1 - i2) is V11() V12() ext-real Element of REAL
(abs (j0 - j1)) + (abs (i1 - i2)) is V11() V12() ext-real Element of REAL
j2 is V11() V12() ext-real Element of REAL
i19 is V11() V12() ext-real Element of REAL
j2 - i19 is V11() V12() ext-real Element of REAL
abs (j2 - i19) is V11() V12() ext-real Element of REAL
i09 is V11() V12() ext-real Element of REAL
i29 is V11() V12() ext-real Element of REAL
i09 - i29 is V11() V12() ext-real Element of REAL
abs (i09 - i29) is V11() V12() ext-real Element of REAL
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),(j0 -' 1),i1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(j0 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(j0 -' 1))) /\ (h_strip ((GoB f),i1)) is Element of K6( the carrier of (TOP-REAL 2))
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),j0,i1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),j0)) /\ (h_strip ((GoB f),i1)) is Element of K6( the carrier of (TOP-REAL 2))
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i2 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),j1,(i2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(i2 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),j1)) /\ (h_strip ((GoB f),(i2 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),j0,i2) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),j0)) /\ (h_strip ((GoB f),i2)) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell ((f),k) is Element of K6( the carrier of (TOP-REAL 2))
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell (f,i0) is Element of K6( the carrier of (TOP-REAL 2))
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((f)) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
Indices (GoB f) is set
f /. k is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i0,j0] is set
{i0,j0} is V92() V93() V94() V95() V96() V97() set
{i0} is V92() V93() V94() V95() V96() V97() set
{{i0,j0},{i0}} is set
(GoB f) * (i0,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. (k + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i1,j1] is set
{i1,j1} is V92() V93() V94() V95() V96() V97() set
{i1} is V92() V93() V94() V95() V96() V97() set
{{i1,j1},{i1}} is set
(GoB f) * (i1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i0 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j0 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 - i1 is V11() V12() ext-real Element of REAL
abs (i0 - i1) is V11() V12() ext-real Element of REAL
j0 - j1 is V11() V12() ext-real Element of REAL
abs (j0 - j1) is V11() V12() ext-real Element of REAL
(abs (i0 - i1)) + (abs (j0 - j1)) is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
j2 is V11() V12() ext-real Element of REAL
i2 - j2 is V11() V12() ext-real Element of REAL
abs (i2 - j2) is V11() V12() ext-real Element of REAL
i19 is V11() V12() ext-real Element of REAL
i09 is V11() V12() ext-real Element of REAL
i19 - i09 is V11() V12() ext-real Element of REAL
abs (i19 - i09) is V11() V12() ext-real Element of REAL
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),(i0 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i0 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i0 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i0,j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i1,(j0 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j0 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j0 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
width k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
h_strip (k,f) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (k,f)) is Element of K6( the carrier of (TOP-REAL 2))
k * (1,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (1,1)) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not (k * (1,1)) `2 <= b₂ } is set
k * (1,(width k)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (1,(width k))) `2 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not b<sub>2</sub> <= (k * (1,(width k))) `2 } is set
k * (1,f) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (1,f)) `2 is V11() V12() ext-real Element of REAL
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k * (1,(f + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (1,(f + 1))) `2 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( not b₂ <= (k * (1,f)) `2 & not (k * (1,(f + 1))) `2 <= b₂ ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : not b₂ <= (k * (1,f)) `2 } is set
i0 is set
j0 is V11() V12() ext-real Element of REAL
i1 is V11() V12() ext-real Element of REAL
|[j0,i1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not (k * (1,(f + 1))) `2 <= b₂ } is set
i0 is set
j0 is V11() V12() ext-real Element of REAL
i1 is V11() V12() ext-real Element of REAL
|[j0,i1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is Element of K6( the carrier of (TOP-REAL 2))
j0 is Element of K6( the carrier of (TOP-REAL 2))
i0 /\ j0 is Element of K6( the carrier of (TOP-REAL 2))
i1 is set
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
i1 is set
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
j2 is V11() V12() ext-real Element of REAL
i19 is V11() V12() ext-real Element of REAL
|[j2,i19]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
v_strip (k,f) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (k,f)) is Element of K6( the carrier of (TOP-REAL 2))
k * (1,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (1,1)) `1 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not (k * (1,1)) `1 <= b₁ } is set
k * ((len k),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * ((len k),1)) `1 is V11() V12() ext-real Element of REAL
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not b<sub>1</sub> <= (k * ((len k),1)) `1 } is set
k * (f,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * (f,1)) `1 is V11() V12() ext-real Element of REAL
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k * ((f + 1),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(k * ((f + 1),1)) `1 is V11() V12() ext-real Element of REAL
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : ( not b₁ <= (k * (f,1)) `1 & not (k * ((f + 1),1)) `1 <= b₁ ) } is set
{ |[b₁,b₂]| where b₁, b₂ is V11() V12() ext-real Element of REAL : not b₁ <= (k * (f,1)) `1 } is set
i0 is set
j0 is V11() V12() ext-real Element of REAL
i1 is V11() V12() ext-real Element of REAL
|[j0,i1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
{ |[b<sub>1</sub>,b<sub>2</sub>]| where b<sub>1</sub>, b<sub>2</sub> is V11() V12() ext-real Element of REAL : not (k * ((f + 1),1)) `1 <= b₁ } is set
i0 is set
j0 is V11() V12() ext-real Element of REAL
i1 is V11() V12() ext-real Element of REAL
|[j0,i1]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is Element of K6( the carrier of (TOP-REAL 2))
j0 is Element of K6( the carrier of (TOP-REAL 2))
i0 /\ j0 is Element of K6( the carrier of (TOP-REAL 2))
i1 is set
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
i1 is set
j1 is V11() V12() ext-real Element of REAL
i2 is V11() V12() ext-real Element of REAL
|[j1,i2]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
j2 is V11() V12() ext-real Element of REAL
i19 is V11() V12() ext-real Element of REAL
|[j2,i19]| is non empty V13() V16( NAT ) Function-like V26() 2 -element FinSequence-like FinSubsequence-like V82() Element of the carrier of (TOP-REAL 2)
f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell (i0,f,k) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (i0,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (i0,k) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (i0,f)) /\ (h_strip (i0,k)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (i0,f,k)) is Element of K6( the carrier of (TOP-REAL 2))
the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * (f,k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,k)) + (i0 * ((f + 1),(k + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * ((i0 * (f,k)) + (i0 * ((f + 1),(k + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * ((i0 * (f,k)) + (i0 * ((f + 1),(k + 1))))), the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * (f,k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 * ((f + 1),k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,k)) + (i0 * ((f + 1),k)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * ((i0 * (f,k)) + (i0 * ((f + 1),k))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * ((i0 * (f,k)) + (i0 * ((f + 1),k)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),(((1 / 2) * ((i0 * (f,k)) + (i0 * ((f + 1),k)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * (f,(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,(k + 1))) + (i0 * ((f + 1),(k + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * ((i0 * (f,(k + 1))) + (i0 * ((f + 1),(k + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * ((i0 * (f,(k + 1))) + (i0 * ((f + 1),(k + 1))))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * ((i0 * (f,(k + 1))) + (i0 * ((f + 1),(k + 1))))) - |[0,1]|), the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * ((f + 1),k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * ((f + 1),k)) + (i0 * ((f + 1),(k + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * ((i0 * ((f + 1),k)) + (i0 * ((f + 1),(k + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * ((i0 * ((f + 1),k)) + (i0 * ((f + 1),(k + 1))))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * ((i0 * ((f + 1),k)) + (i0 * ((f + 1),(k + 1))))) - |[1,0]|), the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * (f,k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 * (f,(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,k)) + (i0 * (f,(k + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * ((i0 * (f,k)) + (i0 * (f,(k + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * ((i0 * (f,k)) + (i0 * (f,(k + 1))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),(((1 / 2) * ((i0 * (f,k)) + (i0 * (f,(k + 1))))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * ((f + 1),(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * ((f + 1),(k + 1))) - |[1,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),((i0 * ((f + 1),(k + 1))) - |[1,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
i0 * (f,k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,k)) + |[1,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),((i0 * (f,k)) + |[1,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * ((f + 1),k) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * ((f + 1),k)) + |[(- 1),1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),((i0 * ((f + 1),k)) + |[(- 1),1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 * (f,(k + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(i0 * (f,(k + 1))) + |[1,(- 1)]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ( the 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2),((i0 * (f,(k + 1))) + |[1,(- 1)]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
f + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i0,j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) -' k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell ((f),((len f) -' k)) is Element of K6( the carrier of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell (i0,f,k) is Element of K6( the carrier of (TOP-REAL 2))
v_strip (i0,f) is Element of K6( the carrier of (TOP-REAL 2))
h_strip (i0,k) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip (i0,f)) /\ (h_strip (i0,k)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell (i0,f,k)) is Element of K6( the carrier of (TOP-REAL 2))
Int (v_strip (i0,f)) is Element of K6( the carrier of (TOP-REAL 2))
Int (h_strip (i0,k)) is Element of K6( the carrier of (TOP-REAL 2))
(Int (v_strip (i0,f))) /\ (Int (h_strip (i0,k))) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i0,j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) -' k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell ((f),((len f) -' k)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,1) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,1)) is Element of K6( the carrier of (TOP-REAL 2))
right_cell (f,1) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,1)) is Element of K6( the carrier of (TOP-REAL 2))
L~ f is Element of K6( the carrier of (TOP-REAL 2))
(L~ f) ` is Element of K6( the carrier of (TOP-REAL 2))
k is Element of K6( the carrier of (TOP-REAL 2))
i0 is Element of K6( the carrier of (TOP-REAL 2))
k is Element of K6( the carrier of (TOP-REAL 2))
i0 is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) is Element of K6( the carrier of (TOP-REAL 2))
0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,0) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,0)) is Element of K6( the carrier of (TOP-REAL 2))
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
(k + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell (f,(k + 1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (left_cell (f,(k + 1))) is Element of K6( the carrier of (TOP-REAL 2))
dom f is V92() V93() V94() V95() V96() V97() Element of K6(NAT)
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
Indices (GoB f) is set
f /. k is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i0,j0] is set
{i0,j0} is V92() V93() V94() V95() V96() V97() set
{i0} is V92() V93() V94() V95() V96() V97() set
{{i0,j0},{i0}} is set
(GoB f) * (i0,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. (k + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i1,j1] is set
{i1,j1} is V92() V93() V94() V95() V96() V97() set
{i1} is V92() V93() V94() V95() V96() V97() set
{{i1,j1},{i1}} is set
(GoB f) * (i1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
f /. ((k + 1) + 1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
[i2,j2] is set
{i2,j2} is V92() V93() V94() V95() V96() V97() set
{i2} is V92() V93() V94() V95() V96() V97() set
{{i2,j2},{i2}} is set
(GoB f) * (i2,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 - i1 is V11() V12() ext-real Element of REAL
abs (i0 - i1) is V11() V12() ext-real Element of REAL
j0 - j1 is V11() V12() ext-real Element of REAL
abs (j0 - j1) is V11() V12() ext-real Element of REAL
(abs (i0 - i1)) + (abs (j0 - j1)) is V11() V12() ext-real Element of REAL
i09 is V11() V12() ext-real Element of REAL
i19 is V11() V12() ext-real Element of REAL
i09 - i19 is V11() V12() ext-real Element of REAL
abs (i09 - i19) is V11() V12() ext-real Element of REAL
j09 is V11() V12() ext-real Element of REAL
j19 is V11() V12() ext-real Element of REAL
j09 - j19 is V11() V12() ext-real Element of REAL
abs (j09 - j19) is V11() V12() ext-real Element of REAL
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 - i2 is V11() V12() ext-real Element of REAL
abs (i1 - i2) is V11() V12() ext-real Element of REAL
j1 - j2 is V11() V12() ext-real Element of REAL
abs (j1 - j2) is V11() V12() ext-real Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is V11() V12() ext-real Element of REAL
i29 is V11() V12() ext-real Element of REAL
i19 - i29 is V11() V12() ext-real Element of REAL
abs (i19 - i29) is V11() V12() ext-real Element of REAL
j29 is V11() V12() ext-real Element of REAL
j19 - j29 is V11() V12() ext-real Element of REAL
abs (j19 - j29) is V11() V12() ext-real Element of REAL
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i1 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i1 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j1 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j1 -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len (GoB f)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len (GoB f)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(width (GoB f)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((width (GoB f)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i0 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i0 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i2 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
i2 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j0 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j0 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j2 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
j2 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
L~ f is Element of K6( the carrier of (TOP-REAL 2))
(L~ f) ` is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,1)) + ((GoB f) * (i0,1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i2,1)) + ((GoB f) * (i1,1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * (i1,1)))) - |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
j0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),i2,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,(j0 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,(j0 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j0)))),((1 / 2) * (((GoB f) * (i2,(j0 -' 1))) + ((GoB f) * (i1,j0))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((len (GoB f)),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),1)) + ((GoB f) * ((len (GoB f)),2)))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (((len (GoB f)) -' 1),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (((len (GoB f)) -' 1),1)) + ((GoB f) * ((len (GoB f)),1)))) - |[0,1]|),(((GoB f) * ((len (GoB f)),1)) + |[1,(- 1)]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i0,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),(1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i1 + 1),2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,1)) + ((GoB f) * ((i0 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * ((i1 + 1),2))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),0)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i2,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i2 + 1),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i2 + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i2 + 2),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i2,1)) + ((GoB f) * ((i2 + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * ((i2 + 1),1)) + ((GoB f) * ((i2 + 2),1)))) - |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(j1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((len (GoB f)),(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),(j1 -' 1))) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i1 -' 1),(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * (i1,j1)))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(j1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (i0,(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i0,(j1 -' 1))) + ((GoB f) * ((i0 + 1),j1)))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i1,(j1 -' 1))) + ((GoB f) * ((i1 + 1),j1)))),((1 / 2) * (((GoB f) * (i2,(j1 -' 1))) + ((GoB f) * (i1,j1))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(len (GoB f)),j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(len (GoB f))) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(len (GoB f)))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(len (GoB f)),j2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(len (GoB f)))) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((len (GoB f)),j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
j2 + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((len (GoB f)),(j2 + 2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),(j2 + 1))))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),(j2 + 1))) + ((GoB f) * ((len (GoB f)),(j2 + 2))))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(len (GoB f)),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i0,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
j2 + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i1 + 1),(j2 + 2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i0,j2)) + ((GoB f) * ((i0 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * (i1,(j2 + 1))) + ((GoB f) * ((i1 + 1),(j2 + 2)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j0)) + |[1,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i1,j0)))) + |[0,1]|),(((GoB f) * (i1,j0)) + |[1,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + |[1,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i1,j2)) + ((GoB f) * (i1,j1)))) + |[1,0]|),(((GoB f) * (i1,j1)) + |[1,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i0 + 1),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
i0 + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i0 + 2),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),j0)))) + |[0,1]|),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i0 + 2),j0)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i0 + 1),j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),j0)))),(((1 / 2) * (((GoB f) * ((i0 + 1),j0)) + ((GoB f) * ((i1 + 1),j0)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i1,(j1 + 1))))),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,(j1 + 1))))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((len (GoB f)),j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((len (GoB f)),(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((len (GoB f)),j2)) + ((GoB f) * ((len (GoB f)),j1)))) + |[1,0]|),(((1 / 2) * (((GoB f) * ((len (GoB f)),j1)) + ((GoB f) * ((len (GoB f)),(j1 + 1))))) + |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i0,(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i0,(j2 + 1))) + ((GoB f) * ((i0 + 1),(j1 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j2) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j2)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i0 + 1),j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(j2 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i0 + 1),j2)) + ((GoB f) * ((i1 + 1),(j2 + 1))))),((1 / 2) * (((GoB f) * ((i0 + 1),(j2 + 1))) + ((GoB f) * ((i1 + 1),(j1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i2,j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i2) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i2)) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
((GoB f) * (i1,j1)) - |[1,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i0,j1)))) - |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((GoB f) * (i1,j1)) - |[1,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i1,j2)))) - |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
(i1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i1 -' 1),1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,1)) + ((GoB f) * (i0,1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),(((1 / 2) * (((GoB f) * (i1,1)) + ((GoB f) * (i0,1)))) - |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,1)))) - |[0,1]|),((1 / 2) * (((GoB f) * ((i1 -' 1),1)) + ((GoB f) * (i1,2))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
j0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j0 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (1,(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (1,((j1 -' 1) + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (2,((j1 -' 1) + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (2,((j1 -' 1) + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(j1 -' 1) + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (1,((j1 -' 1) + 2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (1,(j1 -' 1))) + ((GoB f) * (1,((j1 -' 1) + 1))))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,((j1 -' 1) + 1))) + ((GoB f) * (1,((j1 -' 1) + 2))))) - |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
j0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(j0 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i1 -' 1),(j0 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j0 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j0 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * (i1,(j0 -' 1))) + ((GoB f) * (i0,j1))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i1,(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),(j1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i1 -' 1),(j1 -' 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 -' 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),(j1 -' 1))) + ((GoB f) * (i1,j1)))),((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j2))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,(width (GoB f))) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),(width (GoB f))) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),(width (GoB f)))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,(width (GoB f))) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),(width (GoB f)))) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i0,(width (GoB f))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 + 1),(width (GoB f))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f))))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(width (GoB f))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(width (GoB f))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f))))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,(width (GoB f)))) + ((GoB f) * ((i0 + 1),(width (GoB f)))))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,(width (GoB f)))) + ((GoB f) * ((i1 + 1),(width (GoB f)))))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,(width (GoB f)))) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i0 + 1),(j0 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 + 1),(j0 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * ((i0 + 1),(j0 + 1))))),((1 / 2) * (((GoB f) * (i1,j0)) + ((GoB f) * ((i1 + 1),(j0 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),i0,j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i0,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (1,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,j0)) + ((GoB f) * (1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,j1)) + |[(- 1),1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((GoB f) * (1,j1)) + |[(- 1),1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (2,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,j1)) + ((GoB f) * (2,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((GoB f) * (1,j1)) + |[(- 1),1]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (2,j1)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i1 -' 1),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i1 -' 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j0)) + ((GoB f) * (i1,j1)))),(((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i2,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,j1)))) + |[0,1]|),(((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,j1)))) + |[0,1]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i0,j0)) + ((GoB f) * (i0,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (i0,j1)) + ((GoB f) * (i0,(j1 + 1))))) - |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (i1,(j0 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
j0 + 2 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * (i1,(j0 + 2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,(j0 + 2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i1,(j0 + 2))))) - |[1,0]|),((1 / 2) * (((GoB f) * (i1,(j0 + 1))) + ((GoB f) * (i2,(j0 + 2)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(i1 -' 1) + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(GoB f) * ((i0 -' 1),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 -' 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,(j1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j1)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),i1,j1) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),i1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),i1)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i1 -' 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i1,(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i2,(j1 + 1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i1 -' 1),j1)) + ((GoB f) * (i1,(j1 + 1))))),((1 / 2) * (((GoB f) * (i1,j1)) + ((GoB f) * (i2,(j1 + 1)))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),0,j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),0) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),0)) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),0,j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),0)) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * (1,j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (1,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,j0)) + ((GoB f) * (1,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (1,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * (1,j1)) + ((GoB f) * (1,j2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]| is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB f) * (1,j0)) + ((GoB f) * (1,j1)))) - |[1,0]|),(((1 / 2) * (((GoB f) * (1,j1)) + ((GoB f) * (1,j2)))) - |[1,0]|)) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),0,j0)) is Element of K6( the carrier of (TOP-REAL 2))
cell ((GoB f),(i1 -' 1),j0) is Element of K6( the carrier of (TOP-REAL 2))
v_strip ((GoB f),(i1 -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j0) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j0)) is Element of K6( the carrier of (TOP-REAL 2))
i0 -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
cell ((GoB f),(i1 -' 1),j1) is Element of K6( the carrier of (TOP-REAL 2))
h_strip ((GoB f),j1) is Element of K6( the carrier of (TOP-REAL 2))
(v_strip ((GoB f),(i1 -' 1))) /\ (h_strip ((GoB f),j1)) is Element of K6( the carrier of (TOP-REAL 2))
(GoB f) * ((i0 -' 1),j0) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * ((i0 -' 1),j1) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(GoB f) * (i0,j2) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2)) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
(1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))) is 2 -element FinSequence-like V82() Element of the carrier of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB f) * ((i0 -' 1),j0)) + ((GoB f) * (i0,j1)))),((1 / 2) * (((GoB f) * ((i0 -' 1),j1)) + ((GoB f) * (i0,j2))))) is non empty connected convex Element of K6( the carrier of (TOP-REAL 2))
Int (cell ((GoB f),(i1 -' 1),j0)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
GoB (f) is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
GoB f is V13() non empty-yielding V16( NAT ) V17(K247( the carrier of (TOP-REAL 2))) Function-like V26() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K247( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
(f) is Element of K6( the carrier of (TOP-REAL 2))
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
((f)) is Element of K6( the carrier of (TOP-REAL 2))
L~ (f) is Element of K6( the carrier of (TOP-REAL 2))
(L~ (f)) ` is Element of K6( the carrier of (TOP-REAL 2))
L~ f is Element of K6( the carrier of (TOP-REAL 2))
(L~ f) ` is Element of K6( the carrier of (TOP-REAL 2))
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) -' 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell (f,1) is Element of K6( the carrier of (TOP-REAL 2))
left_cell ((f),((len f) -' 1)) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,1)) is Element of K6( the carrier of (TOP-REAL 2))
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
((f)) is Element of K6( the carrier of (TOP-REAL 2))
(f) is Element of K6( the carrier of (TOP-REAL 2))
((f)) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
f is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(f) is Element of K6( the carrier of (TOP-REAL 2))
k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
right_cell (f,k) is Element of K6( the carrier of (TOP-REAL 2))
Int (right_cell (f,k)) is Element of K6( the carrier of (TOP-REAL 2))
(f) is non empty V13() V16( NAT ) V17( the carrier of (TOP-REAL 2)) Function-like non constant V26() FinSequence-like FinSubsequence-like V174( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len (f) is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
(len f) -' k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + k is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
((len f) -' k) + 1 is V4() V5() V6() V10() V11() V12() ext-real V90() V91() V92() V93() V94() V95() V96() V97() Element of NAT
left_cell ((f),((len f) -' k)) is Element of K6( the carrier of (TOP-REAL 2))
((f)) is Element of K6( the carrier of (TOP-REAL 2))