REAL is set
NAT is non empty V4() V5() V6() Element of K6(REAL)
K6(REAL) is set
COMPLEX is set
NAT is non empty V4() V5() V6() set
K6(NAT) is set
RAT is set
INT is set
K6(NAT) is set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive 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 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 V128() V153() V154() V155() V156() V157() V158() V159() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
K269( the U1 of (TOP-REAL 2)) is M11( the U1 of (TOP-REAL 2))
K6( the U1 of (TOP-REAL 2)) is set
{} is set
0 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
K52(1,2) is V11() V12() ext-real Element of REAL
|[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
|[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
1 / 2 is V11() V12() ext-real Element of COMPLEX
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))))),((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,j1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
((Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))))),((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,j1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
((Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))))),((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),i1,(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,j1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
((Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))))),((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,j1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
((Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),i1,(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * (i1,(j1 + 1))) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 1),(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1))))),((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),(i1 + 1),j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),j1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(i1 + 1),(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),(i1 + 1),j1))) \/ (Int (cell ((GoB k),(i1 + 1),(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))))} is set
((Int (cell ((GoB k),(i1 + 1),j1))) \/ (Int (cell ((GoB k),(i1 + 1),(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 2),(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1))))),((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 2)))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),(i1 + 1),(j1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),(j1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),(i1 + 1),j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),j1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),(i1 + 1),j1))) \/ (Int (cell ((GoB k),(i1 + 1),(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))))} is set
((Int (cell ((GoB k),(i1 + 1),j1))) \/ (Int (cell ((GoB k),(i1 + 1),(j1 + 1))))) \/ {((1 / 2) * (((GoB k) * ((i1 + 1),(j1 + 1))) + ((GoB k) * ((i1 + 2),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 2),(j1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1)))) - |[0,1]|),((1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),2))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),i1,1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,0) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,0)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,0))) \/ (Int (cell ((GoB k),i1,1))) is Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1))))} is set
((Int (cell ((GoB k),i1,0))) \/ (Int (cell ((GoB k),i1,1)))) \/ {((1 / 2) * (((GoB k) * (i1,1)) + ((GoB k) * ((i1 + 1),1))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (i1,1))) is Element of K6( the U1 of (TOP-REAL 2))
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j1) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1)))) - |[0,1]|),((1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),2))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
0 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),(i1 + 1),1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(i1 + 1),0) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),0)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),(i1 + 1),0))) \/ (Int (cell ((GoB k),(i1 + 1),1))) is Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1))))} is set
((Int (cell ((GoB k),(i1 + 1),0))) \/ (Int (cell ((GoB k),(i1 + 1),1)))) \/ {((1 / 2) * (((GoB k) * ((i1 + 1),1)) + ((GoB k) * ((i1 + 2),1))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 2),1))) is Element of K6( the U1 of (TOP-REAL 2))
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j1) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(width (GoB k)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 1),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 1),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k)))))) + |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 1),(width (GoB k)))))),(((1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k)))))) + |[0,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),i1,(width (GoB k))) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,(width (GoB k)))) is Element of K6( the U1 of (TOP-REAL 2))
((width (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
cell ((GoB k),i1,((width (GoB k)) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,((width (GoB k)) -' 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,((width (GoB k)) -' 1)))) \/ (Int (cell ((GoB k),i1,(width (GoB k))))) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),((width (GoB k)) -' 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),((width (GoB k)) -' 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k))))))} is set
((Int (cell ((GoB k),i1,((width (GoB k)) -' 1)))) \/ (Int (cell ((GoB k),i1,(width (GoB k)))))) \/ {((1 / 2) * (((GoB k) * (i1,(width (GoB k)))) + ((GoB k) * ((i1 + 1),(width (GoB k))))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (i1,(width (GoB k))))) is Element of K6( the U1 of (TOP-REAL 2))
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j1) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(width (GoB k)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 2),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 2),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k)))))) + |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * ((i1 + 1),((width (GoB k)) -' 1))) + ((GoB k) * ((i1 + 2),(width (GoB k)))))),(((1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k)))))) + |[0,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),(i1 + 1),(width (GoB k))) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),(width (GoB k)))) is Element of K6( the U1 of (TOP-REAL 2))
((width (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
cell ((GoB k),(i1 + 1),((width (GoB k)) -' 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),((width (GoB k)) -' 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),(i1 + 1),((width (GoB k)) -' 1)))) \/ (Int (cell ((GoB k),(i1 + 1),(width (GoB k))))) is Element of K6( the U1 of (TOP-REAL 2))
(GoB k) * ((i1 + 2),((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),((width (GoB k)) -' 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),((width (GoB k)) -' 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k))))))} is set
((Int (cell ((GoB k),(i1 + 1),((width (GoB k)) -' 1)))) \/ (Int (cell ((GoB k),(i1 + 1),(width (GoB k)))))) \/ {((1 / 2) * (((GoB k) * ((i1 + 1),(width (GoB k)))) + ((GoB k) * ((i1 + 2),(width (GoB k))))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 2),(width (GoB k))))) is Element of K6( the U1 of (TOP-REAL 2))
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j1) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((i1 + 1),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 2),(j1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((i1 + 1),j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (i1,j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))))),((1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 2),(j1 + 1)))))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),i1,j1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(i1 + 1),j1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(i1 + 1),j1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),(i1 + 1),j1))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 1),(j1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
((Int (cell ((GoB k),i1,j1))) \/ (Int (cell ((GoB k),(i1 + 1),j1)))) \/ {((1 / 2) * (((GoB k) * ((i1 + 1),j1)) + ((GoB k) * ((i1 + 1),(j1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((i1 + 1),j1))) is Element of K6( the U1 of (TOP-REAL 2))
j is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,j) is Element of K6( the U1 of (TOP-REAL 2))
k is non empty V15() V18( NAT ) V19( the U1 of (TOP-REAL 2)) V20() non constant FinSequence-like V172( the U1 of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the U1 of (TOP-REAL 2)
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
GoB k is V15() V17() V18( NAT ) V19(K269( the U1 of (TOP-REAL 2))) V20() FinSequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K269( the U1 of (TOP-REAL 2))
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k /. (f + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (f + 2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(f + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
LSeg (k,(f + 1)) is Element of K6( the U1 of (TOP-REAL 2))
LSeg (k,f) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. f),(k /. (f + 1))) is Element of K6( the U1 of (TOP-REAL 2))
LSeg ((k /. (f + 1)),(k /. (f + 2))) is Element of K6( the U1 of (TOP-REAL 2))
i1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((j1 + 1),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((j1 + 1),(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((j1 + 2),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (j1,i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (j1,i1)) + ((GoB k) * ((j1 + 1),(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (j1,i1)) + ((GoB k) * ((j1 + 1),(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((j1 + 1),i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 2),(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 2),(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (j1,i1)) + ((GoB k) * ((j1 + 1),(i1 + 1))))),((1 / 2) * (((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 2),(i1 + 1)))))) is Element of K6( the U1 of (TOP-REAL 2))
(i1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),j1,i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),j1,i1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(j1 + 1),i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(j1 + 1),i1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),j1,i1))) \/ (Int (cell ((GoB k),(j1 + 1),i1))) is Element of K6( the U1 of (TOP-REAL 2))
(j1 + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j1 + (1 + 1) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 1),(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 1),(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 1),(i1 + 1)))))} is set
((Int (cell ((GoB k),j1,i1))) \/ (Int (cell ((GoB k),(j1 + 1),i1)))) \/ {((1 / 2) * (((GoB k) * ((j1 + 1),i1)) + ((GoB k) * ((j1 + 1),(i1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((j1 + 1),i1))) is