REAL is V110() V111() V112() V116() set
NAT is V110() V111() V112() V113() V114() V115() V116() Element of bool REAL
bool REAL is non empty set
COMPLEX is V110() V116() set
NAT is V110() V111() V112() V113() V114() V115() V116() set
bool NAT is non empty set
bool NAT is non empty set
RAT is V110() V111() V112() V113() V116() set
INT is V110() V111() V112() V113() V114() V116() set
1 is non empty V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:1,1:] is non empty V18() set
bool [:1,1:] is non empty non empty-membered set
[:[:1,1:],1:] is non empty V18() set
bool [:[:1,1:],1:] is non empty non empty-membered set
[:[:1,1:],REAL:] is V18() set
bool [:[:1,1:],REAL:] is non empty set
[:REAL,REAL:] is V18() set
[:[:REAL,REAL:],REAL:] is V18() set
bool [:[:REAL,REAL:],REAL:] is non empty set
2 is non empty V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
[:2,2:] is non empty V18() set
[:[:2,2:],REAL:] is V18() set
bool [:[:2,2:],REAL:] is non empty set
bool [:REAL,REAL:] is non empty set
TOP-REAL 2 is non empty TopSpace-like V148() V173() V174() V175() V176() V177() V178() V179() strict RLTopStruct
the carrier of (TOP-REAL 2) is set
K304( the carrier of (TOP-REAL 2)) is non empty functional FinSequence-membered M14( the carrier of (TOP-REAL 2))
bool the carrier of (TOP-REAL 2) is non empty set
3 is non empty V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
{} is set
the empty trivial V18() non-empty empty-yielding functional finite finite-yielding V47() FinSequence-like FinSequence-membered V110() V111() V112() V113() V114() V115() V116() set is empty trivial V18() non-empty empty-yielding functional finite finite-yielding V47() FinSequence-like FinSequence-membered V110() V111() V112() V113() V114() V115() V116() set
0 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
Seg 1 is non empty finite 1 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
{1} is trivial finite V110() V111() V112() V113() V114() V115() set
Seg 2 is non empty finite 2 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
{1,2} is finite V110() V111() V112() V113() V114() V115() set
card {} is cardinal set
{{}} is trivial finite set
f1 is V18() V21( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom f1 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
Seg (len f1) is finite len f1 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
f2 is set
{f2} is trivial finite set
f1 is V18() V21( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
dom f1 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 -' 1 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
1 - 1 is V14() V15() integer ext-real set
1 -' 1 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
2 * 0 is V13() V14() V15() integer even ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
(2 * 0) + 1 is non empty V13() V14() V15() integer non even ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
TOP-REAL f1 is non empty TopSpace-like V148() V173() V174() V175() V176() V177() V178() V179() strict RLTopStruct
the carrier of (TOP-REAL f1) is set
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL f1)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL f1)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
rng f2 is finite set
g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 /. g1 is f1 -element FinSequence-like V101() Element of the carrier of (TOP-REAL f1)
f2 /. (g1 + 1) is f1 -element FinSequence-like V101() Element of the carrier of (TOP-REAL f1)
dom f2 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
f2 . g1 is set
f2 . (g1 + 1) is set
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,g1) is Element of bool the carrier of (TOP-REAL 2)
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f1 ^' f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
2 - 1 is V14() V15() integer ext-real set
(len f2) - 1 is V14() V15() integer ext-real set
g2 is V13() V14() V15() integer ext-real set
g1 is V13() V14() V15() integer ext-real set
g1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,g1) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,g2) is Element of bool the carrier of (TOP-REAL 2)
g2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg ((f1 ^' f2),g2) is Element of bool the carrier of (TOP-REAL 2)
len (f1 ^' f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
(len (f1 ^' f2)) + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
(len f1) + (len f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
((len (f1 ^' f2)) + 1) - 1 is V14() V15() integer ext-real set
(len f1) + ((len f2) - 1) is V14() V15() integer ext-real set
LSeg ((f1 ^' f2),g1) is Element of bool the carrier of (TOP-REAL 2)
g1 is V13() V14() V15() integer ext-real set
g1 + 2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,g1) is Element of bool the carrier of (TOP-REAL 2)
g1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,(g1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g1)) /\ (LSeg (f1,(g1 + 1))) is Element of bool the carrier of (TOP-REAL 2)
f1 /. (g1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{(f1 /. (g1 + 1))} is trivial finite set
(g1 + 1) + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg ((f1 ^' f2),(g1 + 1)) is Element of bool the carrier of (TOP-REAL 2)
dom (f1 ^' f2) is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
LSeg ((f1 ^' f2),g1) is Element of bool the carrier of (TOP-REAL 2)
dom f1 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
f1 . (g1 + 1) is set
(f1 ^' f2) . (g1 + 1) is set
(f1 ^' f2) /. (g1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f1 ^' f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ (f1 ^' f2) is Element of bool the carrier of (TOP-REAL 2)
len (f1 ^' f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg ((f1 ^' f2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (f1 ^' f2) ) } is set
union { (LSeg ((f1 ^' f2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (f1 ^' f2) ) } is set
g1 is set
g2 is set
p1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,p1) is Element of bool the carrier of (TOP-REAL 2)
p1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg ((f1 ^' f2),p1) is Element of bool the carrier of (TOP-REAL 2)
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
TOP-REAL f1 is non empty TopSpace-like V148() V173() V174() V175() V176() V177() V178() V179() strict RLTopStruct
the carrier of (TOP-REAL f1) is set
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
TOP-REAL f1 is non empty TopSpace-like V148() V173() V174() V175() V176() V177() V178() V179() strict RLTopStruct
the carrier of (TOP-REAL f1) is set
g2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL f1)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL f1)
p1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL f1)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL f1)
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
Seg f1 is finite f1 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g1 | (Seg f1) is V18() V21( Seg f1) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
[:NAT, the carrier of (TOP-REAL 2):] is V18() set
bool [:NAT, the carrier of (TOP-REAL 2):] is non empty set
g2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g1 | f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len g2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
dom (g1 | f1) is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
g2 /. p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 /. p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g2 /. (p1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 /. (p1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (g2,p1) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((g2 /. p1),(g2 /. (p1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the carrier of (TOP-REAL 2)
L~ f2 is Element of bool the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
union { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
(L~ f2) /\ (LSeg (g2,p1)) is Element of bool the carrier of (TOP-REAL 2)
p1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
LSeg (f2,p1) is Element of bool the carrier of (TOP-REAL 2)
(L~ g1) /\ (LSeg (f2,p1)) is Element of bool the carrier of (TOP-REAL 2)
L~ g2 is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (g2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g2 ) } is set
union { (LSeg (g2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g2 ) } is set
(L~ g2) /\ (LSeg (f2,p1)) is Element of bool the carrier of (TOP-REAL 2)
rng f2 is finite set
rng g1 is finite set
rng g2 is finite set
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f1 ^' f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g1 ^' g2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
p1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
len (f1 ^' f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
L~ (g1 ^' g2) is Element of bool the carrier of (TOP-REAL 2)
len (g1 ^' g2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg ((g1 ^' g2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (g1 ^' g2) ) } is set
union { (LSeg ((g1 ^' g2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (g1 ^' g2) ) } is set
LSeg ((f1 ^' f2),p1) is Element of bool the carrier of (TOP-REAL 2)
(L~ (g1 ^' g2)) /\ (LSeg ((f1 ^' f2),p1)) is Element of bool the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
(L~ g1) /\ (LSeg ((f1 ^' f2),p1)) is Element of bool the carrier of (TOP-REAL 2)
p1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
L~ (f1 ^' f2) is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg ((f1 ^' f2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (f1 ^' f2) ) } is set
union { (LSeg ((f1 ^' f2),b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len (f1 ^' f2) ) } is set
LSeg ((g1 ^' g2),p1) is Element of bool the carrier of (TOP-REAL 2)
(L~ (f1 ^' f2)) /\ (LSeg ((g1 ^' g2),p1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g1,p1) is Element of bool the carrier of (TOP-REAL 2)
(L~ (f1 ^' f2)) /\ (LSeg (g1,p1)) is Element of bool the carrier of (TOP-REAL 2)
rng (f1 ^' f2) is finite set
rng (g1 ^' g2) is finite set
rng g1 is finite set
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f2 is Element of bool the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
union { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
(L~ f2) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ f2) is set
g1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 . f1 is set
g1 . (f1 + 1) is set
rng g1 is finite set
dom g1 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
((L~ f2) `) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ ((L~ f2) `) is set
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
rng f2 is finite set
g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,g1) is Element of bool the carrier of (TOP-REAL 2)
g2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f2,g2) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g1)) /\ (LSeg (f2,g2)) is Element of bool the carrier of (TOP-REAL 2)
L~ f2 is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
union { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
rng f1 is finite set
f1 /. g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 /. (g1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((f1 /. g1),(f1 /. (g1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f2 /. g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 /. (g2 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((f2 /. g2),(f2 /. (g2 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
s2 is set
a is set
c1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
s is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((f2 /. g2),c1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (c1,(f2 /. (g2 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg ((f2 /. g2),c1)) \/ (LSeg (c1,(f2 /. (g2 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
LSeg (c1,(f1 /. g1)) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg ((f1 /. g1),c1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (c1,(f1 /. (g1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg ((f1 /. g1),c1)) \/ (LSeg (c1,(f1 /. (g1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
LSeg (c1,(f2 /. g2)) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
INTERSECTION ( { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } , { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } ) is set
{ H1(b1,b2) where b1, b2 is Element of bool the carrier of (TOP-REAL 2) : ( b1 in { (LSeg (f1,b1)) where b3 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } & b2 in { (LSeg (f2,b1)) where b3 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } ) } is set
q1 is set
q2 is set
c is set
q2 /\ c is set
s is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,s) is Element of bool the carrier of (TOP-REAL 2)
s + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f2,c1) is Element of bool the carrier of (TOP-REAL 2)
c1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
s2 is Element of bool the carrier of (TOP-REAL 2)
a is Element of bool the carrier of (TOP-REAL 2)
s2 /\ a is Element of bool the carrier of (TOP-REAL 2)
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f2 is Element of bool the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
union { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
(L~ f1) /\ (L~ f2) is Element of bool the carrier of (TOP-REAL 2)
p1 is set
INTERSECTION ( { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } , { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } ) is set
p2 is set
q1 is set
p2 /\ q1 is set
q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f1,q2) is Element of bool the carrier of (TOP-REAL 2)
q2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f2,c) is Element of bool the carrier of (TOP-REAL 2)
c + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
union (INTERSECTION ( { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } , { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } )) is set
f1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
f2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
L~ f2 is Element of bool the carrier of (TOP-REAL 2)
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
union { (LSeg (f2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f2 ) } is set
(L~ f1) /\ (L~ f2) is Element of bool the carrier of (TOP-REAL 2)
g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f2,g1) is Element of bool the carrier of (TOP-REAL 2)
(L~ f1) /\ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
((L~ f1) /\ (L~ f2)) /\ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
(L~ f2) /\ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
(L~ f1) /\ ((L~ f2) /\ (LSeg (f2,g1))) is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
(L~ f1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ f1) is set
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
g2 is Element of bool the carrier of (TOP-REAL 2)
f1 is set
f2 is set
g1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
(L~ g1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ g1) is set
RightComp g1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp g1 is Element of bool the carrier of (TOP-REAL 2)
g2 is Element of bool the carrier of (TOP-REAL 2)
f1 is set
f2 is set
g1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
(L~ g1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ g1) is set
LeftComp g1 is Element of bool the carrier of (TOP-REAL 2)
RightComp g1 is Element of bool the carrier of (TOP-REAL 2)
(LeftComp g1) \/ (RightComp g1) is Element of bool the carrier of (TOP-REAL 2)
(LeftComp g1) \/ (RightComp g1) is Element of bool the carrier of (TOP-REAL 2)
g2 is Element of bool the carrier of (TOP-REAL 2)
g2 is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
(L~ f1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ f1) is set
f2 is set
g1 is set
g2 is set
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
(L~ f1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ f1) is set
f2 is set
g1 is set
g2 is set
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
p1 is Element of bool the carrier of (TOP-REAL 2)
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
v_strip (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g2 `1 is V14() V15() ext-real Element of REAL
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
p1 is set
p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p2 `1 is V14() V15() ext-real Element of REAL
p2 `2 is V14() V15() ext-real Element of REAL
|[(p2 `1),(p2 `2)]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * (1,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (1,1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : b1 <= (f1 * (1,1)) `1 } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * ((len f1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * ((len f1),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : (f1 * ((len f1),1)) `1 <= b1 } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * (f2,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (f2,1)) `1 is V14() V15() ext-real Element of REAL
f2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 * ((f2 + 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * ((f2 + 1),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( (f1 * (f2,1)) `1 <= b1 & b1 <= (f1 * ((f2 + 1),1)) `1 ) } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
len f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
v_strip (f2,f1) is Element of bool the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g2 `1 is V14() V15() ext-real Element of REAL
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
width f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
h_strip (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 `2 is V14() V15() ext-real Element of REAL
g2 `2 is V14() V15() ext-real Element of REAL
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
p1 is set
p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p2 `2 is V14() V15() ext-real Element of REAL
p2 `1 is V14() V15() ext-real Element of REAL
|[(p2 `1),(p2 `2)]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * (1,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (1,1)) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : b2 <= (f1 * (1,1)) `2 } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * (1,(width f1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (1,(width f1))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : (f1 * (1,(width f1))) `2 <= b2 } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 * (1,f2) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (1,f2)) `2 is V14() V15() ext-real Element of REAL
f2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 * (1,(f2 + 1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(f1 * (1,(f2 + 1))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( (f1 * (1,f2)) `2 <= b2 & b2 <= (f1 * (1,(f2 + 1))) `2 ) } is set
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
q1 is V14() V15() ext-real Element of REAL
q2 is V14() V15() ext-real Element of REAL
|[q1,q2]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
width f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
h_strip (f2,f1) is Element of bool the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (g2,p1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g2 `2 is V14() V15() ext-real Element of REAL
p1 `2 is V14() V15() ext-real Element of REAL
f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
width g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell (g1,f1,f2) is Element of bool the carrier of (TOP-REAL 2)
v_strip (g1,f1) is Element of bool the carrier of (TOP-REAL 2)
h_strip (g1,f2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip (g1,f1)) /\ (h_strip (g1,f2)) is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
left_cell (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
GoB f1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
len (GoB f1) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
width (GoB f1) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
g2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB f1),g1,g2) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f1),g1) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f1),g2) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f1),g1)) /\ (h_strip ((GoB f1),g2)) is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
GoB f1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
f2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
left_cell (f1,f2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f1,f2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
left_cell (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
(len f1) -' f2 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
((len f1) -' f2) + f2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
right_cell (f1,f2) is Element of bool the carrier of (TOP-REAL 2)
Rev f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
left_cell ((Rev f1),((len f1) -' f2)) is Element of bool the carrier of (TOP-REAL 2)
len (Rev f1) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
((len f1) -' f2) + 1 is V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
(L~ g1) /\ (LSeg (f1,f2)) is Element of bool the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
p1 is set
{p1} is trivial finite set
p1 is set
{p1} is trivial finite set
p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f1,p2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (p2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,p2)) \/ (LSeg (p2,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g2)) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
{g2} is trivial finite set
LSeg (p2,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (p2,g2)) /\ (LSeg (g2,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g2)) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
{g2} is trivial finite set
LSeg (p2,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (p2,g2)) /\ (LSeg (g2,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g2)) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
{g2} is trivial finite set
LSeg (p2,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (p2,g2)) /\ (LSeg (g2,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,g2)) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
{g2} is trivial finite set
LSeg (p2,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (p2,g2)) /\ (LSeg (g2,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f2,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
q1 is set
q1 is set
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g1 is Element of bool the carrier of (TOP-REAL 2)
len g1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
union { (LSeg (g1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g1 ) } is set
(L~ g1) /\ (LSeg (f1,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ g1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ g1) is set
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ g1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ g1) is set
LSeg (f1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
p1 is set
{p1} is trivial finite set
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f1 `1 is V14() V15() ext-real Element of REAL
g1 `1 is V14() V15() ext-real Element of REAL
(LSeg (f1,f2)) /\ (LSeg (g1,g2)) is Element of bool the carrier of (TOP-REAL 2)
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p1 `1 is V14() V15() ext-real Element of REAL
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 `2 is V14() V15() ext-real Element of REAL
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `2 is V14() V15() ext-real Element of REAL
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 `2 is V14() V15() ext-real Element of REAL
LSeg (f1,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
g1 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
g1 `1 is V14() V15() ext-real Element of REAL
f2 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
f2 `1 is V14() V15() ext-real Element of REAL
g1 `1 is V14() V15() ext-real Element of REAL
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() V15() ext-real Element of REAL
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
LSeg (f1,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f2 `2 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (f2,f1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f2,f1)) \/ (LSeg (f1,g1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,f2)) \/ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 `1 is V14() V15() ext-real Element of REAL
g2 `2 is V14() V15() ext-real Element of REAL
LSeg (g2,f1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (g2,f2)) \/ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (g2,f1)) \/ (LSeg (f1,g1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (g2,g1)) \/ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
(LSeg (g2,f1)) \/ (LSeg (f1,f2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f1 `1 is V14() V15() ext-real Element of REAL
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 `1 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
g2 `2 is V14() V15() ext-real Element of REAL
LSeg (f1,f2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (f1,f2)) /\ (LSeg (g1,g2)) is Element of bool the carrier of (TOP-REAL 2)
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{p1} is trivial finite set
LSeg (g1,p1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
LSeg (p1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (g1,p1)) \/ (LSeg (p1,g2)) is Element of bool the carrier of (TOP-REAL 2)
f1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{f1} is trivial finite set
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
g2 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ g2 is Element of bool the carrier of (TOP-REAL 2)
len g2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (g2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g2 ) } is set
union { (LSeg (g2,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len g2 ) } is set
(L~ g2) /\ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
GoB g2 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
(L~ g2) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ g2) is set
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p1 `1 is V14() V15() ext-real Element of REAL
p1 `2 is V14() V15() ext-real Element of REAL
p2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
right_cell (g2,p2,(GoB g2)) is Element of bool the carrier of (TOP-REAL 2)
left_cell (g2,p2,(GoB g2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is Element of bool the carrier of (TOP-REAL 2)
p2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
right_cell (g2,p2,(GoB g2)) is Element of bool the carrier of (TOP-REAL 2)
left_cell (g2,p2,(GoB g2)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is Element of bool the carrier of (TOP-REAL 2)
(right_cell (g2,p2,(GoB g2))) \ (L~ g2) is Element of bool the carrier of (TOP-REAL 2)
RightComp g2 is Element of bool the carrier of (TOP-REAL 2)
LSeg (p1,f1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(left_cell (g2,p2,(GoB g2))) \ (L~ g2) is Element of bool the carrier of (TOP-REAL 2)
LeftComp g2 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q1 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
f1 is non empty V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like non constant finite FinSequence-like FinSubsequence-like V207( the carrier of (TOP-REAL 2)) special unfolded s.c.c. standard FinSequence of the carrier of (TOP-REAL 2)
L~ f1 is Element of bool the carrier of (TOP-REAL 2)
len f1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
union { (LSeg (f1,b1)) where b1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT : ( 1 <= b1 & b1 + 1 <= len f1 ) } is set
GoB f1 is V18() non empty-yielding V21( NAT ) V22(K304( the carrier of (TOP-REAL 2))) Function-like finite FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K304( the carrier of (TOP-REAL 2))
(L~ f1) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ f1) is set
f2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 `1 is V14() V15() ext-real Element of REAL
f2 `2 is V14() V15() ext-real Element of REAL
g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (f2,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ f1) /\ (LSeg (f2,g1)) is Element of bool the carrier of (TOP-REAL 2)
g1 `1 is V14() V15() ext-real Element of REAL
g1 `2 is V14() V15() ext-real Element of REAL
g2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{g2} is trivial finite set
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p1 `1 is V14() V15() ext-real Element of REAL
p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p2 `1 is V14() V15() ext-real Element of REAL
p1 `2 is V14() V15() ext-real Element of REAL
p2 `2 is V14() V15() ext-real Element of REAL
q1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
q1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
left_cell (f1,q1,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f1,q1,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,q1) is Element of bool the carrier of (TOP-REAL 2)
q1 is V13()