REAL is non empty V33() V146() V147() V148() V152() set
NAT is non empty V7() V8() V9() V33() V38() V39() V146() V147() V148() V149() V150() V151() V152() Element of bool REAL
bool REAL is V33() set
COMPLEX is non empty V33() V146() V152() set
NAT is non empty V7() V8() V9() V33() V38() V39() V146() V147() V148() V149() V150() V151() V152() set
bool NAT is V33() set
bool NAT is V33() set
1 is ext-real positive non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
INT is non empty V33() V146() V147() V148() V149() V150() V152() set
[:1,1:] is RAT -valued INT -valued V136() V137() V138() V139() set
RAT is non empty V33() V146() V147() V148() V149() V152() set
bool [:1,1:] is set
[:[:1,1:],1:] is RAT -valued INT -valued V136() V137() V138() V139() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is V136() V137() V138() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is V33() V136() V137() V138() set
[:[:REAL,REAL:],REAL:] is V33() V136() V137() V138() set
bool [:[:REAL,REAL:],REAL:] is V33() set
2 is ext-real positive non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[:2,2:] is RAT -valued INT -valued V136() V137() V138() V139() set
[:[:2,2:],REAL:] is V136() V137() V138() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is V33() set
TOP-REAL 2 is non empty TopSpace-like V112() V158() V159() V160() V161() V162() V163() V164() V170() L15()
the U1 of (TOP-REAL 2) is non empty set
bool the U1 of (TOP-REAL 2) is set
K179( the U1 of (TOP-REAL 2)) is non empty functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
{} is ext-real empty V7() V8() V9() V11() V12() V13() V14() V15() functional V33() V38() V40( {} ) FinSequence-membered V146() V147() V148() V149() V150() V151() V152() set
3 is ext-real positive non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
0 is ext-real empty V7() V8() V9() V11() V12() V13() V14() V15() functional V33() V38() V40( {} ) FinSequence-membered V83() V84() V146() V147() V148() V149() V150() V151() V152() Element of NAT
Seg 1 is non empty trivial V33() V40(1) V146() V147() V148() V149() V150() V151() Element of bool NAT
{1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
Seg 2 is non empty V33() V40(2) V146() V147() V148() V149() V150() V151() Element of bool NAT
{1,2} is non empty V146() V147() V148() V149() V150() V151() set
P1 is Relation-like non empty-yielding NAT -defined K179( the U1 of (TOP-REAL 2)) -valued Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K179( the U1 of (TOP-REAL 2))
Line (P1,1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width P1), the U1 of (TOP-REAL 2)))
width P1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K180((width P1), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line (P1,1)) is set
len P1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (P1,(len P1)) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width P1), the U1 of (TOP-REAL 2)))
rng (Line (P1,(len P1))) is set
Col (P1,1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len P1), the U1 of (TOP-REAL 2)))
K180((len P1), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col (P1,1)) is set
Col (P1,(width P1)) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len P1), the U1 of (TOP-REAL 2)))
rng (Col (P1,(width P1))) is set
P2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len P2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
P2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
P2 /. (len P2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng P2 is set
p1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len p1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p1 /. (len p1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng p1 is set
p2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p2 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 is Relation-like non empty-yielding NAT -defined K179( the U1 of (TOP-REAL 2)) -valued Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K179( the U1 of (TOP-REAL 2))
width q1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
K180((width q1), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line (q1,1)) is set
len q1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,(len q1)) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,(len q1))) is set
Col (q1,1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
K180((len q1), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col (q1,1)) is set
Col (q1,(width q1)) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
rng (Col (q1,(width q1))) is set
q2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len q2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (len q2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng q2 is set
f1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 /. (len f1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng f1 is set
(rng q2) /\ (rng f1) is set
dom f1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f1 /. f1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
f1 /. f1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f1 | f2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(f1 | f2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len (f1 | f2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
rng (f1 | f2) is set
x1 is set
dom (f1 | f2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
y1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. y1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg f2 is V33() V40(f2) V146() V147() V148() V149() V150() V151() Element of bool NAT
f1 /. y1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len f1) is V33() V40( len f1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (f1 | f2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg (len (f1 | f2)) is V33() V40( len (f1 | f2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
0 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom q1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
(f1 | f2) /. (len (f1 | f2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
Line (q1,x2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,x2)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,x2))) is set
Seg (width q1) is V33() V40( width q1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Col (q1,1)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
x2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(Col (q1,1)) . x2 is set
y2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,y2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,y2)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,y2))) is set
len (Col (q1,1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Col (q1,1))) is V33() V40( len (Col (q1,1))) V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg (len q1) is V33() V40( len q1) V146() V147() V148() V149() V150() V151() Element of bool NAT
(Line (q1,y2)) . 1 is set
len (Line (q1,y2)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom (Line (q1,y2)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
x2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
Line (q1,x2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,x2)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,x2))) is set
y2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
Line (q1,y2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,y2)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,y2))) is set
y2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
Line (q1,y2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
rng (Line (q1,y2)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,y2))) is set
n is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,n) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
dom q2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
rng (Line (q1,n)) is set
g2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
q2 /. g2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. g2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
q2 /. g2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
n - 1 is ext-real V14() V15() Element of REAL
(len q1) - q is ext-real V14() V15() Element of REAL
w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom g1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
m1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
g1 /. m1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len g1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len g1) is V33() V40( len g1) V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg (len q1) is V33() V40( len q1) V146() V147() V148() V149() V150() V151() Element of bool NAT
u is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. u is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom (Line (q1,n)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
h1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
g1 /. h1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len (Line (q1,n)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Col (q1,h1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
rng (Col (q1,h1)) is set
w is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. w is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len (Col (q1,h1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom (Col (q1,h1)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg (len (Line (q1,n))) is V33() V40( len (Line (q1,n))) V146() V147() V148() V149() V150() V151() Element of bool NAT
Lma is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom Lma is V146() V147() V148() V149() V150() V151() Element of bool NAT
mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Lma /. mi1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,mi1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
k2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len k2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom k2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
Lma . mi1 is set
k2 . h1 is set
k2 /. h1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng k2 is set
len Lma is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len Lma) is V33() V40( len Lma) V146() V147() V148() V149() V150() V151() Element of bool NAT
rng (Line (q1,mi1)) is set
(rng (f1 | f2)) /\ (rng (Line (q1,mi1))) is set
Col (q1,m1) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len h1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom h1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg (len q2) is V33() V40( len q2) V146() V147() V148() V149() V150() V151() Element of bool NAT
w is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom w is V146() V147() V148() V149() V150() V151() Element of bool NAT
Lma is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w /. Lma is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,Lma) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
len w is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
mi1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
rng mi1 is set
k2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. k2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len w) is V33() V40( len w) V146() V147() V148() V149() V150() V151() Element of bool NAT
w . Lma is set
dom mi1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
mi1 /. h2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len mi1) is V33() V40( len mi1) V146() V147() V148() V149() V150() V151() Element of bool NAT
mi1 . h2 is set
w5 - 1 is ext-real V14() V15() Element of REAL
Line (q1,q) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
Indices q1 is set
[:(dom q1),(Seg (width q1)):] is INT -valued RAT -valued V136() V137() V138() V139() set
mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
mi1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[(mi1 + 1),m1] is set
{(mi1 + 1),m1} is non empty V146() V147() V148() V149() V150() V151() set
{(mi1 + 1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(mi1 + 1),m1},{(mi1 + 1)}} is non empty set
k2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[k2,h2] is set
{k2,h2} is non empty V146() V147() V148() V149() V150() V151() set
{k2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{k2,h2},{k2}} is non empty set
Ck2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[Ck2,l] is set
{Ck2,l} is non empty V146() V147() V148() V149() V150() V151() set
{Ck2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{Ck2,l},{Ck2}} is non empty set
h1 /. mi1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (k2,h2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h1 /. (mi1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (Ck2,l) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((mi1 + 1),m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[mi1,m1] is set
{mi1,m1} is non empty V146() V147() V148() V149() V150() V151() set
{mi1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{mi1,m1},{mi1}} is non empty set
q1 * (mi1,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
k2 - Ck2 is ext-real V14() V15() Element of REAL
abs (k2 - Ck2) is ext-real V14() V15() Element of REAL
h2 - l is ext-real V14() V15() Element of REAL
abs (h2 - l) is ext-real V14() V15() Element of REAL
(abs (k2 - Ck2)) + (abs (h2 - l)) is ext-real V14() V15() Element of REAL
mi1 - mi1 is ext-real V14() V15() Element of REAL
- 1 is ext-real V14() V15() Element of REAL
(mi1 - mi1) + (- 1) is ext-real V14() V15() Element of REAL
abs ((mi1 - mi1) + (- 1)) is ext-real V14() V15() Element of REAL
(abs ((mi1 - mi1) + (- 1))) + 0 is ext-real V14() V15() Element of REAL
abs 1 is ext-real V14() V15() Element of REAL
rng h1 is set
(rng h1) /\ (rng (f1 | f2)) is set
the Element of (rng h1) /\ (rng (f1 | f2)) is Element of (rng h1) /\ (rng (f1 | f2))
k2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 /. k2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[k2,m1] is set
{k2,m1} is non empty V146() V147() V148() V149() V150() V151() set
{k2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{k2,m1},{k2}} is non empty set
h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. h2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Ck2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[Ck2,l] is set
{Ck2,l} is non empty V146() V147() V148() V149() V150() V151() set
{Ck2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{Ck2,l},{Ck2}} is non empty set
q1 * (Ck2,l) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,Ck2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
f1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len f1) is V33() V40( len f1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom f1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
f1 /. l is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 . l is set
rng f1 is set
(rng (f1 | f2)) /\ (rng f1) is set
q1 * (k2,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng (Line (q1,q)) is set
mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. mi1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
mi1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
q2 /. mi1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Lma is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom Lma is V146() V147() V148() V149() V150() V151() Element of bool NAT
k2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Lma /. k2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
s is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom h2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
Col (q1,k2) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
len Lma is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len Lma) is V33() V40( len Lma) V146() V147() V148() V149() V150() V151() Element of bool NAT
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l + q is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + s is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[f1,f] is set
{f1,f} is non empty V146() V147() V148() V149() V150() V151() set
{f1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{f1,f},{f1}} is non empty set
h2 /. l is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (f1,f) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + (l + 1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q + l) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[((q + l) + 1),k2] is set
{((q + l) + 1),k2} is non empty V146() V147() V148() V149() V150() V151() set
{((q + l) + 1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{((q + l) + 1),k2},{((q + l) + 1)}} is non empty set
f1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[f1,f] is set
{f1,f} is non empty V146() V147() V148() V149() V150() V151() set
{f1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{f1,f},{f1}} is non empty set
ff is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[ff,hf] is set
{ff,hf} is non empty V146() V147() V148() V149() V150() V151() set
{ff} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{ff,hf},{ff}} is non empty set
h2 /. l is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (f1,f) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h2 /. (l + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (ff,hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((q + (l + 1)),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[(q + l),k2] is set
{(q + l),k2} is non empty V146() V147() V148() V149() V150() V151() set
{(q + l)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(q + l),k2},{(q + l)}} is non empty set
q1 * ((q + l),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 - ff is ext-real V14() V15() Element of REAL
abs (f1 - ff) is ext-real V14() V15() Element of REAL
f - hf is ext-real V14() V15() Element of REAL
abs (f - hf) is ext-real V14() V15() Element of REAL
(abs (f1 - ff)) + (abs (f - hf)) is ext-real V14() V15() Element of REAL
(q + l) - (q + l) is ext-real V14() V15() Element of REAL
((q + l) - (q + l)) + (- 1) is ext-real V14() V15() Element of REAL
abs (((q + l) - (q + l)) + (- 1)) is ext-real V14() V15() Element of REAL
(abs (((q + l) - (q + l)) + (- 1))) + 0 is ext-real V14() V15() Element of REAL
mi1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
DelCol (q1,(width q1)) is Relation-like non empty-yielding NAT -defined K179( the U1 of (TOP-REAL 2)) -valued Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K179( the U1 of (TOP-REAL 2))
len (DelCol (q1,(width q1))) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(mi1 + 1) - w5 is ext-real V14() V15() Element of REAL
q2 | mi1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
w is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg l is V33() V40(l) V146() V147() V148() V149() V150() V151() Element of bool NAT
f is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
w + f is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + f) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len f is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w + l is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom f is V146() V147() V148() V149() V150() V151() Element of bool NAT
h1 ^ f is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
(h1 ^ f) ^ h2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
w5 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg mi1 is V33() V40(mi1) V146() V147() V148() V149() V150() V151() Element of bool NAT
w + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f ^ h2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
((h1 ^ f) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
len (Line (q1,1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
x1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom x1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Line (q1,1)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
x1 /. m1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x1 . m1 is set
len (h1 ^ f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len h1) + (len f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom (h1 ^ f) is V146() V147() V148() V149() V150() V151() Element of bool NAT
((h1 ^ f) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(h1 ^ f) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (1,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ f) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ f) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w + hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf + w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
l + w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(hf + w5) - 1 is ext-real V14() V15() Element of REAL
(w5 - 1) + hf is ext-real V14() V15() Element of REAL
Seg mi1 is V33() V40(mi1) V146() V147() V148() V149() V150() V151() Element of bool NAT
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w + hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[D,t] is set
{D,t} is non empty V146() V147() V148() V149() V150() V151() set
{D} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{D,t},{D}} is non empty set
q1 * (D,t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[tt,lg] is set
{tt,lg} is non empty V146() V147() V148() V149() V150() V151() set
{tt} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{tt,lg},{tt}} is non empty set
q1 * (tt,lg) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len f) is V33() V40( len f) V146() V147() V148() V149() V150() V151() Element of bool NAT
rng f is set
hf is set
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w + D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + D) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + D) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len h2) is V33() V40( len h2) V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg mi1 is V33() V40(mi1) V146() V147() V148() V149() V150() V151() Element of bool NAT
len ((h1 ^ f) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(len h1) + (len f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. ((len h1) + (len f)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. l is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. mi1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg s is V33() V40(s) V146() V147() V148() V149() V150() V151() Element of bool NAT
len (Line (q1,(len q1))) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
y1 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
dom y1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
y1 /. k2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
y1 . k2 is set
len ((h1 ^ f) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len (h1 ^ f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len (h1 ^ f)) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. ((len (h1 ^ f)) + (len h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h2 /. s is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((q + s),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len ((h1 ^ f) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len ((h1 ^ f) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ f) ^ h2) /. (len ((h1 ^ f) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
0 + 0 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len h1) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len f) + ((len h1) + (len h2)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
rng ((h1 ^ f) ^ h2) is set
rng (h1 ^ f) is set
rng h2 is set
(rng (h1 ^ f)) \/ (rng h2) is set
(rng h1) \/ (rng f) is set
((rng h1) \/ (rng f)) \/ (rng h2) is set
len (Col (q1,k2)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
len (Col (q1,m1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Col (q1,hf) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((len q1), the U1 of (TOP-REAL 2)))
rng (Col (q1,hf)) is set
(rng f) /\ (rng (Col (q1,hf))) is set
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (q1,hf))) is set
the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (q1,hf))) is Element of (rng ((h1 ^ f) ^ h2)) /\ (rng (Col (q1,hf)))
(rng h1) \/ (rng h2) is set
(rng f) \/ ((rng h1) \/ (rng h2)) is set
((rng h1) \/ (rng h2)) /\ (rng (Col (q1,hf))) is set
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (q1,hf)))) is set
(rng h1) /\ (rng (Col (q1,hf))) is set
(rng h2) /\ (rng (Col (q1,hf))) is set
((rng h1) /\ (rng (Col (q1,hf)))) \/ ((rng h2) /\ (rng (Col (q1,hf)))) is set
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 /. tt is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (tt,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 . m1 is set
dom (Col (q1,m1)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
u is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
u /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u . n is set
dom u is V146() V147() V148() V149() V150() V151() Element of bool NAT
u /. tt is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u . tt is set
lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng u is set
f /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 /. tt is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 * ((q + tt),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Lma . k2 is set
dom (Col (q1,k2)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
Ck2 is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
Ck2 /. q is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Ck2 . q is set
dom Ck2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
Ck2 /. (q + tt) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Ck2 . (q + tt) is set
lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng Ck2 is set
f /. l is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. (w + l) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + l) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(rng h2) /\ (rng (f1 | f2)) is set
the Element of (rng h2) /\ (rng (f1 | f2)) is Element of (rng h2) /\ (rng (f1 | f2))
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[(q + D),k2] is set
{(q + D),k2} is non empty V146() V147() V148() V149() V150() V151() set
{(q + D)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(q + D),k2},{(q + D)}} is non empty set
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. t is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[tt,lg] is set
{tt,lg} is non empty V146() V147() V148() V149() V150() V151() set
{tt} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{tt,lg},{tt}} is non empty set
q1 * (tt,lg) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,tt) is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like M11( the U1 of (TOP-REAL 2),K180((width q1), the U1 of (TOP-REAL 2)))
pf is Relation-like NAT -defined the U1 of (TOP-REAL 2) -valued Function-like V33() FinSequence-like FinSubsequence-like FinSequence of the U1 of (TOP-REAL 2)
len pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len pf) is V33() V40( len pf) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom pf is V146() V147() V148() V149() V150() V151() Element of bool NAT
pf /. lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pf . lg is set
rng pf is set
(rng (f1 | f2)) /\ (rng pf) is set
q1 * ((q + D),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(rng ((h1 ^ f) ^ h2)) /\ (rng (f1 | f2)) is set
((rng h1) \/ (rng f)) /\ (rng (f1 | f2)) is set
(((rng h1) \/ (rng f)) /\ (rng (f1 | f2))) \/ {} is set
(rng f) /\ (rng (f1 | f2)) is set
{} \/ ((rng f) /\ (rng (f1 | f2))) is set
DelCol (q1,1) is Relation-like non empty-yielding NAT -defined K179( the U1 of (TOP-REAL 2)) -valued Function-like V33() FinSequence-like FinSubsequence-like tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column FinSequence of K179( the U1 of (TOP-REAL 2))
len (DelCol (q1,1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom (DelCol (q1,1)) is V146() V147() V148() V149() V150() V151() Element of bool NAT
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w + hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. (hf + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w + (hf + 1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + (hf + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(w + hf) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. ((w + hf) + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[D,t] is set
{D,t} is non empty V146() V147() V148() V149() V150() V151() set
{D} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{D,t},{D}} is non empty set
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[tt,lg] is set
{tt,lg} is non empty V146() V147() V148() V149() V150() V151() set
{tt} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{tt,lg},{tt}} is non empty set
q1 * (D,t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (tt,lg) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
D - tt is ext-real V14() V15() Element of REAL
abs (D - tt) is ext-real V14() V15() Element of REAL
t - lg is ext-real V14() V15() Element of REAL
abs (t - lg) is ext-real V14() V15() Element of REAL
(abs (D - tt)) + (abs (t - lg)) is ext-real V14() V15() Element of REAL
len (h1 ^ f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len (h1 ^ f)) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(len h1) + (len f) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((len h1) + (len f)) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[D,t] is set
{D,t} is non empty V146() V147() V148() V149() V150() V151() set
{D} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{D,t},{D}} is non empty set
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[tt,lg] is set
{tt,lg} is non empty V146() V147() V148() V149() V150() V151() set
{tt} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{tt,lg},{tt}} is non empty set
(h1 ^ f) /. (len (h1 ^ f)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (D,t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (tt,lg) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom (h1 ^ f) is V146() V147() V148() V149() V150() V151() Element of bool NAT
q + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[(q + 1),k2] is set
{(q + 1),k2} is non empty V146() V147() V148() V149() V150() V151() set
{(q + 1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(q + 1),k2},{(q + 1)}} is non empty set
[q,k2] is set
{q,k2} is non empty V146() V147() V148() V149() V150() V151() set
{q} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{q,k2},{q}} is non empty set
Lma . k2 is set
(h1 ^ f) /. ((len h1) + (len f)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. (len f) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. (w + l) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (q,k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((q + 1),k2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
D - tt is ext-real V14() V15() Element of REAL
abs (D - tt) is ext-real V14() V15() Element of REAL
t - lg is ext-real V14() V15() Element of REAL
abs (t - lg) is ext-real V14() V15() Element of REAL
(abs (D - tt)) + (abs (t - lg)) is ext-real V14() V15() Element of REAL
q - (q + 1) is ext-real V14() V15() Element of REAL
abs (q - (q + 1)) is ext-real V14() V15() Element of REAL
(abs (q - (q + 1))) + 0 is ext-real V14() V15() Element of REAL
(q + 1) - q is ext-real V14() V15() Element of REAL
- ((q + 1) - q) is ext-real V14() V15() Element of REAL
abs (- ((q + 1) - q)) is ext-real V14() V15() Element of REAL
[n,m1] is set
{n,m1} is non empty V146() V147() V148() V149() V150() V151() set
{n} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{n,m1},{n}} is non empty set
g1 . m1 is set
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[D,t] is set
{D,t} is non empty V146() V147() V148() V149() V150() V151() set
{D} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{D,t},{D}} is non empty set
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[tt,lg] is set
{tt,lg} is non empty V146() V147() V148() V149() V150() V151() set
{tt} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{tt,lg},{tt}} is non empty set
h1 /. (len h1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (D,t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (tt,lg) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[m,m1] is set
{m,m1} is non empty V146() V147() V148() V149() V150() V151() set
{m} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{m,m1},{m}} is non empty set
w + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (n,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (m,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
D - tt is ext-real V14() V15() Element of REAL
abs (D - tt) is ext-real V14() V15() Element of REAL
t - lg is ext-real V14() V15() Element of REAL
abs (t - lg) is ext-real V14() V15() Element of REAL
(abs (D - tt)) + (abs (t - lg)) is ext-real V14() V15() Element of REAL
(n - 1) - n is ext-real V14() V15() Element of REAL
abs ((n - 1) - n) is ext-real V14() V15() Element of REAL
(abs ((n - 1) - n)) + 0 is ext-real V14() V15() Element of REAL
abs (- 1) is ext-real V14() V15() Element of REAL
D is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
D + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t is ext-real V7() V8() V9() V13() V14() V15()