:: GOBOARD3 semantic presentation

REAL is set
NAT is non empty V4() V5() V6() V33() V38() V39() Element of bool REAL
bool REAL is set
COMPLEX is set
NAT is non empty V4() V5() V6() V33() V38() V39() set
bool NAT is V33() set
bool NAT is V33() set
1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
[:2,2:] is set
[:[:2,2:],REAL:] is set
bool [:[:2,2:],REAL:] is set
RAT is set
INT is set
bool [:REAL,REAL:] is set
TOP-REAL 2 is non empty TopSpace-like V100() V146() V147() V148() V149() V150() V151() V152() strict RLTopStruct
the U1 of (TOP-REAL 2) is non empty set
bool the U1 of (TOP-REAL 2) is set
K292( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
{} is set
the empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative functional V33() V38() V40( {} ) FinSequence-membered V71() set is empty V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative functional V33() V38() V40( {} ) FinSequence-membered V71() set
3 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
Seg 1 is non empty trivial V33() V40(1) Element of bool NAT
{1} is non empty trivial V40(1) set
Seg 2 is non empty V33() V40(2) Element of bool NAT
{1,2} is set
0 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
f is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
f | G is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom (f | G) is Element of bool NAT
len (f | G) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len (f | G)) is V33() V40( len (f | G)) Element of bool NAT
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
0 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
dom f is Element of bool NAT
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg ((f | G),g) is Element of bool the U1 of (TOP-REAL 2)
g + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg ((f | G),(g + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg ((f | G),g)) /\ (LSeg ((f | G),(g + 1))) is Element of bool the U1 of (TOP-REAL 2)
(f | G) /. (g + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{((f | G) /. (g + 1))} is non empty trivial V40(1) set
f1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
f1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg ((f | G),f1) is Element of bool the U1 of (TOP-REAL 2)
LSeg (f,f1) is Element of bool the U1 of (TOP-REAL 2)
f1 + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(f1 + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
f1 + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg ((f | G),(f1 + 1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (f,(f1 + 1)) is Element of bool the U1 of (TOP-REAL 2)
(f | G) /. (f1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f /. (f1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom f is Element of bool NAT
L~ f is Element of bool the U1 of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
f /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f /. (len f) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G is V16() non empty-yielding V19( NAT ) V20(K292( the U1 of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K292( the U1 of (TOP-REAL 2))
Indices G is set
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
c₄ is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len c₄ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom c₄ is Element of bool NAT
L~ c₄ is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (c₄,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₄ ) } is set
union { (LSeg (c₄,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₄ ) } is set
c₄ /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₄ /. (len c₄) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ f1 is Element of bool the U1 of (TOP-REAL 2)
len f1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (f1,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f1 ) } is set
union { (LSeg (f1,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f1 ) } is set
f1 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f1 /. (len f1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
j1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom f1 is Element of bool NAT
j1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
f1 /. j1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f1 /. (j1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
j2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[j2,i1] is set
{j2,i1} is set
{j2} is non empty trivial V40(1) set
{{j2,i1},{j2}} is set
i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
l1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[i2,l1] is set
{i2,l1} is set
{i2} is non empty trivial V40(1) set
{{i2,l1},{i2}} is set
G * (j2,i1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (i2,l1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
j2 - i2 is V11() V12() ext-real V71() set
abs (j2 - i2) is V11() V12() ext-real Element of REAL
i1 - l1 is V11() V12() ext-real V71() set
abs (i1 - l1) is V11() V12() ext-real Element of REAL
(abs (j2 - i2)) + (abs (i1 - l1)) is V11() V12() ext-real set
c₄ | g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len (c₄ | g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg g is V33() V40(g) Element of bool NAT
c₄ | (Seg g) is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like FinSubsequence-like Element of bool [:NAT, the U1 of (TOP-REAL 2):]
[:NAT, the U1 of (TOP-REAL 2):] is V33() set
bool [:NAT, the U1 of (TOP-REAL 2):] is V33() set
dom G is Element of bool NAT
len G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len G) is V33() V40( len G) Element of bool NAT
c₄ /. (g + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
j1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[j1,j2] is set
{j1,j2} is set
{j1} is non empty trivial V40(1) set
{{j1,j2},{j1}} is set
G * (j1,j2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
width G is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (width G) is V33() V40( width G) Element of bool NAT
[:(dom G),(Seg (width G)):] is set
c₄ /. g is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[i1,i2] is set
{i1,i2} is set
{i1} is non empty trivial V40(1) set
{{i1,i2},{i1}} is set
G * (i1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
Line (G,i1) is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M12( the U1 of (TOP-REAL 2),K293((width G), the U1 of (TOP-REAL 2)))
K293((width G), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
Col (G,i2) is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like M12( the U1 of (TOP-REAL 2),K293((len G), the U1 of (TOP-REAL 2)))
K293((len G), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M11( the U1 of (TOP-REAL 2))
l1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
X_axis l1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis l1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL
c1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
X_axis c1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL
Y_axis c1 is V16() V19( NAT ) V20( REAL ) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of REAL
dom (Y_axis l1) is Element of bool NAT
len (Y_axis l1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len (Y_axis l1)) is V33() V40( len (Y_axis l1)) Element of bool NAT
len l1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom (c₄ | g) is Element of bool NAT
Seg (len (c₄ | g)) is V33() V40( len (c₄ | g)) Element of bool NAT
g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(c₄ | g) /. g1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
((c₄ | g) /. g1) `1 is V11() V12() ext-real Element of REAL
(c<sub>4</sub> | g) /. (g1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
((c<sub>4</sub> | g) /. (g1 + 1)) `1 is V11() V12() ext-real Element of REAL
((c₄ | g) /. g1) `2 is V11() V12() ext-real Element of REAL
((c<sub>4</sub> | g) /. (g1 + 1)) `2 is V11() V12() ext-real Element of REAL
c₄ /. (g1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₄ /. g1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
c₄ /. g1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[ppi,pj] is set
{ppi,pj} is set
{ppi} is non empty trivial V40(1) set
{{ppi,pj},{ppi}} is set
G * (ppi,pj) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[l,g2] is set
{l,g2} is set
{l} is non empty trivial V40(1) set
{{l,g2},{l}} is set
(c₄ | g) /. g1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (l,g2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
L~ (c₄ | g) is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg ((c₄ | g),b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (c₄ | g) ) } is set
union { (LSeg ((c₄ | g),b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len (c₄ | g) ) } is set
(c₄ | g) /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(c₄ | g) /. (len (c₄ | g)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g1 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ g1 is Element of bool the U1 of (TOP-REAL 2)
len g1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g1,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
union { (LSeg (g1,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g1 ) } is set
g1 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g1 /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
dom g1 is Element of bool NAT
ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ppi + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[pj,l] is set
{pj,l} is set
{pj} is non empty trivial V40(1) set
{{pj,l},{pj}} is set
g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[g2,g] is set
{g2,g} is set
{g2} is non empty trivial V40(1) set
{{g2,g},{g2}} is set
g1 /. ppi is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (pj,l) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g1 /. (ppi + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (g2,g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
pj - g2 is V11() V12() ext-real V71() set
abs (pj - g2) is V11() V12() ext-real Element of REAL
l - g is V11() V12() ext-real V71() set
abs (l - g) is V11() V12() ext-real Element of REAL
(abs (pj - g2)) + (abs (l - g)) is V11() V12() ext-real set
rng g1 is set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
ppi is set
pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g1 /. pj is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(c₄ /. g)} is non empty trivial V40(1) set
ppi is set
pj is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g1 /. pj is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
Seg (len g1) is V33() V40( len g1) Element of bool NAT
len c1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom c1 is Element of bool NAT
dom (Y_axis c1) is Element of bool NAT
len (Y_axis c1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len (Y_axis c1)) is V33() V40( len (Y_axis c1)) Element of bool NAT
dom (X_axis l1) is Element of bool NAT
len (X_axis l1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len (X_axis l1)) is V33() V40( len (X_axis l1)) Element of bool NAT
dom (X_axis c1) is Element of bool NAT
len (X_axis c1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg (len (X_axis c1)) is V33() V40( len (X_axis c1)) Element of bool NAT
dom l1 is Element of bool NAT
ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g1 /. ppi is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (i1,j2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 /. i2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . i2 is set
(Y_axis l1) . i2 is set
(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL
l1 /. j2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . j2 is set
(Y_axis l1) . j2 is set
(G * (i1,j2)) `2 is V11() V12() ext-real Element of REAL
i2 - j2 is V11() V12() ext-real V71() set
(G * (i1,i2)) `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= b₁ `2 & b<sub>1</sub> `2 <= (G * (i1,i2)) `2 ) } is set
|[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg l is V33() V40(l) Element of bool NAT
i2 - g is V11() V12() ext-real V71() set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 - l is V11() V12() ext-real V71() set
[i1,(i2 - g)] is set
{i1,(i2 - g)} is set
{{i1,(i2 - g)},{i1}} is set
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
i2 - g is V11() V12() ext-real V71() set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g1 ^ g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom g is Element of bool NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 - lg is V11() V12() ext-real V71() set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom lk is Element of bool NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
Seg (len g) is V33() V40( len g) Element of bool NAT
(X_axis l1) . i2 is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 - lg is V11() V12() ext-real V71() set
i2 - (len g) is V11() V12() ext-real V71() set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(X_axis l1) . x is set
l1 /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . x is set
(Y_axis l1) . x is set
(G * (i1,x)) `2 is V11() V12() ext-real Element of REAL
(G * (i1,x)) `1 is V11() V12() ext-real Element of REAL
lf `1 is V11() V12() ext-real Element of REAL
lf `2 is V11() V12() ext-real Element of REAL
Seg (len l1) is V33() V40( len l1) Element of bool NAT
rng l1 is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g /. lg) `1 is V11() V12() ext-real Element of REAL
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g /. (lg + 1)) `1 is V11() V12() ext-real Element of REAL
(g /. lg) `2 is V11() V12() ext-real Element of REAL
(g /. (lg + 1)) `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 - lg is V11() V12() ext-real V71() set
i2 - lf is V11() V12() ext-real V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . ma is set
(Y_axis l1) . ma is set
(G * (i1,ma)) `2 is V11() V12() ext-real Element of REAL
l1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . ma is set
(Y_axis l1) . ma is set
(G * (i1,ma)) `2 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lg) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of bool the U1 of (TOP-REAL 2)
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & p1 `2 <= b₁ `2 & b<sub>1</sub> `2 <= x `2 ) } is set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & ma `2 <= b₁ `2 & b<sub>1</sub> `2 <= ma `2 ) } is set
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
the Element of (LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of (LSeg (g,lg)) /\ (LSeg (g,lf))
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (p1,x) is Element of bool the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
q2 `2 is V11() V12() ext-real Element of REAL
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
L~ g is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & ma `2 <= b<sub>1</sub> `2 & b₁ `2 <= p1 `2 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,p1) is Element of bool the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
qa `2 is V11() V12() ext-real Element of REAL
(X_axis l1) . j2 is set
(G * (i1,j2)) `1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 - lg is V11() V12() ext-real V71() set
i2 - lf is V11() V12() ext-real V71() set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 - lg)] is set
{i1,(i2 - lg)} is set
{{i1,(i2 - lg)},{i1}} is set
[i1,(i2 - lf)] is set
{i1,(i2 - lf)} is set
{{i1,(i2 - lf)},{i1}} is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
|[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (c₄,g) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,j2)),(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)
rng g is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 - x is V11() V12() ext-real V71() set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(G * (i1,p1)) `2 is V11() V12() ext-real Element of REAL
(G * (i1,p1)) `1 is V11() V12() ext-real Element of REAL
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
i2 - lf is V11() V12() ext-real V71() set
i2 - (lf + 1) is V11() V12() ext-real V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[ma,ma] is set
{ma,ma} is set
{ma} is non empty trivial V40(1) set
{{ma,ma},{ma}} is set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[qa,qa1] is set
{qa,qa1} is set
{qa} is non empty trivial V40(1) set
{{qa,qa1},{qa}} is set
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (qa,qa1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 - (lf + 1))] is set
{i1,(i2 - (lf + 1))} is set
{{i1,(i2 - (lf + 1))},{i1}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 - lf)] is set
{i1,(i2 - lf)} is set
{{i1,(i2 - lf)},{i1}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma - qa is V11() V12() ext-real V71() set
abs (ma - qa) is V11() V12() ext-real Element of REAL
ma - qa1 is V11() V12() ext-real V71() set
abs (ma - qa1) is V11() V12() ext-real Element of REAL
(abs (ma - qa)) + (abs (ma - qa1)) is V11() V12() ext-real set
(i2 - lf) - (i2 - (lf + 1)) is V11() V12() ext-real V71() set
abs ((i2 - lf) - (i2 - (lf + 1))) is V11() V12() ext-real Element of REAL
0 + (abs ((i2 - lf) - (i2 - (lf + 1)))) is V11() V12() ext-real set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 - 1 is V11() V12() ext-real V71() set
[i1,(i2 - 1)] is set
{i1,(i2 - 1)} is set
{{i1,(i2 - 1)},{i1}} is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
i2 - (i2 - 1) is V11() V12() ext-real V71() set
abs (i2 - (i2 - 1)) is V11() V12() ext-real Element of REAL
0 + (abs (i2 - (i2 - 1))) is V11() V12() ext-real set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[ma,ma] is set
{ma,ma} is set
{ma} is non empty trivial V40(1) set
{{ma,ma},{ma}} is set
lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
p1 - ma is V11() V12() ext-real V71() set
abs (p1 - ma) is V11() V12() ext-real Element of REAL
(abs (x - ma)) + (abs (p1 - ma)) is V11() V12() ext-real set
LSeg ((G * (i1,i2)),(G * (i1,j2))) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 - lf is V11() V12() ext-real V71() set
[i1,(i2 - lf)] is set
{i1,(i2 - lf)} is set
{{i1,(i2 - lf)},{i1}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(rng g1) /\ (rng g) is set
the Element of (rng g1) /\ (rng g) is Element of (rng g1) /\ (rng g)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lf)) /\ (LSeg (g,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g /. (lf + 1))} is non empty trivial V40(1) set
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
g /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
LSeg (ma,x) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & p1 `2 <= b<sub>1</sub> `2 & b₁ `2 <= ma `2 ) } is set
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((g /. lf),(g /. (lf + 2))) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,lf)) /\ (LSeg (lk,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(lk /. (lf + 1))} is non empty trivial V40(1) set
(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(lf + 2) - (len g1) is V11() V12() ext-real V71() set
lf - (len g1) is V11() V12() ext-real V71() set
(lf - (len g1)) + 2 is V11() V12() ext-real V71() set
g1 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lf + 2) - 1 is V11() V12() ext-real V71() set
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
(len lk) - (len g1) is V11() V12() ext-real V71() set
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
LSeg ((G * (i1,i2)),x) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
0 + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
g /. 2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & ma `2 <= b<sub>1</sub> `2 & b₁ `2 <= (G * (i1,i2)) `2 ) } is set
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),(g /. 2)) is Element of bool the U1 of (TOP-REAL 2)
lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),p1) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (p1,ma) is Element of bool the U1 of (TOP-REAL 2)
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(x + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,(x + 1)) is Element of bool the U1 of (TOP-REAL 2)
lf is set
p1 is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,qa) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (L~ g) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (L~ g1) /\ (L~ g) is Element of (L~ g1) /\ (L~ g)
lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
j2 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `1 is V11() V12() ext-real Element of REAL
lf `2 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lk /. ((len g1) + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
|[(lf `1),(lf `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & lf `2 <= b<sub>1</sub> `2 & b₁ `2 <= (G * (i1,i2)) `2 ) } is set
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,(len g1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (lf,(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
lma is set
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
q2 `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(qa1 + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,qa1) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
(ma - (len g1)) + 1 is V11() V12() ext-real V71() set
(ma + 1) - (len g1) is V11() V12() ext-real V71() set
lma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (qa1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & x `2 <= b<sub>1</sub> `2 & b₁ `2 <= q2 `2 ) } is set
q2 `1 is V11() V12() ext-real Element of REAL
|[(q2 `1),(q2 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (x,q2) is Element of bool the U1 of (TOP-REAL 2)
lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
c₃₆ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₆ `1 is V11() V12() ext-real Element of REAL
c<sub>36</sub> `2 is V11() V12() ext-real Element of REAL
c₃₇ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₇ `1 is V11() V12() ext-real Element of REAL
c<sub>37</sub> `2 is V11() V12() ext-real Element of REAL
LSeg (g,lma) is Element of bool the U1 of (TOP-REAL 2)
lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
j2 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(g /. 1) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `2 is V11() V12() ext-real Element of REAL
(g /. 1) `2 is V11() V12() ext-real Element of REAL
L~ lk is Element of bool the U1 of (TOP-REAL 2)
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (lk,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len lk ) } is set
union { (LSeg (lk,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len lk ) } is set
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 - (len g1) is V11() V12() ext-real V71() set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
p1 is set
ma is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
qa `2 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
qa1 `2 is V11() V12() ext-real Element of REAL
|[(qa `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(qa `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (qa1,qa) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = qa `1 & qa1 `2 <= b<sub>1</sub> `2 & b₁ `2 <= qa `2 ) } is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
lma `2 is V11() V12() ext-real Element of REAL
{qa} is non empty trivial V40(1) set
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = qa `1 & qa `2 <= b<sub>1</sub> `2 & b₁ `2 <= qa1 `2 ) } is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
lma `2 is V11() V12() ext-real Element of REAL
p1 is set
(L~ (c₄ | g)) \/ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa - 1 is V11() V12() ext-real V71() set
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
lma `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & (G * (i1,j2)) `2 <= b₁ `2 & b<sub>1</sub> `2 <= lma `2 ) } is set
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lk,qa1) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,j2)),lma) is Element of bool the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (qa + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & lma `2 <= b₁ `2 & b<sub>1</sub> `2 <= qa1 `2 ) } is set
lma `1 is V11() V12() ext-real Element of REAL
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
qa1 `1 is V11() V12() ext-real Element of REAL
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lk,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (lma,qa1) is Element of bool the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (len lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,lg) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 /. i2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . i2 is set
(Y_axis l1) . i2 is set
(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL
l1 /. j2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . j2 is set
(Y_axis l1) . j2 is set
(G * (i1,j2)) `2 is V11() V12() ext-real Element of REAL
j2 - i2 is V11() V12() ext-real V71() set
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom g2 is Element of bool NAT
g1 ^ g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Seg (len g2) is V33() V40( len g2) Element of bool NAT
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg l is V33() V40(l) Element of bool NAT
l + i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[i1,(i2 + lk)] is set
{i1,(i2 + lk)} is set
{{i1,(i2 + lk)},{i1}} is set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lg,lf] is set
{lg,lf} is set
{lg} is non empty trivial V40(1) set
{{lg,lf},{lg}} is set
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lg,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom g is Element of bool NAT
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(X_axis l1) . i2 is set
(G * (i1,i2)) `1 is V11() V12() ext-real Element of REAL
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lk)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(X_axis l1) . (i2 + lk) is set
l1 /. (i2 + lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . (i2 + lk) is set
(Y_axis l1) . (i2 + lk) is set
(G * (i1,(i2 + lk))) `2 is V11() V12() ext-real Element of REAL
i2 + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(G * (i1,(i2 + lk))) `1 is V11() V12() ext-real Element of REAL
lg `1 is V11() V12() ext-real Element of REAL
lg `2 is V11() V12() ext-real Element of REAL
Seg (len l1) is V33() V40( len l1) Element of bool NAT
rng l1 is set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g2 /. lk) `1 is V11() V12() ext-real Element of REAL
g2 /. (lk + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g2 /. (lk + 1)) `1 is V11() V12() ext-real Element of REAL
(g2 /. lk) `2 is V11() V12() ext-real Element of REAL
(g2 /. (lk + 1)) `2 is V11() V12() ext-real Element of REAL
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lk)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lg)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 + lk)] is set
{i1,(i2 + lk)} is set
{{i1,(i2 + lk)},{i1}} is set
[i1,(i2 + lg)] is set
{i1,(i2 + lg)} is set
{{i1,(i2 + lg)},{i1}} is set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= b₁ `2 & b<sub>1</sub> `2 <= (G * (i1,j2)) `2 ) } is set
|[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 + lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lg)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (i1,(i2 + lf)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 /. (i2 + lg) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . (i2 + lg) is set
(Y_axis l1) . (i2 + lg) is set
(G * (i1,(i2 + lg))) `2 is V11() V12() ext-real Element of REAL
l1 /. (i2 + lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l1 . (i2 + lf) is set
(Y_axis l1) . (i2 + lf) is set
(G * (i1,(i2 + lf))) `2 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lg) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lf) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g2,lg)) /\ (LSeg (g2,lf)) is Element of bool the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & x `2 <= b₁ `2 & b<sub>1</sub> `2 <= p1 `2 ) } is set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & ma `2 <= b₁ `2 & b<sub>1</sub> `2 <= ma `2 ) } is set
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
the Element of (LSeg (g2,lg)) /\ (LSeg (g2,lf)) is Element of (LSeg (g2,lg)) /\ (LSeg (g2,lf))
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
q2 `2 is V11() V12() ext-real Element of REAL
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
L~ g2 is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g2,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g2 ) } is set
union { (LSeg (g2,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g2 ) } is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & p1 `2 <= b<sub>1</sub> `2 & b₁ `2 <= ma `2 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (p1,ma) is Element of bool the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
qa `2 is V11() V12() ext-real Element of REAL
(X_axis l1) . j2 is set
(G * (i1,j2)) `1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + (lg + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + (lg + 1))) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 + (lg + 1))] is set
{i1,(i2 + (lg + 1))} is set
{{i1,(i2 + (lg + 1))},{i1}} is set
i2 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lg)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 + lg)] is set
{i1,(i2 + lg)} is set
{{i1,(i2 + lg)},{i1}} is set
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
(i2 + lg) - (i2 + (lg + 1)) is V11() V12() ext-real V71() set
abs ((i2 + lg) - (i2 + (lg + 1))) is V11() V12() ext-real Element of REAL
0 + (abs ((i2 + lg) - (i2 + (lg + 1)))) is V11() V12() ext-real set
- 1 is V11() V12() ext-real non positive V71() set
abs (- 1) is V11() V12() ext-real Element of REAL
abs 1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lg,lf] is set
{lg,lf} is set
{lg} is non empty trivial V40(1) set
{{lg,lf},{lg}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
G * (lg,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + 1)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 + 1)] is set
{i1,(i2 + 1)} is set
{{i1,(i2 + 1)},{i1}} is set
lg - x is V11() V12() ext-real V71() set
abs (lg - x) is V11() V12() ext-real Element of REAL
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V11() V12() ext-real set
i2 - (i2 + 1) is V11() V12() ext-real V71() set
abs (i2 - (i2 + 1)) is V11() V12() ext-real Element of REAL
0 + (abs (i2 - (i2 + 1))) is V11() V12() ext-real set
i2 - i2 is V11() V12() ext-real V71() set
(i2 - i2) + (- 1) is V11() V12() ext-real V71() set
abs ((i2 - i2) + (- 1)) is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
|[((G * (i1,j2)) `1),((G * (i1,j2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (c₄,g) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),(G * (i1,j2))) is Element of bool the U1 of (TOP-REAL 2)
rng g2 is set
lg is set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lf)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(G * (i1,(i2 + lf))) `2 is V11() V12() ext-real Element of REAL
(G * (i1,(i2 + lf))) `1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + lg)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[i1,(i2 + lg)] is set
{i1,(i2 + lg)} is set
{{i1,(i2 + lg)},{i1}} is set
(rng g1) /\ (rng g2) is set
the Element of (rng g1) /\ (rng g2) is Element of (rng g1) /\ (rng g2)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lg) is Element of bool the U1 of (TOP-REAL 2)
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g2,lg)) /\ (LSeg (g2,(lg + 1))) is Element of bool the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g2 /. (lg + 1))} is non empty trivial V40(1) set
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `1 is V11() V12() ext-real Element of REAL
lf `2 is V11() V12() ext-real Element of REAL
g2 /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
(lg + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lg + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lf,x) is Element of bool the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
LSeg (p1,lf) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & p1 `2 <= b<sub>1</sub> `2 & b₁ `2 <= x `2 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((g2 /. lg),(g2 /. (lg + 2))) is Element of bool the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lg + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,lg) is Element of bool the U1 of (TOP-REAL 2)
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lg)) /\ (LSeg (g,(lg + 1))) is Element of bool the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g /. (lg + 1))} is non empty trivial V40(1) set
(lg + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(lg + 2) - (len g1) is V11() V12() ext-real V71() set
lg - (len g1) is V11() V12() ext-real V71() set
(lg - (len g1)) + 2 is V11() V12() ext-real V71() set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lg + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g1 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g1,lg) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lg + 2) - 1 is V11() V12() ext-real V71() set
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
(len g) - (len g1) is V11() V12() ext-real V71() set
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `1 is V11() V12() ext-real Element of REAL
lf `2 is V11() V12() ext-real Element of REAL
LSeg ((G * (i1,i2)),lf) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,lg) is Element of bool the U1 of (TOP-REAL 2)
g /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
x `2 is V11() V12() ext-real Element of REAL
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),x) is Element of bool the U1 of (TOP-REAL 2)
g2 /. 2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= b<sub>1</sub> `2 & b₁ `2 <= p1 `2 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),p1) is Element of bool the U1 of (TOP-REAL 2)
g /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lf + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g2,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
lg is set
x is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,p1) is Element of bool the U1 of (TOP-REAL 2)
p1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (p1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (L~ g2) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (L~ g1) /\ (L~ g2) is Element of (L~ g1) /\ (L~ g2)
g /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,p1) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg `1 is V11() V12() ext-real Element of REAL
lg `2 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ((len g1) + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
|[(lg `1),(lg `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & (G * (i1,i2)) `2 <= b<sub>1</sub> `2 & b₁ `2 <= lg `2 ) } is set
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,(len g1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),lg) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
qa1 is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
lma `2 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of (LSeg (g,p1)) /\ (LSeg (g,ma))
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(qa + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
p1 - (len g1) is V11() V12() ext-real V71() set
(p1 - (len g1)) + 1 is V11() V12() ext-real V71() set
(p1 + 1) - (len g1) is V11() V12() ext-real V71() set
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (qa + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of (LSeg (g,p1)) /\ (LSeg (g,ma))
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = (G * (i1,i2)) `1 & lma `2 <= b<sub>1</sub> `2 & b₁ `2 <= q2 `2 ) } is set
lma `1 is V11() V12() ext-real Element of REAL
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
|[(q2 `1),(q2 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lma,q2) is Element of bool the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
q1l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q1l `1 is V11() V12() ext-real Element of REAL
q1l `2 is V11() V12() ext-real Element of REAL
c₃₆ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₆ `1 is V11() V12() ext-real Element of REAL
c<sub>36</sub> `2 is V11() V12() ext-real Element of REAL
LSeg (g2,qa1) is Element of bool the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(g2 /. 1) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `2 is V11() V12() ext-real Element of REAL
(g2 /. 1) `2 is V11() V12() ext-real Element of REAL
L~ g is Element of bool the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x - (len g1) is V11() V12() ext-real V71() set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
x is set
p1 is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
qa `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (qa,ma) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = ma `1 & qa `2 <= b<sub>1</sub> `2 & b₁ `2 <= ma `2 ) } is set
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
qa1 `2 is V11() V12() ext-real Element of REAL
{ma} is non empty trivial V40(1) set
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `1 = ma `1 & ma `2 <= b<sub>1</sub> `2 & b₁ `2 <= qa `2 ) } is set
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
qa1 `2 is V11() V12() ext-real Element of REAL
x is set
(L~ (c₄ | g)) \/ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `1 is V11() V12() ext-real Element of REAL
p1 `2 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
ma - 1 is V11() V12() ext-real V71() set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
qa1 `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & qa1 `2 <= b₁ `2 & b<sub>1</sub> `2 <= (G * (i1,j2)) `2 ) } is set
i2 + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (qa1,(G * (i1,j2))) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `1 = (G * (i1,i2)) `1 & qa `2 <= b₁ `2 & b<sub>1</sub> `2 <= qa1 `2 ) } is set
qa1 `1 is V11() V12() ext-real Element of REAL
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
qa `1 is V11() V12() ext-real Element of REAL
|[(qa `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (qa,qa1) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(len g1) + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. (len g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i2 + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (i1,(i2 + l)) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ l is Element of bool the U1 of (TOP-REAL 2)
len l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (l,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len l ) } is set
union { (LSeg (l,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len l ) } is set
l /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l /. (len l) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ g2 is Element of bool the U1 of (TOP-REAL 2)
len g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g2,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
union { (LSeg (g2,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
g2 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (len g2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (j1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 /. i1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . i1 is set
(X_axis c1) . i1 is set
(G * (i1,i2)) `1 is V11() V12() ext-real Element of REAL
c1 /. j1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . j1 is set
(X_axis c1) . j1 is set
(G * (j1,i2)) `1 is V11() V12() ext-real Element of REAL
i1 - j1 is V11() V12() ext-real V71() set
(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= b₁ `1 & b<sub>1</sub> `1 <= (G * (i1,i2)) `1 ) } is set
|[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg l is V33() V40(l) Element of bool NAT
i1 - g is V11() V12() ext-real V71() set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 - l is V11() V12() ext-real V71() set
[(i1 - g),i2] is set
{(i1 - g),i2} is set
{(i1 - g)} is non empty trivial V40(1) set
{{(i1 - g),i2},{(i1 - g)}} is set
g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
i1 - g is V11() V12() ext-real V71() set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (lk,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (lf,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g1 ^ g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom g is Element of bool NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 - lg is V11() V12() ext-real V71() set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom lk is Element of bool NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
Seg (len g) is V33() V40( len g) Element of bool NAT
(Y_axis c1) . i1 is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 - lg is V11() V12() ext-real V71() set
i1 - (len g) is V11() V12() ext-real V71() set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (x,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(Y_axis c1) . x is set
c1 /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . x is set
(X_axis c1) . x is set
(G * (x,i2)) `1 is V11() V12() ext-real Element of REAL
(G * (x,i2)) `2 is V11() V12() ext-real Element of REAL
lf `2 is V11() V12() ext-real Element of REAL
lf `1 is V11() V12() ext-real Element of REAL
rng c1 is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g /. lg) `1 is V11() V12() ext-real Element of REAL
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g /. (lg + 1)) `1 is V11() V12() ext-real Element of REAL
(g /. lg) `2 is V11() V12() ext-real Element of REAL
(g /. (lg + 1)) `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 - lg is V11() V12() ext-real V71() set
i1 - lf is V11() V12() ext-real V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (ma,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (ma,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . ma is set
(X_axis c1) . ma is set
(G * (ma,i2)) `1 is V11() V12() ext-real Element of REAL
c1 /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . ma is set
(X_axis c1) . ma is set
(G * (ma,i2)) `1 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lg) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of bool the U1 of (TOP-REAL 2)
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & p1 `1 <= b₁ `1 & b<sub>1</sub> `1 <= x `1 ) } is set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & ma `1 <= b₁ `1 & b<sub>1</sub> `1 <= ma `1 ) } is set
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
the Element of (LSeg (g,lg)) /\ (LSeg (g,lf)) is Element of (LSeg (g,lg)) /\ (LSeg (g,lf))
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (p1,x) is Element of bool the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
q2 `1 is V11() V12() ext-real Element of REAL
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
L~ g is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
union { (LSeg (g,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g ) } is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & ma `1 <= b<sub>1</sub> `1 & b₁ `1 <= p1 `1 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,p1) is Element of bool the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
qa `1 is V11() V12() ext-real Element of REAL
(Y_axis c1) . j1 is set
(G * (j1,i2)) `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 - lg is V11() V12() ext-real V71() set
i1 - lf is V11() V12() ext-real V71() set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (x,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (p1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 - lg),i2] is set
{(i1 - lg),i2} is set
{(i1 - lg)} is non empty trivial V40(1) set
{{(i1 - lg),i2},{(i1 - lg)}} is set
[(i1 - lf),i2] is set
{(i1 - lf),i2} is set
{(i1 - lf)} is non empty trivial V40(1) set
{{(i1 - lf),i2},{(i1 - lf)}} is set
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
|[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (c₄,g) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (j1,i2)),(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)
rng g is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 - x is V11() V12() ext-real V71() set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (p1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(G * (p1,i2)) `1 is V11() V12() ext-real Element of REAL
(G * (p1,i2)) `2 is V11() V12() ext-real Element of REAL
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
i1 - lf is V11() V12() ext-real V71() set
i1 - (lf + 1) is V11() V12() ext-real V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[ma,ma] is set
{ma,ma} is set
{ma} is non empty trivial V40(1) set
{{ma,ma},{ma}} is set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[qa,qa1] is set
{qa,qa1} is set
{qa} is non empty trivial V40(1) set
{{qa,qa1},{qa}} is set
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (qa,qa1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 - (lf + 1)),i2] is set
{(i1 - (lf + 1)),i2} is set
{(i1 - (lf + 1))} is non empty trivial V40(1) set
{{(i1 - (lf + 1)),i2},{(i1 - (lf + 1))}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (p1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 - lf),i2] is set
{(i1 - lf),i2} is set
{(i1 - lf)} is non empty trivial V40(1) set
{{(i1 - lf),i2},{(i1 - lf)}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (x,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma - qa is V11() V12() ext-real V71() set
abs (ma - qa) is V11() V12() ext-real Element of REAL
ma - qa1 is V11() V12() ext-real V71() set
abs (ma - qa1) is V11() V12() ext-real Element of REAL
(abs (ma - qa)) + (abs (ma - qa1)) is V11() V12() ext-real set
(i1 - lf) - (i1 - (lf + 1)) is V11() V12() ext-real V71() set
abs ((i1 - lf) - (i1 - (lf + 1))) is V11() V12() ext-real Element of REAL
(abs ((i1 - lf) - (i1 - (lf + 1)))) + 0 is V11() V12() ext-real set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 - 1 is V11() V12() ext-real V71() set
[(i1 - 1),i2] is set
{(i1 - 1),i2} is set
{(i1 - 1)} is non empty trivial V40(1) set
{{(i1 - 1),i2},{(i1 - 1)}} is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (ma,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
i1 - (i1 - 1) is V11() V12() ext-real V71() set
abs (i1 - (i1 - 1)) is V11() V12() ext-real Element of REAL
(abs (i1 - (i1 - 1))) + 0 is V11() V12() ext-real set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[ma,ma] is set
{ma,ma} is set
{ma} is non empty trivial V40(1) set
{{ma,ma},{ma}} is set
lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (ma,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
p1 - ma is V11() V12() ext-real V71() set
abs (p1 - ma) is V11() V12() ext-real Element of REAL
(abs (x - ma)) + (abs (p1 - ma)) is V11() V12() ext-real set
LSeg ((G * (i1,i2)),(G * (j1,i2))) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 - lf is V11() V12() ext-real V71() set
[(i1 - lf),i2] is set
{(i1 - lf),i2} is set
{(i1 - lf)} is non empty trivial V40(1) set
{{(i1 - lf),i2},{(i1 - lf)}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (x,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(rng g1) /\ (rng g) is set
the Element of (rng g1) /\ (rng g) is Element of (rng g1) /\ (rng g)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lf)) /\ (LSeg (g,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)
g /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g /. (lf + 1))} is non empty trivial V40(1) set
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
g /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
g /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
LSeg (ma,x) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & p1 `1 <= b<sub>1</sub> `1 & b₁ `1 <= ma `1 ) } is set
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((g /. lf),(g /. (lf + 2))) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lf + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,lf)) /\ (LSeg (lk,(lf + 1))) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(lk /. (lf + 1))} is non empty trivial V40(1) set
(lf + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(lf + 2) - (len g1) is V11() V12() ext-real V71() set
lf - (len g1) is V11() V12() ext-real V71() set
(lf - (len g1)) + 2 is V11() V12() ext-real V71() set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g1 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lf + 2) - 1 is V11() V12() ext-real V71() set
(len lk) - (len g1) is V11() V12() ext-real V71() set
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
LSeg ((G * (i1,i2)),x) is Element of bool the U1 of (TOP-REAL 2)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,lf) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
lk /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),p1) is Element of bool the U1 of (TOP-REAL 2)
g /. 2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & ma `1 <= b<sub>1</sub> `1 & b₁ `1 <= (G * (i1,i2)) `1 ) } is set
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),(g /. 2)) is Element of bool the U1 of (TOP-REAL 2)
lk /. (lf + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (p1,ma) is Element of bool the U1 of (TOP-REAL 2)
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(x + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,(x + 1)) is Element of bool the U1 of (TOP-REAL 2)
lf is set
p1 is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,qa) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (L~ g) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (L~ g1) /\ (L~ g) is Element of (L~ g1) /\ (L~ g)
lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
j1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `2 is V11() V12() ext-real Element of REAL
lf `1 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lk /. ((len g1) + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
|[(lf `1),(lf `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & lf `1 <= b<sub>1</sub> `1 & b₁ `1 <= (G * (i1,i2)) `1 ) } is set
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,(len g1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (lf,(G * (i1,i2))) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
lma is set
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
q2 `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(qa1 + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,qa1) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
(ma - (len g1)) + 1 is V11() V12() ext-real V71() set
(ma + 1) - (len g1) is V11() V12() ext-real V71() set
lma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (qa1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma)) is Element of (LSeg (lk,ma)) /\ (LSeg (lk,ma))
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & x `1 <= b<sub>1</sub> `1 & b₁ `1 <= q2 `1 ) } is set
q2 `2 is V11() V12() ext-real Element of REAL
|[(q2 `1),(q2 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (x,q2) is Element of bool the U1 of (TOP-REAL 2)
lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
c₃₆ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₆ `2 is V11() V12() ext-real Element of REAL
c<sub>36</sub> `1 is V11() V12() ext-real Element of REAL
c₃₇ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₇ `2 is V11() V12() ext-real Element of REAL
c<sub>37</sub> `1 is V11() V12() ext-real Element of REAL
LSeg (g,lma) is Element of bool the U1 of (TOP-REAL 2)
lma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
j1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(g /. 1) `2 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `1 is V11() V12() ext-real Element of REAL
(g /. 1) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `2 is V11() V12() ext-real Element of REAL
L~ lk is Element of bool the U1 of (TOP-REAL 2)
len lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (lk,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len lk ) } is set
union { (LSeg (lk,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len lk ) } is set
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 - (len g1) is V11() V12() ext-real V71() set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
Seg (len c1) is V33() V40( len c1) Element of bool NAT
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
p1 is set
ma is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (lk,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
qa `1 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
qa1 `1 is V11() V12() ext-real Element of REAL
|[(qa1 `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(qa `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (qa1,qa) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = qa `2 & qa1 `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa `1 ) } is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
lma `1 is V11() V12() ext-real Element of REAL
{qa} is non empty trivial V40(1) set
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = qa `2 & qa `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa1 `1 ) } is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
lma `1 is V11() V12() ext-real Element of REAL
p1 is set
(L~ (c₄ | g)) \/ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa - 1 is V11() V12() ext-real V71() set
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
lma `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & (G * (j1,i2)) `1 <= b₁ `1 & b<sub>1</sub> `1 <= lma `1 ) } is set
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lk,qa1) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (j1,i2)),lma) is Element of bool the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lk /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (qa + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & lma `1 <= b₁ `1 & b<sub>1</sub> `1 <= qa1 `1 ) } is set
lma `2 is V11() V12() ext-real Element of REAL
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `1 is V11() V12() ext-real Element of REAL
qa1 `2 is V11() V12() ext-real Element of REAL
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lk,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (lma,qa1) is Element of bool the U1 of (TOP-REAL 2)
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + (len g) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lk /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lk /. (len lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * (lg,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 /. i1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . i1 is set
(X_axis c1) . i1 is set
(G * (i1,i2)) `1 is V11() V12() ext-real Element of REAL
c1 /. j1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . j1 is set
(X_axis c1) . j1 is set
(G * (j1,i2)) `1 is V11() V12() ext-real Element of REAL
j1 - i1 is V11() V12() ext-real V71() set
l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom g2 is Element of bool NAT
g1 ^ g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
Seg l is V33() V40(l) Element of bool NAT
l + i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[(i1 + lk),i2] is set
{(i1 + lk),i2} is set
{(i1 + lk)} is non empty trivial V40(1) set
{{(i1 + lk),i2},{(i1 + lk)}} is set
Seg (len g2) is V33() V40( len g2) Element of bool NAT
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lg,lf] is set
{lg,lf} is set
{lg} is non empty trivial V40(1) set
{{lg,lf},{lg}} is set
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lg,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom g is Element of bool NAT
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(Y_axis c1) . i1 is set
(G * (i1,i2)) `2 is V11() V12() ext-real Element of REAL
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lk),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(Y_axis c1) . (i1 + lk) is set
c1 /. (i1 + lk) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . (i1 + lk) is set
(X_axis c1) . (i1 + lk) is set
(G * ((i1 + lk),i2)) `1 is V11() V12() ext-real Element of REAL
i1 + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(G * ((i1 + lk),i2)) `2 is V11() V12() ext-real Element of REAL
lg `2 is V11() V12() ext-real Element of REAL
lg `1 is V11() V12() ext-real Element of REAL
rng c1 is set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lk + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g2 /. lk) `1 is V11() V12() ext-real Element of REAL
g2 /. (lk + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(g2 /. (lk + 1)) `1 is V11() V12() ext-real Element of REAL
(g2 /. lk) `2 is V11() V12() ext-real Element of REAL
(g2 /. (lk + 1)) `2 is V11() V12() ext-real Element of REAL
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lk),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lg),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 + lk),i2] is set
{(i1 + lk),i2} is set
{(i1 + lk)} is non empty trivial V40(1) set
{{(i1 + lk),i2},{(i1 + lk)}} is set
[(i1 + lg),i2] is set
{(i1 + lg),i2} is set
{(i1 + lg)} is non empty trivial V40(1) set
{{(i1 + lg),i2},{(i1 + lg)}} is set
lk is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lk is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= b₁ `1 & b<sub>1</sub> `1 <= (G * (j1,i2)) `1 ) } is set
|[((G * (i1,i2)) `1),((G * (i1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i1 + lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lg),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * ((i1 + lf),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 /. (i1 + lg) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . (i1 + lg) is set
(X_axis c1) . (i1 + lg) is set
(G * ((i1 + lg),i2)) `1 is V11() V12() ext-real Element of REAL
c1 /. (i1 + lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c1 . (i1 + lf) is set
(X_axis c1) . (i1 + lf) is set
(G * ((i1 + lf),i2)) `1 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lg) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lf) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g2,lg)) /\ (LSeg (g2,lf)) is Element of bool the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & x `1 <= b₁ `1 & b<sub>1</sub> `1 <= p1 `1 ) } is set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & ma `1 <= b₁ `1 & b<sub>1</sub> `1 <= ma `1 ) } is set
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
the Element of (LSeg (g2,lg)) /\ (LSeg (g2,lf)) is Element of (LSeg (g2,lg)) /\ (LSeg (g2,lf))
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
q2 `1 is V11() V12() ext-real Element of REAL
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
L~ g2 is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g2,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g2 ) } is set
union { (LSeg (g2,b<sub>1</sub>)) where b<sub>1</sub> is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b<sub>1</sub> & b<sub>1</sub> + 1 <= len g2 ) } is set
lf is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,x) is Element of bool the U1 of (TOP-REAL 2)
x + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (x + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & p1 `1 <= b<sub>1</sub> `1 & b₁ `1 <= ma `1 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (p1,ma) is Element of bool the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
qa `1 is V11() V12() ext-real Element of REAL
(Y_axis c1) . j1 is set
(G * (j1,i2)) `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + (lg + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
G * ((i1 + (lg + 1)),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 + (lg + 1)),i2] is set
{(i1 + (lg + 1)),i2} is set
{(i1 + (lg + 1))} is non empty trivial V40(1) set
{{(i1 + (lg + 1)),i2},{(i1 + (lg + 1))}} is set
i1 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lg),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 + lg),i2] is set
{(i1 + lg),i2} is set
{(i1 + lg)} is non empty trivial V40(1) set
{{(i1 + lg),i2},{(i1 + lg)}} is set
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
(i1 + lg) - (i1 + (lg + 1)) is V11() V12() ext-real V71() set
abs ((i1 + lg) - (i1 + (lg + 1))) is V11() V12() ext-real Element of REAL
(abs ((i1 + lg) - (i1 + (lg + 1)))) + 0 is V11() V12() ext-real set
- 1 is V11() V12() ext-real non positive V71() set
abs (- 1) is V11() V12() ext-real Element of REAL
abs 1 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lg,lf] is set
{lg,lf} is set
{lg} is non empty trivial V40(1) set
{{lg,lf},{lg}} is set
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[x,p1] is set
{x,p1} is set
{x} is non empty trivial V40(1) set
{{x,p1},{x}} is set
G * (lg,lf) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (x,p1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
G * ((i1 + 1),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 + 1),i2] is set
{(i1 + 1),i2} is set
{(i1 + 1)} is non empty trivial V40(1) set
{{(i1 + 1),i2},{(i1 + 1)}} is set
lg - x is V11() V12() ext-real V71() set
abs (lg - x) is V11() V12() ext-real Element of REAL
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
(abs (lg - x)) + (abs (lf - p1)) is V11() V12() ext-real set
i1 - (i1 + 1) is V11() V12() ext-real V71() set
abs (i1 - (i1 + 1)) is V11() V12() ext-real Element of REAL
(abs (i1 - (i1 + 1))) + 0 is V11() V12() ext-real set
i1 - i1 is V11() V12() ext-real V71() set
(i1 - i1) + (- 1) is V11() V12() ext-real V71() set
abs ((i1 - i1) + (- 1)) is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[lf,x] is set
{lf,x} is set
{lf} is non empty trivial V40(1) set
{{lf,x},{lf}} is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[p1,ma] is set
{p1,ma} is set
{p1} is non empty trivial V40(1) set
{{p1,ma},{p1}} is set
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (lf,x) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (p1,ma) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf - p1 is V11() V12() ext-real V71() set
abs (lf - p1) is V11() V12() ext-real Element of REAL
x - ma is V11() V12() ext-real V71() set
abs (x - ma) is V11() V12() ext-real Element of REAL
(abs (lf - p1)) + (abs (x - ma)) is V11() V12() ext-real set
|[((G * (j1,i2)) `1),((G * (j1,i2)) `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (c₄,g) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),(G * (j1,i2))) is Element of bool the U1 of (TOP-REAL 2)
rng g2 is set
lg is set
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lf),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(G * ((i1 + lf),i2)) `1 is V11() V12() ext-real Element of REAL
(G * ((i1 + lf),i2)) `2 is V11() V12() ext-real Element of REAL
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + lg),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
[(i1 + lg),i2] is set
{(i1 + lg),i2} is set
{(i1 + lg)} is non empty trivial V40(1) set
{{(i1 + lg),i2},{(i1 + lg)}} is set
(rng g1) /\ (rng g2) is set
the Element of (rng g1) /\ (rng g2) is Element of (rng g1) /\ (rng g2)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lg + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,lg) is Element of bool the U1 of (TOP-REAL 2)
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g2,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g2,lg)) /\ (LSeg (g2,(lg + 1))) is Element of bool the U1 of (TOP-REAL 2)
g2 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g2 /. (lg + 1))} is non empty trivial V40(1) set
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `2 is V11() V12() ext-real Element of REAL
lf `1 is V11() V12() ext-real Element of REAL
g2 /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
(lg + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lg + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (lf,x) is Element of bool the U1 of (TOP-REAL 2)
g2 /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
LSeg (p1,lf) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & p1 `1 <= b<sub>1</sub> `1 & b₁ `1 <= x `1 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(x `1),(x `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((g2 /. lg),(g2 /. (lg + 2))) is Element of bool the U1 of (TOP-REAL 2)
lg is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
lg + 2 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,lg) is Element of bool the U1 of (TOP-REAL 2)
lg + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,lg)) /\ (LSeg (g,(lg + 1))) is Element of bool the U1 of (TOP-REAL 2)
g /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
{(g /. (lg + 1))} is non empty trivial V40(1) set
(lg + 1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(lg + 2) - (len g1) is V11() V12() ext-real V71() set
lg - (len g1) is V11() V12() ext-real V71() set
(lg - (len g1)) + 2 is V11() V12() ext-real V71() set
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
lg + (1 + 1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g1 /. (lg + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g1,lg) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,(lg + 1)) is Element of bool the U1 of (TOP-REAL 2)
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lg + 2) - 1 is V11() V12() ext-real V71() set
(len g) - (len g1) is V11() V12() ext-real V71() set
lf is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lf `2 is V11() V12() ext-real Element of REAL
lf `1 is V11() V12() ext-real Element of REAL
LSeg ((G * (i1,i2)),lf) is Element of bool the U1 of (TOP-REAL 2)
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,lg) is Element of bool the U1 of (TOP-REAL 2)
1 + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
x `2 is V11() V12() ext-real Element of REAL
x `1 is V11() V12() ext-real Element of REAL
g /. lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),x) is Element of bool the U1 of (TOP-REAL 2)
g2 /. 2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= b<sub>1</sub> `1 & b₁ `1 <= p1 `1 ) } is set
|[(p1 `1),(p1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),p1) is Element of bool the U1 of (TOP-REAL 2)
g /. (lg + 2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (x,p1) is Element of bool the U1 of (TOP-REAL 2)
lf is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
lf + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,lf) is Element of bool the U1 of (TOP-REAL 2)
lf + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(lf + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. (lf + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g2,(lf + 1)) is Element of bool the U1 of (TOP-REAL 2)
lg is set
x is set
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,p1) is Element of bool the U1 of (TOP-REAL 2)
p1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g2 /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (p1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (ma,ma) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (L~ g2) is Element of bool the U1 of (TOP-REAL 2)
(L~ g1) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (L~ g1) /\ (L~ g2) is Element of (L~ g1) /\ (L~ g2)
g /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,p1) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lg `2 is V11() V12() ext-real Element of REAL
lg `1 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ((len g1) + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
|[(lg `1),(lg `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & (G * (i1,i2)) `1 <= b<sub>1</sub> `1 & b₁ `1 <= lg `1 ) } is set
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,(len g1)) is Element of bool the U1 of (TOP-REAL 2)
LSeg ((G * (i1,i2)),lg) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
ma - (len g1) is V11() V12() ext-real V71() set
qa1 is set
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `2 is V11() V12() ext-real Element of REAL
lma `1 is V11() V12() ext-real Element of REAL
1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(L~ (c₄ | g)) /\ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of (LSeg (g,p1)) /\ (LSeg (g,ma))
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(qa + 1) + (len g1) is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
qa + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g2,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
p1 - (len g1) is V11() V12() ext-real V71() set
(p1 - (len g1)) + 1 is V11() V12() ext-real V71() set
(p1 + 1) - (len g1) is V11() V12() ext-real V71() set
qa1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
qa1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (qa + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of bool the U1 of (TOP-REAL 2)
the Element of (LSeg (g,p1)) /\ (LSeg (g,ma)) is Element of (LSeg (g,p1)) /\ (LSeg (g,ma))
lma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
lma `1 is V11() V12() ext-real Element of REAL
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = (G * (i1,i2)) `2 & lma `1 <= b<sub>1</sub> `1 & b₁ `1 <= q2 `1 ) } is set
lma `2 is V11() V12() ext-real Element of REAL
|[(lma `1),(lma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `2 is V11() V12() ext-real Element of REAL
|[(q2 `1),(q2 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (lma,q2) is Element of bool the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
q1l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q1l `2 is V11() V12() ext-real Element of REAL
q1l `1 is V11() V12() ext-real Element of REAL
c₃₆ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₃₆ `2 is V11() V12() ext-real Element of REAL
c<sub>36</sub> `1 is V11() V12() ext-real Element of REAL
LSeg (g2,qa1) is Element of bool the U1 of (TOP-REAL 2)
qa1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
(g2 /. 1) `2 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `1 is V11() V12() ext-real Element of REAL
(g2 /. 1) `1 is V11() V12() ext-real Element of REAL
(g1 /. (len g1)) `2 is V11() V12() ext-real Element of REAL
L~ g is Element of bool the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
(len g1) + (len g2) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
x - (len g1) is V11() V12() ext-real V71() set
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. x is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (len g1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
p1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
p1 + (len g1) is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g2 /. p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
x is set
p1 is set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
LSeg (g1,ma) is Element of bool the U1 of (TOP-REAL 2)
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma `2 is V11() V12() ext-real Element of REAL
ma `1 is V11() V12() ext-real Element of REAL
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `2 is V11() V12() ext-real Element of REAL
qa `1 is V11() V12() ext-real Element of REAL
|[(qa `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
|[(ma `1),(ma `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (qa,ma) is Element of bool the U1 of (TOP-REAL 2)
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = ma `2 & qa `1 <= b<sub>1</sub> `1 & b₁ `1 <= ma `1 ) } is set
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
qa1 `1 is V11() V12() ext-real Element of REAL
{ma} is non empty trivial V40(1) set
{ b₁ where b₁ is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b₁ `2 = ma `2 & ma `1 <= b<sub>1</sub> `1 & b₁ `1 <= qa `1 ) } is set
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
qa1 `1 is V11() V12() ext-real Element of REAL
x is set
(L~ (c₄ | g)) \/ (LSeg (c₄,g)) is Element of bool the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
p1 `2 is V11() V12() ext-real Element of REAL
p1 `1 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() set
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
(len g1) + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
ma - 1 is V11() V12() ext-real V71() set
qa is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `2 is V11() V12() ext-real Element of REAL
qa1 `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & qa1 `1 <= b₁ `1 & b<sub>1</sub> `1 <= (G * (j1,i2)) `1 ) } is set
i1 + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,qa) is Element of bool the U1 of (TOP-REAL 2)
LSeg (qa1,(G * (j1,i2))) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
ma + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
g /. ma is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (ma + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa `1 is V11() V12() ext-real Element of REAL
qa1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
qa1 `1 is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2) : ( b<sub>1</sub> `2 = (G * (i1,i2)) `2 & qa `1 <= b₁ `1 & b<sub>1</sub> `1 <= qa1 `1 ) } is set
qa1 `2 is V11() V12() ext-real Element of REAL
|[(qa1 `1),(qa1 `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
q2 `1 is V11() V12() ext-real Element of REAL
qa `2 is V11() V12() ext-real Element of REAL
|[(qa `1),(qa `2)]| is non empty V16() V19( NAT ) Function-like V33() V40(2) FinSequence-like FinSubsequence-like V126() Element of the U1 of (TOP-REAL 2)
LSeg (g,ma) is Element of bool the U1 of (TOP-REAL 2)
LSeg (qa,qa1) is Element of bool the U1 of (TOP-REAL 2)
ma is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
(len g1) + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
g /. (len g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. l is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
i1 + l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
G * ((i1 + l),i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ l is Element of bool the U1 of (TOP-REAL 2)
len l is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (l,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len l ) } is set
union { (LSeg (l,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len l ) } is set
l /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
l /. (len l) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ g2 is Element of bool the U1 of (TOP-REAL 2)
len g2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g2,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
union { (LSeg (g2,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g2 ) } is set
g2 /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g2 /. (len g2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ppi is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ ppi is Element of bool the U1 of (TOP-REAL 2)
len ppi is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (ppi,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len ppi ) } is set
union { (LSeg (ppi,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len ppi ) } is set
ppi /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
ppi /. (len ppi) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
dom g is Element of bool NAT
L~ g is Element of bool the U1 of (TOP-REAL 2)
{ (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (len g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₄ is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ c₄ is Element of bool the U1 of (TOP-REAL 2)
len c₄ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (c₄,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₄ ) } is set
union { (LSeg (c₄,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len c₄ ) } is set
c₄ /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₄ /. (len c₄) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
dom c₄ is Element of bool NAT
f1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
f1 + 1 is non empty V4() V5() V6() V10() V11() V12() ext-real positive non negative V33() V38() V71() Element of NAT
j1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
j2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[j1,j2] is set
{j1,j2} is set
{j1} is non empty trivial V40(1) set
{{j1,j2},{j1}} is set
i1 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
i2 is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
[i1,i2] is set
{i1,i2} is set
{i1} is non empty trivial V40(1) set
{{i1,i2},{i1}} is set
c₄ /. f1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (j1,j2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
c₄ /. (f1 + 1) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G * (i1,i2) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
j1 - i1 is V11() V12() ext-real V71() set
abs (j1 - i1) is V11() V12() ext-real Element of REAL
j2 - i2 is V11() V12() ext-real V71() set
abs (j2 - i2) is V11() V12() ext-real Element of REAL
(abs (j1 - i1)) + (abs (j2 - i2)) is V11() V12() ext-real set
f is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom f is Element of bool NAT
L~ f is Element of bool the U1 of (TOP-REAL 2)
len f is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (f,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
union { (LSeg (f,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len f ) } is set
f /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
f /. (len f) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
G is V16() non empty-yielding V19( NAT ) V20(K292( the U1 of (TOP-REAL 2))) Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K292( the U1 of (TOP-REAL 2))
Indices G is set
g is V16() V19( NAT ) V20( the U1 of (TOP-REAL 2)) Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
L~ g is Element of bool the U1 of (TOP-REAL 2)
len g is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT
{ (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
union { (LSeg (g,b₁)) where b₁ is V4() V5() V6() V10() V11() V12() ext-real non negative V33() V38() V71() Element of NAT : ( 1 <= b₁ & b₁ + 1 <= len g ) } is set
g /. 1 is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)
g /. (len g) is V40(2) FinSequence-like V126() Element of the U1 of (TOP-REAL 2)