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() 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)
(left_cell (f1,q1,(GoB f1))) \ (L~ f1) is Element of bool the carrier of (TOP-REAL 2)
LeftComp f1 is Element of bool the carrier of (TOP-REAL 2)
(right_cell (f1,q1,(GoB f1))) \ (L~ f1) is Element of bool the carrier of (TOP-REAL 2)
RightComp f1 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
q2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
left_cell (f1,q2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f1,q2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,q2) is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
q2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
left_cell (f1,q2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f1,q2,(GoB f1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg (f1,q2) is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 is Element of bool the carrier of (TOP-REAL 2)
q2 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 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~ 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
rng f2 is non empty finite 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 2 -element FinSequence-like V101() Element of 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)
LSeg (g1,g2) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ f2) /\ (LSeg (g1,g2)) is Element of bool 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,g1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
p1 is set
GoB 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))
q1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
LSeg (f2,q1) is Element of bool the carrier of (TOP-REAL 2)
q1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
Indices (GoB f2) is set
f2 /. q1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 /. (q1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
q2 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
[q2,c] is non empty set
{q2,c} is finite V110() V111() V112() V113() V114() V115() set
{q2} is trivial finite V110() V111() V112() V113() V114() V115() set
{{q2,c},{q2}} is finite V47() set
(GoB f2) * (q2,c) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
a is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
[s2,a] is non empty set
{s2,a} is finite V110() V111() V112() V113() V114() V115() set
{s2} is trivial finite V110() V111() V112() V113() V114() V115() set
{{s2,a},{s2}} is finite V47() set
(GoB f2) * (s2,a) is 2 -element FinSequence-like V101() Element of 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
q2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
s2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
a + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
dom f2 is non empty finite V110() V111() V112() V113() V114() V115() Element of bool NAT
f2 . (q1 + 1) is set
len (GoB f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
width (GoB f2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB f2),q2,c) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f2),q2) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f2),c) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),q2)) /\ (h_strip ((GoB f2),c)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),q2,c)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f2) * (q2,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (q2,1)) `1 is V14() V15() ext-real Element of REAL
(GoB f2) * ((q2 + 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * ((q2 + 1),1)) `1 is V14() V15() ext-real Element of REAL
(GoB f2) * (1,(width (GoB f2))) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,(width (GoB f2)))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (q2,1)) `1 & not ((GoB f2) * ((q2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,(width (GoB f2)))) `2 ) } is set
(GoB f2) * (1,c) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,c)) `2 is V14() V15() ext-real Element of REAL
(GoB f2) * (1,(c + 1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,(c + 1))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (q2,1)) `1 & not ((GoB f2) * ((q2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,c)) `2 & not ((GoB f2) * (1,(c + 1))) `2 <= b2 ) } is set
(GoB f2) * ((len (GoB f2)),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * ((len (GoB f2)),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * ((len (GoB f2)),1)) `1 & not b2 <= ((GoB f2) * (1,c)) `2 & not ((GoB f2) * (1,(c + 1))) `2 <= b2 ) } is set
cell ((GoB f2),s2,a) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f2),s2) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f2),a) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),s2)) /\ (h_strip ((GoB f2),a)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),s2,a)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f2) * (1,a) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,a)) `2 is V14() V15() ext-real Element of REAL
(GoB f2) * (1,(a + 1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,(a + 1))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * ((len (GoB f2)),1)) `1 & not b2 <= ((GoB f2) * (1,a)) `2 & not ((GoB f2) * (1,(a + 1))) `2 <= b2 ) } is set
(GoB f2) * (s2,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (s2,1)) `1 is V14() V15() ext-real Element of REAL
(GoB f2) * ((s2 + 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * ((s2 + 1),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (s2,1)) `1 & not ((GoB f2) * ((s2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,a)) `2 & not ((GoB f2) * (1,(a + 1))) `2 <= b2 ) } is set
cell ((GoB f2),s2,c) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),s2)) /\ (h_strip ((GoB f2),c)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),s2,c)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (s2,1)) `1 & not ((GoB f2) * ((s2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,(width (GoB f2)))) `2 ) } is set
f2 . q1 is set
c -' 1 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB f2),q2,(c -' 1)) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f2),(c -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),q2)) /\ (h_strip ((GoB f2),(c -' 1))) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),q2,(c -' 1))) is Element of bool the carrier of (TOP-REAL 2)
(GoB f2) * (1,(c -' 1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,(c -' 1))) `2 is V14() V15() ext-real Element of REAL
(c -' 1) + 1 is V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB f2) * (1,((c -' 1) + 1)) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,((c -' 1) + 1))) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (q2,1)) `1 & not ((GoB f2) * ((q2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,(c -' 1))) `2 & not ((GoB f2) * (1,((c -' 1) + 1))) `2 <= b2 ) } is set
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (s2,1)) `1 & not ((GoB f2) * ((s2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,c)) `2 & not ((GoB f2) * (1,(c + 1))) `2 <= b2 ) } is set
cell ((GoB f2),s2,(c -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),s2)) /\ (h_strip ((GoB f2),(c -' 1))) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),s2,(c -' 1))) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (s2,1)) `1 & not ((GoB f2) * ((s2 + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,(c -' 1))) `2 & not ((GoB f2) * (1,((c -' 1) + 1))) `2 <= b2 ) } is set
cell ((GoB f2),s2,0) is Element of bool the carrier of (TOP-REAL 2)
h_strip ((GoB f2),0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),s2)) /\ (h_strip ((GoB f2),0)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),s2,0)) is Element of bool the carrier of (TOP-REAL 2)
(GoB f2) * (1,1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (1,1)) `2 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (s2,1)) `1 & not ((GoB f2) * ((s2 + 1),1)) `1 <= b1 & not ((GoB f2) * (1,1)) `2 <= b2 ) } is set
left_cell (f2,q1,(GoB f2)) is Element of bool the carrier of (TOP-REAL 2)
Int (left_cell (f2,q1,(GoB f2))) is Element of bool the carrier of (TOP-REAL 2)
right_cell (f2,q1,(GoB f2)) is Element of bool the carrier of (TOP-REAL 2)
Int (right_cell (f2,q1,(GoB f2))) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f2 /. (q1 + 1)),(f2 /. q1)) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(f2 /. q1) `2 is V14() V15() ext-real Element of REAL
(f2 /. (q1 + 1)) `2 is V14() V15() ext-real Element of REAL
f1 `2 is V14() V15() ext-real Element of REAL
s2 -' 1 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB f2),(s2 -' 1),a) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f2),(s2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),(s2 -' 1))) /\ (h_strip ((GoB f2),a)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),(s2 -' 1),a)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f2),0,a) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f2),0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),0)) /\ (h_strip ((GoB f2),a)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),0,a)) is Element of bool the carrier of (TOP-REAL 2)
((GoB 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 : ( not ((GoB f2) * (1,1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,a)) `2 & not ((GoB f2) * (1,(a + 1))) `2 <= b2 ) } is set
(LSeg (g1,g2)) /\ (LSeg (f2,q1)) is Element of bool the carrier of (TOP-REAL 2)
LSeg ((f2 /. q1),(f2 /. (q1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(LSeg (g1,g2)) /\ (LSeg ((f2 /. q1),(f2 /. (q1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
q2 -' 1 is V13() V14() V15() integer ext-real non negative V109() V110() V111() V112() V113() V114() V115() Element of NAT
cell ((GoB f2),(q2 -' 1),c) is Element of bool the carrier of (TOP-REAL 2)
v_strip ((GoB f2),(q2 -' 1)) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),(q2 -' 1))) /\ (h_strip ((GoB f2),c)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),(q2 -' 1),c)) is Element of bool the carrier of (TOP-REAL 2)
cell ((GoB f2),0,c) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),0)) /\ (h_strip ((GoB f2),c)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),0,c)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not ((GoB f2) * (1,1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,c)) `2 & not ((GoB f2) * (1,(c + 1))) `2 <= b2 ) } is set
s 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)
cell ((GoB f2),q2,0) is Element of bool the carrier of (TOP-REAL 2)
(v_strip ((GoB f2),q2)) /\ (h_strip ((GoB f2),0)) is Element of bool the carrier of (TOP-REAL 2)
Int (cell ((GoB f2),q2,0)) is Element of bool the carrier of (TOP-REAL 2)
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * (q2,1)) `1 & not ((GoB f2) * ((q2 + 1),1)) `1 <= b1 & not ((GoB f2) * (1,1)) `2 <= b2 ) } is set
(f2 /. q1) `1 is V14() V15() ext-real Element of REAL
(f2 /. (q1 + 1)) `1 is V14() V15() ext-real Element of REAL
f1 `1 is V14() V15() ext-real Element of REAL
(GoB f2) * ((s2 -' 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * ((s2 -' 1),1)) `1 is V14() V15() ext-real Element of REAL
(s2 -' 1) + 1 is V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB f2) * (((s2 -' 1) + 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (((s2 -' 1) + 1),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * ((s2 -' 1),1)) `1 & not ((GoB f2) * (((s2 -' 1) + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,a)) `2 & not ((GoB f2) * (1,(a + 1))) `2 <= b2 ) } is set
((GoB f2) * (q2,c)) `1 is V14() V15() ext-real Element of REAL
(GoB f2) * (s2,c) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (s2,c)) `1 is V14() V15() ext-real Element of REAL
(GoB f2) * ((q2 -' 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * ((q2 -' 1),1)) `1 is V14() V15() ext-real Element of REAL
(q2 -' 1) + 1 is V13() V14() V15() integer ext-real positive V109() V110() V111() V112() V113() V114() V115() Element of NAT
(GoB f2) * (((q2 -' 1) + 1),1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
((GoB f2) * (((q2 -' 1) + 1),1)) `1 is V14() V15() ext-real Element of REAL
{ |[b1,b2]| where b1, b2 is V14() V15() ext-real Element of REAL : ( not b1 <= ((GoB f2) * ((q2 -' 1),1)) `1 & not ((GoB f2) * (((q2 -' 1) + 1),1)) `1 <= b1 & not b2 <= ((GoB f2) * (1,c)) `2 & not ((GoB f2) * (1,(c + 1))) `2 <= b2 ) } is set
s is set
c1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
c1 `1 is V14() V15() ext-real Element of REAL
|[(c1 `1),(f1 `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)
c is V14() V15() ext-real Element of REAL
rp9 is V14() V15() ext-real Element of REAL
|[c,rp9]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
c is V14() V15() ext-real Element of REAL
rp9 is V14() V15() ext-real Element of REAL
|[c,rp9]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c is set
rp9 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
rp9 `1 is V14() V15() ext-real Element of REAL
|[(rp9 `1),(f1 `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)
rp is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
rp `2 is V14() V15() ext-real Element of REAL
c2 `2 is V14() V15() ext-real Element of REAL
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
rp `1 is V14() V15() ext-real Element of REAL
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
s is set
c1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
c1 `2 is V14() V15() ext-real Element of REAL
|[(f1 `1),(c1 `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)
c2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
c2 `2 is V14() V15() ext-real Element of REAL
c is V14() V15() ext-real Element of REAL
rp9 is V14() V15() ext-real Element of REAL
|[c,rp9]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c is V14() V15() ext-real Element of REAL
rp9 is V14() V15() ext-real Element of REAL
|[c,rp9]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c is set
rp9 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
rp9 `2 is V14() V15() ext-real Element of REAL
|[(f1 `1),(rp9 `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)
c2 `1 is V14() V15() ext-real Element of REAL
rp is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
rp `1 is V14() V15() ext-real Element of REAL
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
rp `2 is V14() V15() ext-real Element of REAL
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is V14() V15() ext-real Element of REAL
c19 is V14() V15() ext-real Element of REAL
|[c18,c19]| is non empty V18() V21( NAT ) Function-like finite 2 -element FinSequence-like FinSubsequence-like V101() Element of the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
c18 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 V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like special 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
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 (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)
card ((L~ f1) /\ (LSeg (f2,g1))) is cardinal set
f2 . g1 is set
f2 . (g1 + 1) is set
dom f2 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
f2 /. g1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 /. (g1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((f2 /. g1),(f2 /. (g1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(f2 /. g1) `1 is V14() V15() ext-real Element of REAL
(f2 /. (g1 + 1)) `1 is V14() V15() ext-real Element of REAL
(f2 /. g1) `2 is V14() V15() ext-real Element of REAL
(f2 /. (g1 + 1)) `2 is V14() V15() ext-real Element of REAL
rng f2 is finite set
q2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
q1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg (q2,q1) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
c is set
{c} is trivial finite set
rng f1 is non empty finite set
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
(L~ f1) /\ (LSeg ((f2 /. g1),(f2 /. (g1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
s2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{s2} is trivial finite set
a 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)
2 * 0 is V13() V14() V15() integer even ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is Element of bool the carrier of (TOP-REAL 2)
s2 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 special 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 special 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 special 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
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
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
(L~ (f1 ^' f2)) /\ (L~ g1) is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ g1)) is cardinal set
(L~ (f1 ^' f2)) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ (f1 ^' f2)) is set
g1 . 1 is set
g1 . (len g1) is set
g2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like special unfolded s.n.c. s.c.c. FinSequence of the carrier of (TOP-REAL 2)
rng g2 is finite set
len g2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
dom g2 is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
Seg (len g2) is finite len g2 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p2 is V13() V14() V15() integer ext-real set
Seg p2 is finite p2 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
g2 | (Seg p2) is V18() V21( Seg p2) 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
p2 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
q1 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)
q1 . 1 is set
g2 . 1 is set
L~ q1 is Element of bool the carrier of (TOP-REAL 2)
len q1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (q1,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 q1 ) } is set
union { (LSeg (q1,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 q1 ) } is set
(L~ (f1 ^' f2)) /\ (L~ q1) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,p2) is Element of bool the carrier of (TOP-REAL 2)
(L~ (f1 ^' f2)) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
Seg (p2 + 1) is finite p2 + 1 -element V110() V111() V112() V113() V114() V115() Element of bool NAT
g2 . (p2 + 1) is set
g2 . p2 is set
a 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 | (Seg (p2 + 1)) is V18() V21( Seg (p2 + 1)) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
dom a is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
(dom g2) /\ (Seg (p2 + 1)) is finite V110() V111() V112() V113() V114() V115() Element of bool NAT
a . (p2 + 1) is set
len a is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
a . (len a) is set
a /. (p2 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 /. (p2 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 | (p2 + 1) is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like special unfolded s.n.c. s.c.c. FinSequence of the carrier of (TOP-REAL 2)
a | p2 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~ (a | p2) is Element of bool the carrier of (TOP-REAL 2)
len (a | p2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg ((a | p2),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 (a | p2) ) } is set
union { (LSeg ((a | p2),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 (a | p2) ) } is set
LSeg (a,p2) is Element of bool the carrier of (TOP-REAL 2)
(L~ (a | p2)) /\ (LSeg (a,p2)) is Element of bool the carrier of (TOP-REAL 2)
a /. p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
{(a /. p2)} is trivial finite set
LSeg ((a /. p2),(a /. (p2 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ (a | p2)) /\ (LSeg ((a /. p2),(a /. (p2 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
a . 1 is set
L~ a is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (a,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 a ) } is set
union { (LSeg (a,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 a ) } is set
(L~ (f1 ^' f2)) /\ (L~ a) is Element of bool the carrier of (TOP-REAL 2)
(g2 | (Seg (p2 + 1))) | (Seg p2) is V18() V21( Seg p2) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
g2 | p2 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)
q1 . (len q1) is set
q1 . p2 is set
a . p2 is set
g2 /. p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((g2 /. p2),(g2 /. (p2 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ q1) /\ (LSeg ((g2 /. p2),(g2 /. (p2 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
{(g2 /. p2)} is trivial finite set
(L~ q1) /\ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
{(g2 . p2)} is trivial finite set
q2 is finite set
s2 is finite set
c1 is set
L~ (g2 | p2) is Element of bool the carrier of (TOP-REAL 2)
len (g2 | p2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg ((g2 | p2),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 | p2) ) } is set
union { (LSeg ((g2 | p2),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 | p2) ) } is set
(L~ (g2 | p2)) \/ (LSeg ((g2 /. p2),(g2 /. (p2 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(L~ q1) \/ (LSeg ((g2 /. p2),(g2 /. (p2 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
(L~ q1) \/ (LSeg (g2,p2)) is Element of bool the carrier of (TOP-REAL 2)
s is finite set
q2 \/ s2 is finite set
card q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (L~ q1)) is cardinal set
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (LSeg (g2,p2))) is cardinal set
card s is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is V14() V15() integer ext-real set
c1 is V14() V15() integer even ext-real set
c2 is V14() V15() integer even ext-real set
c1 + c2 is V14() V15() integer even ext-real set
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
rp9 is Element of bool the carrier of (TOP-REAL 2)
rp is Element of bool the carrier of (TOP-REAL 2)
c18 is Element of bool the carrier of (TOP-REAL 2)
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (LSeg (g2,p2))) is cardinal set
card s is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is V14() V15() integer ext-real set
c1 is V14() V15() integer even ext-real set
c2 is non empty V14() V15() integer non even ext-real set
c1 + c2 is non empty V14() V15() integer non even ext-real set
rp9 is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
rp9 is Element of bool the carrier of (TOP-REAL 2)
rp is Element of bool the carrier of (TOP-REAL 2)
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
c2 is Element of bool the carrier of (TOP-REAL 2)
c is Element of bool the carrier of (TOP-REAL 2)
card q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (L~ q1)) is cardinal set
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (LSeg (g2,p2))) is cardinal set
card s is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is V14() V15() integer ext-real set
c1 is non empty V14() V15() integer non even ext-real set
c2 is V14() V15() integer even ext-real set
c1 + c2 is non empty V14() V15() integer non even ext-real set
rp9 is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
rp9 is Element of bool the carrier of (TOP-REAL 2)
rp is Element of bool the carrier of (TOP-REAL 2)
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (LSeg (g2,p2))) is cardinal set
card s is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
c is V14() V15() integer ext-real set
c1 is non empty V14() V15() integer non even ext-real set
c2 is non empty V14() V15() integer non even ext-real set
c1 + c2 is V14() V15() integer even ext-real set
rp9 is Element of bool the carrier of (TOP-REAL 2)
rp9 is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
rp9 is Element of bool the carrier of (TOP-REAL 2)
card s2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
card ((L~ (f1 ^' f2)) /\ (L~ a)) is cardinal set
c2 is Element of bool the carrier of (TOP-REAL 2)
c is Element of bool the carrier of (TOP-REAL 2)
card q2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
q1 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~ q1 is Element of bool the carrier of (TOP-REAL 2)
len q1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (q1,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 q1 ) } is set
union { (LSeg (q1,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 q1 ) } is set
(L~ (f1 ^' f2)) /\ (L~ q1) is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ q1)) is cardinal set
q1 . 1 is set
q1 . (len q1) is set
q2 is Element of bool the carrier of (TOP-REAL 2)
g2 | (Seg (len g2)) is V18() V21( Seg (len g2)) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
g2 | 1 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like special unfolded s.n.c. s.c.c. FinSequence of the carrier of (TOP-REAL 2)
g2 | (Seg 1) is V18() V21( Seg 1) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
len (g2 | 1) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p2 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 | (Seg 2) is V18() V21( Seg 2) V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSubsequence-like Element of bool [:NAT, the carrier of (TOP-REAL 2):]
len p2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
p2 . (len p2) is set
p2 . 2 is set
g2 . (1 + 1) is set
p2 . 1 is set
L~ p2 is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg (p2,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 p2 ) } is set
union { (LSeg (p2,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 p2 ) } is set
g2 | 2 is V18() V21( NAT ) V22( the carrier of (TOP-REAL 2)) Function-like finite FinSequence-like FinSubsequence-like special unfolded s.n.c. s.c.c. FinSequence of the carrier of (TOP-REAL 2)
L~ (g2 | 2) is Element of bool the carrier of (TOP-REAL 2)
len (g2 | 2) is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg ((g2 | 2),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 | 2) ) } is set
union { (LSeg ((g2 | 2),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 | 2) ) } is set
L~ (g2 | 1) is Element of bool the carrier of (TOP-REAL 2)
{ (LSeg ((g2 | 1),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 | 1) ) } is set
union { (LSeg ((g2 | 1),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 | 1) ) } is set
g2 /. 1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 /. (1 + 1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
LSeg ((g2 /. 1),(g2 /. (1 + 1))) is non empty V94( TOP-REAL 2) convex Element of bool the carrier of (TOP-REAL 2)
(L~ (g2 | 1)) \/ (LSeg ((g2 /. 1),(g2 /. (1 + 1)))) is Element of bool the carrier of (TOP-REAL 2)
LSeg (g2,1) is Element of bool the carrier of (TOP-REAL 2)
(L~ (g2 | 1)) \/ (LSeg (g2,1)) is Element of bool the carrier of (TOP-REAL 2)
{} \/ (LSeg (g2,1)) is set
(L~ (f1 ^' f2)) /\ (L~ p2) is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ p2)) is cardinal set
q1 is Element of bool the carrier of (TOP-REAL 2)
p2 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~ p2 is Element of bool the carrier of (TOP-REAL 2)
len p2 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
{ (LSeg (p2,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 p2 ) } is set
union { (LSeg (p2,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 p2 ) } is set
(L~ (f1 ^' f2)) /\ (L~ p2) is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ p2)) is cardinal set
p2 . 1 is set
p2 . (len p2) is set
q1 is Element of bool the carrier of (TOP-REAL 2)
p2 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 special 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 special 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 special 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 special 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)
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~ 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~ 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~ 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
f1 . 1 is set
f1 . (len f1) is set
g1 . 1 is set
g1 . (len g1) is set
f1 /. (len f1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
f2 /. 1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g1 /. (len g1) is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
g2 /. 1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
(L~ f1) /\ (L~ f2) is Element of bool the carrier of (TOP-REAL 2)
(L~ g1) /\ (L~ g2) is Element of bool 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
(L~ (f1 ^' f2)) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ (f1 ^' f2)) is set
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
(L~ (g1 ^' g2)) ` is Element of bool the carrier of (TOP-REAL 2)
the carrier of (TOP-REAL 2) \ (L~ (g1 ^' g2)) is set
p1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
p2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
q1 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
q2 is 2 -element FinSequence-like V101() Element of the carrier of (TOP-REAL 2)
1 + 1 is V13() V14() V15() integer ext-real V109() V110() V111() V112() V113() V114() V115() Element of NAT
(L~ (f1 ^' f2)) /\ (L~ g1) is Element of bool the carrier of (TOP-REAL 2)
card ((L~ (f1 ^' f2)) /\ (L~ g1)) is cardinal set
c is Element of bool the carrier of (TOP-REAL 2)
(L~ f1) \/ (L~ f2) is Element of bool the carrier of (TOP-REAL 2)
((L~ f1) \/ (L~ f2)) /\ (L~ g1) is Element of bool the carrier of (TOP-REAL 2)
(L~ f1) /\ (L~ g1) is Element of bool the carrier of (TOP-REAL 2)
(L~ f2) /\ (L~ g1) is Element of bool the carrier of (TOP-REAL 2)
((L~ f1) /\ (L~ g1)) \/ ((L~ f2) /\ (L~ g1)) is Element of bool the carrier of (TOP-REAL 2)
((L~ f1) /\ (L~ g1)) \/ {} is set
(L~ f1) /\ (L~ g2) is Element of bool the carrier of (TOP-REAL 2)
((L~ f1) /\ (L~ g1)) \/ ((L~ f1) /\ (L~ g2)) is Element of bool the carrier of (TOP-REAL 2)
(L~ g1) \/ (L~ g2) is Element of bool the carrier of (TOP-REAL 2)
((L~ g1) \/ (L~ g2)) /\ (L~ f1) is Element of bool the carrier of (TOP-REAL 2)
(L~ f1) /\ (L~ (g1 ^' g2)) is Element of bool the carrier of (TOP-REAL 2)