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 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,(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 + 2),(i1 + 1)) 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 + 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))
(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),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))
(Int (cell ((GoB k),j1,i1))) \/ (Int (cell ((GoB k),(j1 + 1),i1))) is Element of K6( the U1 of (TOP-REAL 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 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 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 + 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) 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 + 2),i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((j1 + 1),(i1 + 1)) 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 + 2),(i1 + 1)) 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))
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 + 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))
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) 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 + 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,(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (j1,(i1 + 1))) + ((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 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (j1,(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))))),((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 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),j1,(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),j1,(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),(j1 + 1),(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(j1 + 1),(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),j1,(i1 + 1)))) \/ (Int (cell ((GoB k),(j1 + 1),(i1 + 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) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))))} is set
((Int (cell ((GoB k),j1,(i1 + 1)))) \/ (Int (cell ((GoB k),(j1 + 1),(i1 + 1))))) \/ {((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((j1 + 1),(i1 + 2)))) 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) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (j1,(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,(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (j1,(i1 + 1))) + ((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 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (j1,(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))))),((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 2),(i1 + 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),(j1 + 1),(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(j1 + 1),(i1 + 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),j1,(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),j1,(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),j1,(i1 + 1)))) \/ (Int (cell ((GoB k),(j1 + 1),(i1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))))} is set
((Int (cell ((GoB k),j1,(i1 + 1)))) \/ (Int (cell ((GoB k),(j1 + 1),(i1 + 1))))) \/ {((1 / 2) * (((GoB k) * ((j1 + 1),(i1 + 1))) + ((GoB k) * ((j1 + 1),(i1 + 2)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((j1 + 1),(i1 + 2)))) 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
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))
len (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) * (1,(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (2,(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1))))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i1)) + ((GoB k) * (2,(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (2,(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1))))) - |[1,0]|),((1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (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
0 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB k),1,i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),1,i1)) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),0,i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),0,i1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),0,i1))) \/ (Int (cell ((GoB k),1,i1))) is Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1)))))} is set
((Int (cell ((GoB k),0,i1))) \/ (Int (cell ((GoB k),1,i1)))) \/ {((1 / 2) * (((GoB k) * (1,i1)) + ((GoB k) * (1,(i1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (1,i1))) 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
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))
len (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) * (1,(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (2,(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2))))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (2,(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(i1 + 1))) + ((GoB k) * (2,(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (2,(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2))))) - |[1,0]|),((1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (2,(i1 + 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),1,(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),1,(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
cell ((GoB k),0,(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),0,(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),0,(i1 + 1)))) \/ (Int (cell ((GoB k),1,(i1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
{((1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2)))))} is set
((Int (cell ((GoB k),0,(i1 + 1)))) \/ (Int (cell ((GoB k),1,(i1 + 1))))) \/ {((1 / 2) * (((GoB k) * (1,(i1 + 1))) + ((GoB k) * (1,(i1 + 2)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * (1,(i1 + 2)))) 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
(len (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) * ((len (GoB k)),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (((len (GoB k)) -' 1),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (((len (GoB k)) -' 1),i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1))))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1))))),(((1 / 2) * (((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1))))) + |[1,0]|)) 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),(len (GoB k)),i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(len (GoB k)),i1)) is Element of K6( the U1 of (TOP-REAL 2))
((len (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
cell ((GoB k),((len (GoB k)) -' 1),i1) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),((len (GoB k)) -' 1),i1)) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),((len (GoB k)) -' 1),i1))) \/ (Int (cell ((GoB k),(len (GoB k)),i1))) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * (((len (GoB k)) -' 1),(i1 + 1))) + ((GoB k) * ((len (GoB k)),i1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(i1 + 1))) + ((GoB k) * ((len (GoB k)),i1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1)))))} is set
((Int (cell ((GoB k),((len (GoB k)) -' 1),i1))) \/ (Int (cell ((GoB k),(len (GoB k)),i1)))) \/ {((1 / 2) * (((GoB k) * ((len (GoB k)),i1)) + ((GoB k) * ((len (GoB k)),(i1 + 1)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((len (GoB k)),i1))) 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
(len (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) * ((len (GoB k)),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),i1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (((len (GoB k)) -' 1),(i1 + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2))))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg (((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2))))),(((1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2))))) + |[1,0]|)) 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),(len (GoB k)),(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),(len (GoB k)),(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
((len (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
cell ((GoB k),((len (GoB k)) -' 1),(i1 + 1)) is Element of K6( the U1 of (TOP-REAL 2))
Int (cell ((GoB k),((len (GoB k)) -' 1),(i1 + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(Int (cell ((GoB k),((len (GoB k)) -' 1),(i1 + 1)))) \/ (Int (cell ((GoB k),(len (GoB k)),(i1 + 1)))) is Element of K6( the U1 of (TOP-REAL 2))
(GoB k) * (((len (GoB k)) -' 1),(i1 + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * (((len (GoB k)) -' 1),(i1 + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * (((len (GoB k)) -' 1),(i1 + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
{((1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2)))))} is set
((Int (cell ((GoB k),((len (GoB k)) -' 1),(i1 + 1)))) \/ (Int (cell ((GoB k),(len (GoB k)),(i1 + 1))))) \/ {((1 / 2) * (((GoB k) * ((len (GoB k)),(i1 + 1))) + ((GoB k) * ((len (GoB k)),(i1 + 2)))))} is set
LSeg ((k /. (f + 1)),((GoB k) * ((len (GoB k)),(i1 + 2)))) 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)
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))
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `1 is V11() V12() ext-real Element of REAL
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is Element of K6( the U1 of (TOP-REAL 2))
i1 is set
j1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 `1 is V11() V12() ext-real Element of REAL
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
k /. j is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (j + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((k /. j),(k /. (j + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(k /. j) `1 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (i,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i,1)) `1 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. j) `1 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (i,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i,1)) `1 is V11() V12() ext-real Element of REAL
(k /. j) `1 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * ((len (GoB k)),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) `1 is V11() V12() ext-real Element of REAL
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is Element of K6( the U1 of (TOP-REAL 2))
i1 is set
j1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 `1 is V11() V12() ext-real Element of REAL
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
k /. j is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (j + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((k /. j),(k /. (j + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. j) `1 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i,1)) `1 is V11() V12() ext-real Element of REAL
(k /. j) `1 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (i,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (i,1)) `1 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `1 is V11() V12() ext-real Element of REAL
(k /. j) `1 is V11() V12() ext-real Element of REAL
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)
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))
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `2 is V11() V12() ext-real Element of REAL
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is Element of K6( the U1 of (TOP-REAL 2))
i1 is set
j1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 `2 is V11() V12() ext-real Element of REAL
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
k /. j is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (j + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((k /. j),(k /. (j + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(k /. j) `2 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (1,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i2)) `2 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. j) `2 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (1,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i2)) `2 is V11() V12() ext-real Element of REAL
(k /. j) `2 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * (1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
L~ k is Element of K6( the U1 of (TOP-REAL 2))
f is Element of K6( the U1 of (TOP-REAL 2))
i1 is set
j1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
j1 `2 is V11() V12() ext-real Element of REAL
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
len k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
k /. j is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
k /. (j + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((k /. j),(k /. (j + 1))) is Element of K6( the U1 of (TOP-REAL 2))
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. j) `2 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i2)) `2 is V11() V12() ext-real Element of REAL
(k /. j) `2 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
dom k is Element of K6(NAT)
Indices (GoB k) is set
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i,i2] is set
(GoB k) * (i,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,i2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,i2)) `2 is V11() V12() ext-real Element of REAL
(k /. (j + 1)) `2 is V11() V12() ext-real Element of REAL
(k /. j) `2 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * (f,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((f + 1),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((f + 2),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) - |[0,1]|),(((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) - |[0,1]|)) 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
((GoB k) * (f,1)) `2 is V11() V12() ext-real Element of REAL
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `2 is V11() V12() ext-real Element of REAL
((GoB k) * ((f + 1),1)) `2 is V11() V12() ext-real Element of REAL
((GoB k) * ((f + 2),1)) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) - |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) `2) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1))) `2)) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2))) - (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `2)) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) - |[0,1]|) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `2) - 1 is V11() V12() ext-real set
|[((((1 / 2) * (((GoB k) * ((f + 1),1)) + ((GoB k) * ((f + 2),1)))) - |[0,1]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) - |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) `2) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1))) `2)) - (|[0,1]| `2) is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) - |[0,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((1 / 2) * (((GoB k) * (f,1)) + ((GoB k) * ((f + 1),1)))) - |[0,1]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 `2 is V11() V12() ext-real Element of REAL
|[1,1]| is V39(2) V78() FinSequence-like Element of 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)
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))
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) - |[1,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (2,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) + ((GoB k) * (2,1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((GoB k) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) - |[0,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k 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
len (GoB k) 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
((GoB k) * (2,1)) `2 is V11() V12() ext-real Element of REAL
((GoB k) * (1,1)) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) - |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) `2) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) + ((GoB k) * (2,1))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,1)) + ((GoB k) * (2,1))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) + ((GoB k) * (2,1))) `2)) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2))) - (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `2)) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) - |[0,1]|) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `2) - 1 is V11() V12() ext-real set
|[((((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (2,1)))) - |[0,1]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((GoB k) * (1,1)) - |[1,1]|) `2 is V11() V12() ext-real Element of REAL
|[1,1]| `2 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `2) - (|[1,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) - |[1,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) - |[1,1]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `2 is V11() V12() ext-real Element of REAL
- 1 is V11() V12() ext-real set
|[1,(- 1)]| is V39(2) V78() FinSequence-like Element of 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)
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
(len (GoB k)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative Element of NAT
(GoB k) * (((len (GoB k)) -' 1),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) - |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) - |[0,1]|),(((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k 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
((len (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
((GoB k) * ((len (GoB k)),1)) `2 is V11() V12() ext-real Element of REAL
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `2 is V11() V12() ext-real Element of REAL
(((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `2 is V11() V12() ext-real Element of REAL
|[1,(- 1)]| `2 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `2) + (|[1,(- 1)]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) `2) + (- 1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `2) - 1 is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `1 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),1)) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) - |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) `2) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1))) `2)) - (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `2) + (((GoB k) * (1,1)) `2))) - (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `2)) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) - |[0,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),1)) + ((GoB k) * ((len (GoB k)),1)))) - |[0,1]|) `1),((((GoB k) * (1,1)) `2) - 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `2 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * (f,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((f + 1),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) + |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((f + 2),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 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) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) + |[0,1]|),(((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) + |[0,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * (f,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(GoB k) * (1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
((GoB k) * ((f + 1),(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
((GoB k) * ((f + 2),(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) + |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) `2) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k))))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k))))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k))))) `2)) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2))) + (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,(width (GoB k)))) `2)) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) + |[0,1]|) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,(width (GoB k)))) `2) + 1 is V11() V12() ext-real set
|[((((1 / 2) * (((GoB k) * ((f + 1),(width (GoB k)))) + ((GoB k) * ((f + 2),(width (GoB k)))))) + |[0,1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) + |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) `2) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k))))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k))))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k))))) `2)) + (|[0,1]| `2) is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) + |[0,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((1 / 2) * (((GoB k) * (f,(width (GoB k)))) + ((GoB k) * ((f + 1),(width (GoB k)))))) + |[0,1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 `2 is V11() V12() ext-real Element of REAL
|[(- 1),1]| is V39(2) V78() FinSequence-like Element of 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)
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
(GoB k) * (1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (2,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) + |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|),(((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) + |[0,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k is Element of K6( the U1 of (TOP-REAL 2))
len (GoB k) 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
((GoB k) * (2,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
((GoB k) * (1,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) + |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) `2) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k))))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k))))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k))))) `2)) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2))) + (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,(width (GoB k)))) `2)) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) + |[0,1]|) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,(width (GoB k)))) `2) + 1 is V11() V12() ext-real set
|[((((1 / 2) * (((GoB k) * (1,(width (GoB k)))) + ((GoB k) * (2,(width (GoB k)))))) + |[0,1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `2 is V11() V12() ext-real Element of REAL
|[(- 1),1]| `2 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,(width (GoB k)))) `2) + (|[(- 1),1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `1 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `2 is V11() V12() ext-real Element of REAL
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)
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
(len (GoB k)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative Element of NAT
width (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (((len (GoB k)) -' 1),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[0,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[0,1]|),(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k is Element of K6( the U1 of (TOP-REAL 2))
((len (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
((GoB k) * ((len (GoB k)),(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(GoB k) * (1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `2 is V11() V12() ext-real Element of REAL
|[1,1]| `2 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,(width (GoB k)))) `2) + (|[1,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) `2) + 1 is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[0,1]|) `2 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) `2 is V11() V12() ext-real Element of REAL
|[0,1]| `2 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) `2) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `2 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `2) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `2)) + (|[0,1]| `2) is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,(width (GoB k)))) `2) + (((GoB k) * (1,(width (GoB k)))) `2))) + (|[0,1]| `2) is V11() V12() ext-real set
1 * (((GoB k) * (1,(width (GoB k)))) `2) is V11() V12() ext-real set
(1 * (((GoB k) * (1,(width (GoB k)))) `2)) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[0,1]|) `1 is V11() V12() ext-real Element of REAL
|[((((1 / 2) * (((GoB k) * (((len (GoB k)) -' 1),(width (GoB k)))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[0,1]|) `1),((((GoB k) * (1,(width (GoB k)))) `2) + 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `2 is V11() V12() ext-real Element of REAL
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)
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
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
(GoB k) * (1,f) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * (1,(f + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,(f + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) - |[1,0]|),(((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) - |[1,0]|)) is Element of K6( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * (1,f)) `1 is V11() V12() ext-real Element of REAL
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `1 is V11() V12() ext-real Element of REAL
((GoB k) * (1,(f + 1))) `1 is V11() V12() ext-real Element of REAL
((GoB k) * (1,(f + 2))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) - |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) `1) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2)))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2)))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2)))) `1)) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1))) - (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `1)) - 1 is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) - |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((1 / 2) * (((GoB k) * (1,(f + 1))) + ((GoB k) * (1,(f + 2))))) - |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) - |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) `1) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1)))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1)))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1)))) `1)) - (|[1,0]| `1) is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) - |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((1 / 2) * (((GoB k) * (1,f)) + ((GoB k) * (1,(f + 1))))) - |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 `1 is V11() V12() ext-real Element of REAL
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)
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))
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) - |[1,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) + ((GoB k) * (1,2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((GoB k) * (1,1)) - |[1,1]|),(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) - |[1,0]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k is Element of K6( 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
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * (1,2)) `1 is V11() V12() ext-real Element of REAL
((GoB k) * (1,1)) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) - |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) `1) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) + ((GoB k) * (1,2))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,1)) + ((GoB k) * (1,2))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) + ((GoB k) * (1,2))) `1)) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1))) - (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `1)) - 1 is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) - |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((1 / 2) * (((GoB k) * (1,1)) + ((GoB k) * (1,2)))) - |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((GoB k) * (1,1)) - |[1,1]|) `1 is V11() V12() ext-real Element of REAL
|[1,1]| `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `1) - (|[1,1]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) - |[1,1]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((GoB k) * (1,1)) - |[1,1]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
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)
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
(width (GoB k)) -' 1 is V4() V5() V6() V10() V11() V12() ext-real non negative Element of NAT
(GoB k) * (1,((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * (1,(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) - |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) - |[1,0]|),(((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k is Element of K6( the U1 of (TOP-REAL 2))
len (GoB k) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((width (GoB k)) -' 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real positive Element of NAT
((GoB k) * (1,(width (GoB k)))) `1 is V11() V12() ext-real Element of REAL
(GoB k) * (1,1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,1)) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `1 is V11() V12() ext-real Element of REAL
|[(- 1),1]| `1 is V11() V12() ext-real Element of REAL
(((GoB k) * (1,1)) `1) + (|[(- 1),1]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) + (- 1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) - 1 is V11() V12() ext-real set
(((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((GoB k) * (1,(width (GoB k)))) + |[(- 1),1]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * (1,((width (GoB k)) -' 1))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) - |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) `1) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k))))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k))))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k))))) `1)) - (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * (1,1)) `1) + (((GoB k) * (1,1)) `1))) - (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * (1,1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * (1,1)) `1)) - 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) - |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * (1,1)) `1) - 1),((((1 / 2) * (((GoB k) * (1,((width (GoB k)) -' 1))) + ((GoB k) * (1,(width (GoB k)))))) - |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * ((len (GoB k)),f) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
(GoB k) * ((len (GoB k)),(f + 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),(f + 2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) + |[1,0]|),(((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) + |[1,0]|)) is Element of K6( the U1 of (TOP-REAL 2))
((GoB k) * ((len (GoB k)),f)) `1 is V11() V12() ext-real Element of REAL
(GoB k) * ((len (GoB k)),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) `1 is V11() V12() ext-real Element of REAL
((GoB k) * ((len (GoB k)),(f + 1))) `1 is V11() V12() ext-real Element of REAL
((GoB k) * ((len (GoB k)),(f + 2))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) + |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) `1) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2)))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2)))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2)))) `1)) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1))) + (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * ((len (GoB k)),1)) `1)) + 1 is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) + |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((1 / 2) * (((GoB k) * ((len (GoB k)),(f + 1))) + ((GoB k) * ((len (GoB k)),(f + 2))))) + |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) + |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) `1) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1)))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1)))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1)))) `1)) + (|[1,0]| `1) is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) + |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((1 / 2) * (((GoB k) * ((len (GoB k)),f)) + ((GoB k) * ((len (GoB k)),(f + 1))))) + |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 `1 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * ((len (GoB k)),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|),(((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) + |[1,0]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ k 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
1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
((GoB k) * ((len (GoB k)),2)) `1 is V11() V12() ext-real Element of REAL
((GoB k) * ((len (GoB k)),1)) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) + |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) `1) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2))) `1)) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1))) + (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * ((len (GoB k)),1)) `1)) + 1 is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) + |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((1 / 2) * (((GoB k) * ((len (GoB k)),1)) + ((GoB k) * ((len (GoB k)),2)))) + |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `1 is V11() V12() ext-real Element of REAL
|[1,(- 1)]| `1 is V11() V12() ext-real Element of REAL
(((GoB k) * ((len (GoB k)),1)) `1) + (|[1,(- 1)]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((GoB k) * ((len (GoB k)),1)) + |[1,(- 1)]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
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)
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
(GoB k) * ((len (GoB k)),((width (GoB k)) -' 1)) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(GoB k) * ((len (GoB k)),(width (GoB k))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
(1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[1,0]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
LSeg ((((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[1,0]|),(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|)) is Element of K6( the U1 of (TOP-REAL 2))
L~ 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
((GoB k) * ((len (GoB k)),(width (GoB k)))) `1 is V11() V12() ext-real Element of REAL
(GoB k) * ((len (GoB k)),1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),1)) `1 is V11() V12() ext-real Element of REAL
(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `1 is V11() V12() ext-real Element of REAL
|[1,1]| `1 is V11() V12() ext-real Element of REAL
(((GoB k) * ((len (GoB k)),1)) `1) + (|[1,1]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + 1 is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((GoB k) * ((len (GoB k)),(width (GoB k)))) + |[1,1]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[1,0]|) `1 is V11() V12() ext-real Element of REAL
((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) `1 is V11() V12() ext-real Element of REAL
|[1,0]| `1 is V11() V12() ext-real Element of REAL
(((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) `1) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `1 is V11() V12() ext-real Element of REAL
(1 / 2) * ((((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `1) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k))))) `1)) + (|[1,0]| `1) is V11() V12() ext-real set
(((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1)) is V11() V12() ext-real set
((1 / 2) * ((((GoB k) * ((len (GoB k)),1)) `1) + (((GoB k) * ((len (GoB k)),1)) `1))) + (|[1,0]| `1) is V11() V12() ext-real set
1 * (((GoB k) * ((len (GoB k)),1)) `1) is V11() V12() ext-real set
(1 * (((GoB k) * ((len (GoB k)),1)) `1)) + 1 is V11() V12() ext-real set
(((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[1,0]|) `2 is V11() V12() ext-real Element of REAL
|[((((GoB k) * ((len (GoB k)),1)) `1) + 1),((((1 / 2) * (((GoB k) * ((len (GoB k)),((width (GoB k)) -' 1))) + ((GoB k) * ((len (GoB k)),(width (GoB k)))))) + |[1,0]|) `2)]| is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
f `1 is V11() V12() ext-real Element of REAL
k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f 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 f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
left_cell (f,k) is Element of K6( the U1 of (TOP-REAL 2))
Int (left_cell (f,k)) is Element of K6( the U1 of (TOP-REAL 2))
L~ f is Element of K6( the U1 of (TOP-REAL 2))
dom f is Element of K6(NAT)
GoB f 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))
Indices (GoB f) is set
f /. k is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 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
[i1,j1] is set
(GoB f) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j is V4() V5() V6() V10() V11() V12() ext-real set
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i is V4() V5() V6() V10() V11() V12() ext-real set
i + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f /. (k + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i2,j2] is set
(GoB f) * (i2,j2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 - i2 is V11() V12() ext-real set
abs (i1 - i2) is V11() V12() ext-real Element of REAL
j1 - j2 is V11() V12() ext-real set
abs (j1 - j2) is V11() V12() ext-real Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is V11() V12() ext-real set
i19 is V11() V12() ext-real Element of REAL
i29 is V11() V12() ext-real Element of REAL
i19 - i29 is V11() V12() ext-real set
abs (i19 - i29) is V11() V12() ext-real Element of REAL
j19 is V11() V12() ext-real Element of REAL
j29 is V11() V12() ext-real Element of REAL
j19 - j29 is V11() V12() ext-real set
abs (j19 - j29) is V11() V12() ext-real Element of REAL
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i,j1) is Element of K6( the U1 of (TOP-REAL 2))
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i2,j) is Element of K6( the U1 of (TOP-REAL 2))
j2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i1,j2) is Element of K6( the U1 of (TOP-REAL 2))
j1 + 1 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
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
k + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f 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 f is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
right_cell (f,k) is Element of K6( the U1 of (TOP-REAL 2))
Int (right_cell (f,k)) is Element of K6( the U1 of (TOP-REAL 2))
L~ f is Element of K6( the U1 of (TOP-REAL 2))
dom f is Element of K6(NAT)
GoB f 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))
Indices (GoB f) is set
f /. k is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 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
[i1,j1] is set
(GoB f) * (i1,j1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
len (GoB f) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j is V4() V5() V6() V10() V11() V12() ext-real set
j + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i is V4() V5() V6() V10() V11() V12() ext-real set
i + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
width (GoB f) is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
f /. (k + 1) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
[i2,j2] is set
(GoB f) * (i2,j2) is V39(2) V78() FinSequence-like Element of the U1 of (TOP-REAL 2)
i1 - i2 is V11() V12() ext-real set
abs (i1 - i2) is V11() V12() ext-real Element of REAL
j1 - j2 is V11() V12() ext-real set
abs (j1 - j2) is V11() V12() ext-real Element of REAL
(abs (i1 - i2)) + (abs (j1 - j2)) is V11() V12() ext-real set
i19 is V11() V12() ext-real Element of REAL
i29 is V11() V12() ext-real Element of REAL
i19 - i29 is V11() V12() ext-real set
abs (i19 - i29) is V11() V12() ext-real Element of REAL
j19 is V11() V12() ext-real Element of REAL
j29 is V11() V12() ext-real Element of REAL
j19 - j29 is V11() V12() ext-real set
abs (j19 - j29) is V11() V12() ext-real Element of REAL
i is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
i + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
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
j1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i1,j1) is Element of K6( the U1 of (TOP-REAL 2))
i1 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i1,j) is Element of K6( the U1 of (TOP-REAL 2))
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i2,j1) is Element of K6( the U1 of (TOP-REAL 2))
j2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
cell ((GoB f),i,j2) is Element of K6( the U1 of (TOP-REAL 2))
j1 + 1 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
i2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT
j2 + 1 is V4() V5() V6() V10() V11() V12() ext-real Element of NAT