:: GOBOARD4 semantic presentation

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() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[t,tt] is set
{t,tt} is non empty V146() V147() V148() V149() V150() V151() set
{t} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{t,tt},{t}} is non empty set
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[lg,pf] is set
{lg,pf} is non empty V146() V147() V148() V149() V150() V151() set
{lg} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{lg,pf},{lg}} is non empty set
(h1 ^ f) /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (t,tt) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(h1 ^ f) /. (D + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (lg,pf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
t - lg is ext-real V14() V15() Element of REAL
abs (t - lg) is ext-real V14() V15() Element of REAL
tt - pf is ext-real V14() V15() Element of REAL
abs (tt - pf) is ext-real V14() V15() Element of REAL
(abs (t - lg)) + (abs (tt - pf)) is ext-real V14() V15() Element of REAL
dom ((h1 ^ f) ^ h2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
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() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[t,tt] is set
{t,tt} is non empty V146() V147() V148() V149() V150() V151() set
{t} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{t,tt},{t}} is non empty set
lg is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[lg,pf] is set
{lg,pf} is non empty V146() V147() V148() V149() V150() V151() set
{lg} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{lg,pf},{lg}} is non empty set
((h1 ^ f) ^ h2) /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (t,tt) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ f) ^ h2) /. (D + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (lg,pf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
t - lg is ext-real V14() V15() Element of REAL
abs (t - lg) is ext-real V14() V15() Element of REAL
tt - pf is ext-real V14() V15() Element of REAL
abs (tt - pf) is ext-real V14() V15() Element of REAL
(abs (t - lg)) + (abs (tt - pf)) 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
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[t,tt] is set
{t,tt} is non empty V146() V147() V148() V149() V150() V151() set
{t} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{t,tt},{t}} is non empty set
h1 /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (t,tt) 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
(h1 ^ f) /. D 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
((h1 ^ f) ^ h2) /. D is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len ((h1 ^ f) ^ h2)) is V33() V40( len ((h1 ^ f) ^ h2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
(rng f) /\ (rng (Col (q1,1))) is set
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (q1,1))) is set
Line ((DelCol (q1,1)),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 (DelCol (q1,1))), the U1 of (TOP-REAL 2)))
width (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
K180((width (DelCol (q1,1))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line ((DelCol (q1,1)),1)) is set
Line ((DelCol (q1,1)),(len (DelCol (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 (DelCol (q1,1))), the U1 of (TOP-REAL 2)))
rng (Line ((DelCol (q1,1)),(len (DelCol (q1,1))))) is set
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(f1 | f2) /. t is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(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
(f1 | f2) /. tt 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
(f1 | f2) /. tt is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(len (f1 | f2)) - tt is ext-real V14() V15() Element of REAL
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
C 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 C is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
dom C is V146() V147() V148() V149() V150() V151() Element of bool NAT
Seg pf is V33() V40(pf) V146() V147() V148() V149() V150() V151() Element of bool NAT
rng C is set
Li is set
La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
C /. La is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt + La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt + pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
La + tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. (tt + La) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Li is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt + Li is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Li + tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt + 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 C) is V33() V40( len C) V146() V147() V148() V149() V150() V151() Element of bool NAT
Indices (DelCol (q1,1)) is set
Seg (width (DelCol (q1,1))) is V33() V40( width (DelCol (q1,1))) V146() V147() V148() V149() V150() V151() Element of bool NAT
[:(dom (DelCol (q1,1))),(Seg (width (DelCol (q1,1)))):] is INT -valued RAT -valued V136() V137() V138() V139() set
La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Li 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 Li is V146() V147() V148() V149() V150() V151() Element of bool NAT
tt + La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. (tt + La) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[pl,pf] is set
{pl,pf} is non empty V146() V147() V148() V149() V150() V151() set
{pl} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{pl,pf},{pl}} is non empty set
q1 * (pl,pf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pf - 1 is ext-real V14() V15() Element of REAL
Col (q1,pf) 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)))
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
K2 /. pl is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
K2 . pl is set
rng (Col (q1,pf)) is set
tt + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt - tt is ext-real V14() V15() Element of REAL
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Li /. La is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
K1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
CK2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[CK2,K1] is set
{CK2,K1} 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,K1},{CK2}} is non empty set
K1 + 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,1)) * (CK2,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col ((DelCol (q1,1)),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 (DelCol (q1,1))), the U1 of (TOP-REAL 2)))
K180((len (DelCol (q1,1))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
Col (q1,(1 + 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)))
len Li is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Li /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (tt + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng (Col ((DelCol (q1,1)),1)) is set
La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
La + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[pl,pf] is set
{pl,pf} is non empty V146() V147() V148() V149() V150() V151() set
{pl} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{pl,pf},{pl}} is non empty set
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[pl,K2] is set
{pl,K2} is non empty V146() V147() V148() V149() V150() V151() set
{pl} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{pl,K2},{pl}} is non empty set
Li /. La is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(DelCol (q1,1)) * (pl,pf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Li /. (La + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(DelCol (q1,1)) * (pl,K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg p2 is V33() V40(p2) V146() V147() V148() V149() V150() V151() Element of bool NAT
pf + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[pl,(pf + 1)] is set
{pl,(pf + 1)} is non empty V146() V147() V148() V149() V150() V151() set
{{pl,(pf + 1)},{pl}} is non empty set
tt + La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. (tt + La) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (pl,(pf + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt + (La + 1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(tt + La) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K2 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[pl,(K2 + 1)] is set
{pl,(K2 + 1)} is non empty V146() V147() V148() V149() V150() V151() set
{{pl,(K2 + 1)},{pl}} is non empty set
(f1 | f2) /. (tt + (La + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. ((tt + La) + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (pl,(K2 + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pl - pl is ext-real V14() V15() Element of REAL
abs (pl - pl) is ext-real V14() V15() Element of REAL
(pf + 1) - (K2 + 1) is ext-real V14() V15() Element of REAL
abs ((pf + 1) - (K2 + 1)) is ext-real V14() V15() Element of REAL
(abs (pl - pl)) + (abs ((pf + 1) - (K2 + 1))) is ext-real V14() V15() Element of REAL
pf - K2 is ext-real V14() V15() Element of REAL
abs (pf - K2) is ext-real V14() V15() Element of REAL
(abs (pl - pl)) + (abs (pf - K2)) is ext-real V14() V15() Element of REAL
rng Li is set
(rng ((h1 ^ f) ^ h2)) /\ (rng Li) is set
the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng Li) is Element of (rng ((h1 ^ f) ^ h2)) /\ (rng Li)
Li /. (len Li) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
tt + pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. (tt + pf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col ((DelCol (q1,1)),(width (DelCol (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 (DelCol (q1,1))), the U1 of (TOP-REAL 2)))
rng (Col ((DelCol (q1,1)),(width (DelCol (q1,1))))) is set
(rng f) /\ (rng (Col (q1,1))) is set
(rng f) /\ (rng (Col (q1,(width q1)))) is set
(rng ((h1 ^ f) ^ h2)) /\ (rng (Col (q1,(width q1)))) is set
Col ((DelCol (q1,(width 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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
K180((len (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col ((DelCol (q1,(width q1))),1)) is set
width (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
Col ((DelCol (q1,(width q1))),(width (DelCol (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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
rng (Col ((DelCol (q1,(width q1))),(width (DelCol (q1,(width q1)))))) is set
t 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)
t /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t /. (len t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng t is set
(rng ((h1 ^ f) ^ h2)) /\ (rng t) is set
the Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t) is Element of (rng ((h1 ^ f) ^ h2)) /\ (rng t)
Line ((DelCol (q1,(width 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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
K180((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line ((DelCol (q1,(width q1))),1)) is set
Line ((DelCol (q1,(width q1))),(len (DelCol (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((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
rng (Line ((DelCol (q1,(width q1))),(len (DelCol (q1,(width q1)))))) is set
(rng f) /\ (rng (Col (q1,(width q1)))) is set
t 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 t is set
t /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len t is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
t /. (len t) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col ((DelCol (q1,(width 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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
K180((len (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col ((DelCol (q1,(width q1))),1)) is set
width (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
Col ((DelCol (q1,(width q1))),(width (DelCol (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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
rng (Col ((DelCol (q1,(width q1))),(width (DelCol (q1,(width q1)))))) is set
tt 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)
tt /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len tt is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
tt /. (len tt) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng tt is set
(len (f1 | f2)) - 1 is ext-real V14() V15() Element of REAL
lg 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)) /\ (rng (Line (q1,n))) is set
the Element of (rng (f1 | f2)) /\ (rng (Line (q1,n))) is Element of (rng (f1 | f2)) /\ (rng (Line (q1,n)))
C is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. C is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Li is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
La is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(f1 | f2) /. La is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(f1 | f2) /. pf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
lg + 1 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)) /\ (rng (Line (q1,q))) is set
the Element of (rng (f1 | f2)) /\ (rng (Line (q1,q))) is Element of (rng (f1 | f2)) /\ (rng (Line (q1,q)))
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. pf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
K2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(f1 | f2) /. K2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(f1 | f2) /. pl is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
pl is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. pl is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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)
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)))
Li 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 Li is V146() V147() V148() V149() V150() V151() Element of bool NAT
(f1 | f2) /. pf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
K1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Li /. K1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col (q1,K1) 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)))
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
h2 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 V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h2 + 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 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,LL) 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,LL)) is set
rng Li is 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
q1 * (F1,F) 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
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[hf,FF] is set
{hf,FF} is non empty V146() V147() V148() V149() V150() V151() set
{hf} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{hf,FF},{hf}} is non empty set
q1 * (hf,FF) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (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((width q1), the U1 of (TOP-REAL 2)))
x 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 x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len x) is V33() V40( len x) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom x is V146() V147() V148() V149() V150() V151() Element of bool NAT
x /. FF is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x . FF is set
rng x is set
Line (q1,F1) 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)))
w4 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 w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len w4) is V33() V40( len w4) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom w4 is V146() V147() V148() V149() V150() V151() Element of bool NAT
w4 /. F is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 . F is set
rng w4 is set
w + h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q2 /. (w + h2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(q2 | mi1) /. (w + h2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w + (h2 + 1) 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 V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q2 | mi1) /. (w + (h2 + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + (h2 + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,(n + 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)))
rng (Line (q1,(n + 1))) is set
rng (Line (q1,F1)) is set
F1 - hf is ext-real V14() V15() Element of REAL
abs (F1 - hf) is ext-real V14() V15() Element of REAL
hf + 1 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 ext-real V14() V15() Element of REAL
F1 + 1 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
F1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
rng (Line (q1,F1)) is set
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,i1) 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,i1)) is set
F1 - i1 is ext-real V14() V15() Element of REAL
abs (F1 - i1) is ext-real V14() V15() Element of REAL
len Li is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len Li) is V33() V40( len Li) 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
h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL 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
[LL,F1] is set
{LL,F1} is non empty V146() V147() V148() V149() V150() V151() set
{LL} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{LL,F1},{LL}} is non empty set
h1 /. h2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (LL,F1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[(h2 + 1),K1] is set
{(h2 + 1),K1} is non empty V146() V147() V148() V149() V150() V151() set
{(h2 + 1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(h2 + 1),K1},{(h2 + 1)}} is non empty set
LL 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
[LL,F1] is set
{LL,F1} is non empty V146() V147() V148() V149() V150() V151() set
{LL} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{LL,F1},{LL}} is non empty set
F 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
[F,hf] is set
{F,hf} is non empty V146() V147() V148() V149() V150() V151() set
{F} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{F,hf},{F}} is non empty set
h1 /. h2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (LL,F1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
h1 /. (h2 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (F,hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((h2 + 1),K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[h2,K1] is set
{h2,K1} is non empty V146() V147() V148() V149() V150() V151() set
{h2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{h2,K1},{h2}} is non empty set
q1 * (h2,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL - F is ext-real V14() V15() Element of REAL
abs (LL - F) is ext-real V14() V15() Element of REAL
F1 - hf is ext-real V14() V15() Element of REAL
abs (F1 - hf) is ext-real V14() V15() Element of REAL
(abs (LL - F)) + (abs (F1 - hf)) is ext-real V14() V15() Element of REAL
h2 - h2 is ext-real V14() V15() Element of REAL
(h2 - h2) + (- 1) is ext-real V14() V15() Element of REAL
abs ((h2 - h2) + (- 1)) is ext-real V14() V15() Element of REAL
(abs ((h2 - h2) + (- 1))) + 0 is ext-real V14() V15() Element of REAL
Lma . K2 is set
q1 * (q,K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
f /. 0 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,LL) 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,LL)) is set
rng h1 is set
(rng h1) /\ (rng tt) is set
the Element of (rng h1) /\ (rng tt) is Element of (rng h1) /\ (rng tt)
F1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 /. F1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg (len h1) is V33() V40( len h1) V146() V147() V148() V149() V150() V151() Element of bool NAT
[F1,K1] is set
{F1,K1} 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,K1},{F1}} is non empty set
F is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. F 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
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[hf,FF] is set
{hf,FF} is non empty V146() V147() V148() V149() V150() V151() set
{hf} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{hf,FF},{hf}} is non empty set
q1 * (hf,FF) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (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((width q1), the U1 of (TOP-REAL 2)))
x 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 x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len x) is V33() V40( len x) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom x is V146() V147() V148() V149() V150() V151() Element of bool NAT
x /. FF is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x . FF is set
rng x is set
q1 * (F1,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. (LL + 1) 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() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,F1) 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,F1)) is set
(q2 | mi1) /. (w + 1) 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)
rng Li is set
F 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
[F,hf] is set
{F,hf} is non empty V146() V147() V148() V149() V150() V151() set
{F} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{F,hf},{F}} is non empty set
q1 * (F,hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,F) 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)))
FF 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 FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len FF) is V33() V40( len FF) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom FF is V146() V147() V148() V149() V150() V151() Element of bool NAT
FF /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
FF . hf is set
rng FF is set
x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[x,w4] is set
{x,w4} is non empty V146() V147() V148() V149() V150() V151() set
{x} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{x,w4},{x}} is non empty set
q1 * (x,w4) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (q1,x) 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)))
i1 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 i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len i1) is V33() V40( len i1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom i1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
i1 /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 . w4 is set
rng i1 is set
w + LL 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 + LL) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 /. (w + LL) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng (Line (q1,x)) is set
x - F is ext-real V14() V15() Element of REAL
abs (x - F) is ext-real V14() V15() Element of REAL
F + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
x + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
x + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
rng (Line (q1,x)) is set
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,i2) 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,i2)) is set
x - i2 is ext-real V14() V15() Element of REAL
abs (x - i2) is ext-real V14() V15() Element of REAL
Seg (len h1) is V33() V40( len h1) V146() V147() V148() V149() V150() V151() Element of bool NAT
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL + q is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + LL 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 /. LL 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)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + (LL + 1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q + LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(q + LL) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[((q + LL) + 1),K2] is set
{((q + LL) + 1),K2} is non empty V146() V147() V148() V149() V150() V151() set
{((q + LL) + 1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{((q + LL) + 1),K2},{((q + LL) + 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
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[hf,FF] is set
{hf,FF} is non empty V146() V147() V148() V149() V150() V151() set
{hf} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{hf,FF},{hf}} is non empty set
h2 /. LL 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 /. (LL + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (hf,FF) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * ((q + (LL + 1)),K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[(q + LL),K2] is set
{(q + LL),K2} is non empty V146() V147() V148() V149() V150() V151() set
{(q + LL)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(q + LL),K2},{(q + LL)}} is non empty set
q1 * ((q + LL),K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 - hf is ext-real V14() V15() Element of REAL
abs (F1 - hf) is ext-real V14() V15() Element of REAL
F - FF is ext-real V14() V15() Element of REAL
abs (F - FF) is ext-real V14() V15() Element of REAL
(abs (F1 - hf)) + (abs (F - FF)) is ext-real V14() V15() Element of REAL
(q + LL) - (q + LL) is ext-real V14() V15() Element of REAL
((q + LL) - (q + LL)) + (- 1) is ext-real V14() V15() Element of REAL
abs (((q + LL) - (q + LL)) + (- 1)) is ext-real V14() V15() Element of REAL
(abs (((q + LL) - (q + LL)) + (- 1))) + 0 is ext-real V14() V15() Element of REAL
Seg (len h2) is V33() V40( len h2) V146() V147() V148() V149() V150() V151() Element of bool NAT
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line (q1,LL) 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,LL)) is set
rng h2 is set
(rng h2) /\ (rng tt) is set
the Element of (rng h2) /\ (rng tt) is Element of (rng h2) /\ (rng tt)
F1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 /. F1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + F1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[(q + F1),K2] is set
{(q + F1),K2} is non empty V146() V147() V148() V149() V150() V151() set
{(q + F1)} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{(q + F1),K2},{(q + F1)}} is non empty set
F is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f /. F 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
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[hf,FF] is set
{hf,FF} is non empty V146() V147() V148() V149() V150() V151() set
{hf} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{hf,FF},{hf}} is non empty set
q1 * (hf,FF) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (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((width q1), the U1 of (TOP-REAL 2)))
x 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 x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len x) is V33() V40( len x) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom x is V146() V147() V148() V149() V150() V151() Element of bool NAT
x /. FF is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x . FF is set
rng x is set
q1 * ((q + F1),K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
C 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 C is V146() V147() V148() V149() V150() V151() Element of bool NAT
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
C /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len C is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len C) is V33() V40( len C) V146() V147() V148() V149() V150() V151() Element of bool NAT
[LL,(width q1)] is set
{LL,(width q1)} is non empty V146() V147() V148() V149() V150() V151() set
{LL} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{LL,(width q1)},{LL}} is non empty set
C . LL is set
q1 * (LL,(width q1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. lg 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() 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
q1 * (F1,F) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[q,K2] is set
{q,K2} is non empty V146() V147() V148() V149() V150() V151() set
{{q,K2},{q}} is non empty set
F1 - q is ext-real V14() V15() Element of REAL
abs (F1 - q) is ext-real V14() V15() Element of REAL
F - (width q1) is ext-real V14() V15() Element of REAL
abs (F - (width q1)) is ext-real V14() V15() Element of REAL
(abs (F1 - q)) + (abs (F - (width q1))) is ext-real V14() V15() Element of REAL
C /. F1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
C . F1 is set
rng C is set
f1 /. lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
La 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)
La /. F is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Lma . F is set
Lma /. F is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng Lma is set
Li . K1 is set
q1 * (n,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
C /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
C . LL is set
q1 * (LL,(width q1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[LL,(width q1)] is set
{LL,(width q1)} is non empty V146() V147() V148() V149() V150() V151() set
{LL} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{LL,(width q1)},{LL}} 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
q1 * (F1,F) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[n,K1] is set
{n,K1} is non empty V146() V147() V148() V149() V150() V151() set
{{n,K1},{n}} is non empty set
F1 - n is ext-real V14() V15() Element of REAL
abs (F1 - n) is ext-real V14() V15() Element of REAL
F - (width q1) is ext-real V14() V15() Element of REAL
abs (F - (width q1)) is ext-real V14() V15() Element of REAL
(abs (F1 - n)) + (abs (F - (width q1))) is ext-real V14() V15() Element of REAL
C /. F1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
C . F1 is set
rng C is set
f1 /. lg is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Li /. F is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Li . F is set
rng Li is set
pl + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pl + 1) - pf is ext-real V14() V15() Element of REAL
pf - 1 is ext-real V14() V15() Element of REAL
(f1 | f2) | pl 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 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg LL is V33() V40(LL) V146() V147() V148() V149() V150() V151() Element of bool NAT
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
F1 + hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf 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 hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 ^ hf 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 ^ hf) ^ 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)
Seg (len hf) is V33() V40( len hf) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom hf is V146() V147() V148() V149() V150() V151() Element of bool NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F1 + w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + w4) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + w4) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 + pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
LL + pf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(w4 + pf) - 1 is ext-real V14() V15() Element of REAL
Seg pl is V33() V40(pl) V146() V147() V148() V149() V150() V151() Element of bool NAT
rng hf is set
w4 is set
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + i1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + i1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pf + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[w4,i1] is set
{w4,i1} is non empty V146() V147() V148() V149() V150() V151() set
{w4} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{w4,i1},{w4}} is non empty set
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i2,j1] is set
{i2,j1} is non empty V146() V147() V148() V149() V150() V151() set
{i2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i2,j1},{i2}} is non empty set
len (h1 ^ hf) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(h1 ^ hf) /. (len (h1 ^ hf)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (w4,i1) 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 * (i2,j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom (h1 ^ hf) is V146() V147() V148() V149() V150() V151() Element of bool NAT
[(q + 1),K2] is set
{(q + 1),K2} is non empty V146() V147() V148() V149() V150() V151() set
{{(q + 1),K2},{(q + 1)}} is non empty set
(len h1) + (len hf) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(h1 ^ hf) /. ((len h1) + (len hf)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf /. (len hf) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + LL) 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)
w4 - i2 is ext-real V14() V15() Element of REAL
abs (w4 - i2) is ext-real V14() V15() Element of REAL
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
(abs (w4 - i2)) + (abs (i1 - j1)) is ext-real V14() V15() Element of REAL
rng ((h1 ^ hf) ^ h2) is set
rng (h1 ^ hf) is set
(rng (h1 ^ hf)) \/ (rng h2) is set
(rng h1) \/ (rng hf) is set
((rng h1) \/ (rng hf)) \/ (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,K1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Col (q1,w4) 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,w4)) is set
(rng hf) /\ (rng (Col (q1,w4))) is set
(rng ((h1 ^ hf) ^ h2)) /\ (rng (Col (q1,w4))) is set
the Element of (rng ((h1 ^ hf) ^ h2)) /\ (rng (Col (q1,w4))) is Element of (rng ((h1 ^ hf) ^ h2)) /\ (rng (Col (q1,w4)))
(rng h1) \/ (rng h2) is set
(rng hf) \/ ((rng h1) \/ (rng h2)) is set
((rng h1) \/ (rng h2)) /\ (rng (Col (q1,w4))) is set
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (q1,w4)))) is set
(rng h1) /\ (rng (Col (q1,w4))) is set
(rng h2) /\ (rng (Col (q1,w4))) is set
((rng h1) /\ (rng (Col (q1,w4)))) \/ ((rng h2) /\ (rng (Col (q1,w4)))) is set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 /. K1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 . K1 is set
CK1 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 CK1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
CK1 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK1 . n is set
CK1 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK1 . j1 is set
j2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng CK1 is set
hf /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 * ((q + j1),K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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)
dom CK2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
CK2 /. q is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK2 . q is set
CK2 /. (q + j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK2 . (q + j1) is set
j2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng CK2 is set
hf /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + LL) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng C is set
(rng hf) /\ (rng C) is set
the Element of (rng hf) /\ (rng C) is Element of (rng hf) /\ (rng C)
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F1 + i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 /. (w4 + i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(rng ((h1 ^ hf) ^ h2)) /\ (rng (Col (q1,(width q1)))) is set
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F1 + i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. (w4 + i1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i2,j1] is set
{i2,j1} is non empty V146() V147() V148() V149() V150() V151() set
{i2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i2,j1},{i2}} is non empty set
q1 * (i2,j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((f1 | f2) | pl) /. (F1 + i1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j2,j1] is set
{j2,j1} is non empty V146() V147() V148() V149() V150() V151() set
{j2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j2,j1},{j2}} is non empty set
q1 * (j2,j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(h1 ^ hf) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom ((h1 ^ hf) ^ h2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ hf) ^ h2) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[w4,i1] is set
{w4,i1} is non empty V146() V147() V148() V149() V150() V151() set
{w4} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{w4,i1},{w4}} is non empty set
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i2,j1] is set
{i2,j1} is non empty V146() V147() V148() V149() V150() V151() set
{i2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i2,j1},{i2}} is non empty set
h1 /. (len h1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (w4,i1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i2,j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[m,K1] is set
{m,K1} is non empty V146() V147() V148() V149() V150() V151() set
{{m,K1},{m}} is non empty set
q1 * (m,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 - i2 is ext-real V14() V15() Element of REAL
abs (w4 - i2) is ext-real V14() V15() Element of REAL
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
(abs (w4 - i2)) + (abs (i1 - j1)) is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
hf /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + w4) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. (F1 + w4) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F1 + (w4 + 1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pl) /. (F1 + (w4 + 1)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(F1 + w4) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. ((F1 + w4) + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
(h1 ^ hf) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(h1 ^ hf) /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
((h1 ^ hf) ^ h2) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ hf) ^ h2) /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
(rng ((h1 ^ hf) ^ h2)) /\ (rng tt) is set
the Element of (rng ((h1 ^ hf) ^ h2)) /\ (rng tt) is Element of (rng ((h1 ^ hf) ^ h2)) /\ (rng tt)
(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 hf) + ((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
Seg pl is V33() V40(pl) V146() V147() V148() V149() V150() V151() Element of bool NAT
hf ^ 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 ^ hf) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg m is V33() V40(m) V146() V147() V148() V149() V150() V151() Element of bool 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
x1 /. K1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x1 . K1 is set
((h1 ^ hf) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(h1 ^ hf) /. 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,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ hf) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ hf) ^ h2) /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg pl is V33() V40(pl) V146() V147() V148() V149() V150() V151() Element of bool NAT
len ((h1 ^ hf) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ hf) ^ h2) /. (len ((h1 ^ hf) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ hf) ^ h2) /. ((len h1) + (len hf)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
hf /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((f1 | f2) | pl) /. pl is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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 ^ hf) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ hf) ^ h2) /. (len ((h1 ^ hf) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(len (h1 ^ hf)) + (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 ^ hf) ^ h2) /. ((len (h1 ^ hf)) + (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 ^ hf) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ hf) ^ h2) /. (len ((h1 ^ hf) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len ((h1 ^ hf) ^ h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((h1 ^ hf) ^ h2) /. (len ((h1 ^ hf) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(len (h1 ^ hf)) + (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 hf)) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line ((DelCol (q1,(width 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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
K180((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line ((DelCol (q1,(width q1))),1)) is set
Line ((DelCol (q1,(width q1))),(len (DelCol (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((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
rng (Line ((DelCol (q1,(width q1))),(len (DelCol (q1,(width q1)))))) is set
(rng tt) /\ (rng ((h1 ^ hf) ^ h2)) is set
((rng h1) \/ (rng hf)) /\ (rng tt) is set
(((rng h1) \/ (rng hf)) /\ (rng tt)) \/ {} is set
(rng hf) /\ (rng tt) is set
{} \/ ((rng hf) /\ (rng tt)) is set
(rng tt) /\ (rng hf) is set
pf + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - pl is ext-real V14() V15() Element of REAL
(f1 | f2) | 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)
LL is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg LL is V33() V40(LL) V146() V147() V148() V149() V150() V151() Element of bool NAT
F is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - F is ext-real V14() V15() Element of REAL
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(pf + 1) - 1 is ext-real V14() V15() Element of REAL
(pf + 1) - 0 is ext-real V14() V15() Element of REAL
(pf + 1) - LL is ext-real V14() V15() Element of REAL
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg pf is V33() V40(pf) V146() V147() V148() V149() V150() V151() Element of bool NAT
F is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - F is ext-real V14() V15() Element of REAL
(pf + 1) - 0 is ext-real V14() V15() Element of REAL
F is ext-real V7() V8() V9() V13() V14() V15() V33() V38() set
(pf + 1) - F is ext-real V14() V15() Element of REAL
hf is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(f1 | f2) /. hf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
FF is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. FF 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
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)
Seg (len F) is V33() V40( len F) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom F is V146() V147() V148() V149() V150() V151() Element of bool NAT
rng F is set
x is set
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(pf + 1) - w4 is ext-real V14() V15() Element of REAL
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
pl + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - LL is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[w4,i1] is set
{w4,i1} is non empty V146() V147() V148() V149() V150() V151() set
{w4} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{w4,i1},{w4}} is non empty set
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i2,j1] is set
{i2,j1} is non empty V146() V147() V148() V149() V150() V151() set
{i2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i2,j1},{i2}} is non empty 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
(h1 ^ F) /. (len (h1 ^ F)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (w4,i1) 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 * (i2,j1) 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),K2] is set
{(q + 1),K2} is non empty V146() V147() V148() V149() V150() V151() set
{{(q + 1),K2},{(q + 1)}} is non empty set
(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) /. ((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)
x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. x is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. x 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)
w4 - i2 is ext-real V14() V15() Element of REAL
abs (w4 - i2) is ext-real V14() V15() Element of REAL
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
(abs (w4 - i2)) + (abs (i1 - j1)) is ext-real V14() V15() Element of REAL
x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - x is ext-real V14() V15() Element of REAL
F /. x is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(h1 ^ F) /. x is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom ((h1 ^ F) ^ h2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
x 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) /. x is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng ((h1 ^ F) ^ h2) is set
(rng ((h1 ^ F) ^ h2)) /\ (rng tt) is set
the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt) is Element of (rng ((h1 ^ F) ^ h2)) /\ (rng tt)
(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) 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,K1)) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Col (q1,w4) 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,w4)) is set
(rng F) /\ (rng (Col (q1,w4))) is set
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (q1,w4))) is set
the Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (q1,w4))) is Element of (rng ((h1 ^ F) ^ h2)) /\ (rng (Col (q1,w4)))
(rng h1) \/ (rng h2) is set
(rng F) \/ ((rng h1) \/ (rng h2)) is set
((rng h1) \/ (rng h2)) /\ (rng (Col (q1,w4))) is set
{} \/ (((rng h1) \/ (rng h2)) /\ (rng (Col (q1,w4)))) is set
(rng h1) /\ (rng (Col (q1,w4))) is set
(rng h2) /\ (rng (Col (q1,w4))) is set
((rng h1) /\ (rng (Col (q1,w4)))) \/ ((rng h2) /\ (rng (Col (q1,w4)))) is set
(pf + 1) - 1 is ext-real V14() V15() Element of REAL
F /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((f1 | f2) | pf) /. pf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h1 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 /. K1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
g1 . K1 is set
CK1 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 CK1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
CK1 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK1 . j1 is set
j2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng CK1 is set
CK1 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK1 . n is set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
h2 /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q + j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 * ((q + j1),K2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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)
dom CK2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
CK2 /. q is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK2 . q is set
CK2 /. (q + j1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
CK2 . (q + j1) is set
j2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng CK2 is set
F /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. j1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
rng C is set
(rng F) /\ (rng C) is set
the Element of (rng F) /\ (rng C) is Element of (rng F) /\ (rng C)
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
F /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(pf + 1) - i1 is ext-real V14() V15() Element of REAL
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - 1 is ext-real V14() V15() Element of REAL
((f1 | f2) | pf) /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(rng ((h1 ^ F) ^ h2)) /\ (rng (Col (q1,(width q1)))) is set
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(pf + 1) - w4 is ext-real V14() V15() Element of REAL
(pf + 1) - (w4 + 1) is ext-real V14() V15() Element of REAL
F /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. i1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. i2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i2 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j1 - j1 is ext-real V14() V15() Element of REAL
abs (j1 - j1) is ext-real V14() V15() Element of REAL
j2 - j2 is ext-real V14() V15() Element of REAL
abs (j2 - j2) is ext-real V14() V15() Element of REAL
(abs (j1 - j1)) + (abs (j2 - j2)) is ext-real V14() V15() Element of REAL
j1 - j1 is ext-real V14() V15() Element of REAL
- (j1 - j1) is ext-real V14() V15() Element of REAL
abs (- (j1 - j1)) is ext-real V14() V15() Element of REAL
j2 - j2 is ext-real V14() V15() Element of REAL
- (j2 - j2) is ext-real V14() V15() Element of REAL
abs (- (j2 - j2)) is ext-real V14() V15() Element of REAL
(abs (- (j1 - j1))) + (abs (- (j2 - j2))) is ext-real V14() V15() Element of REAL
abs (j1 - j1) is ext-real V14() V15() Element of REAL
(abs (j1 - j1)) + (abs (- (j2 - j2))) is ext-real V14() V15() Element of REAL
abs (j2 - j2) is ext-real V14() V15() Element of REAL
(abs (j1 - j1)) + (abs (j2 - j2)) is ext-real V14() V15() Element of REAL
(pf + 1) - 1 is ext-real V14() V15() Element of REAL
Seg pf is V33() V40(pf) V146() V147() V148() V149() V150() V151() Element of bool 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)
((f1 | f2) | pf) /. pf is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Seg m is V33() V40(m) V146() V147() V148() V149() V150() V151() Element of bool 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
x1 /. K1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
x1 . K1 is set
((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,K1) 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)
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
h1 /. (len h1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i1,i2) 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 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
((f1 | f2) | pf) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(f1 | f2) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
[m,K1] is set
{m,K1} is non empty V146() V147() V148() V149() V150() V151() set
{{m,K1},{m}} is non empty set
q1 * (m,K1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
(h1 ^ F) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(h1 ^ F) /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
w4 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
w4 + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
i2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[i1,i2] is set
{i1,i2} is non empty V146() V147() V148() V149() V150() V151() set
{i1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{i1,i2},{i1}} is non empty set
j1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
j2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[j1,j2] is set
{j1,j2} is non empty V146() V147() V148() V149() V150() V151() set
{j1} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{j1,j2},{j1}} is non empty set
((h1 ^ F) ^ h2) /. w4 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (i1,i2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ F) ^ h2) /. (w4 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 * (j1,j2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
i1 - j1 is ext-real V14() V15() Element of REAL
abs (i1 - j1) is ext-real V14() V15() Element of REAL
i2 - j2 is ext-real V14() V15() Element of REAL
abs (i2 - j2) is ext-real V14() V15() Element of REAL
(abs (i1 - j1)) + (abs (i2 - j2)) is ext-real V14() V15() Element of REAL
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
(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)) + (len h2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line ((DelCol (q1,(width 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 (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
K180((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line ((DelCol (q1,(width q1))),1)) is set
Seg pf is V33() V40(pf) V146() V147() V148() V149() V150() V151() Element of bool NAT
(pf + 1) - ((pf + 1) - pl) is ext-real V14() V15() Element of REAL
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ F) ^ h2) /. ((len h1) + (len F)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
F /. LL is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((f1 | f2) | pf) /. pl is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((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)
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
((h1 ^ F) ^ h2) /. (len ((h1 ^ F) ^ h2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line ((DelCol (q1,(width q1))),(len (DelCol (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((width (DelCol (q1,(width q1)))), the U1 of (TOP-REAL 2)))
rng (Line ((DelCol (q1,(width q1))),(len (DelCol (q1,(width q1)))))) is set
(rng tt) /\ (rng ((h1 ^ F) ^ h2)) is set
((rng h1) \/ (rng F)) /\ (rng tt) is set
(((rng h1) \/ (rng F)) /\ (rng tt)) \/ {} is set
(rng F) /\ (rng tt) is set
{} \/ ((rng F) /\ (rng tt)) is set
(rng tt) /\ (rng F) is set
(rng f) /\ (rng (Col (q1,(width q1)))) is set
(rng f) /\ (rng (Col (q1,1))) is set
p2 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 p2 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 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 q1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
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
q1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Line (p2,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 p2), the U1 of (TOP-REAL 2)))
K180((width p2), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line (p2,1)) is set
q1 /. (len q1) is V40(2) FinSequence-like V138() Element 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
Line (p2,(len p2)) 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 p2), the U1 of (TOP-REAL 2)))
rng (Line (p2,(len p2))) is set
q2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col (p2,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 p2), the U1 of (TOP-REAL 2)))
K180((len p2), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col (p2,1)) is set
q2 /. (len q2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
Col (p2,(width p2)) 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 p2), the U1 of (TOP-REAL 2)))
rng (Col (p2,(width p2))) is set
rng q1 is set
rng q2 is set
(rng q1) /\ (rng q2) 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
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
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
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
q2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
q2 /. (len q2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
f1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
f1 /. (len f1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
rng q2 is set
rng f1 is set
(rng q2) /\ (rng f1) is 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)
L~ P2 is Element of bool the U1 of (TOP-REAL 2)
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)
L~ p1 is Element of bool the U1 of (TOP-REAL 2)
rng P2 is set
rng p1 is set
p2 is set
dom p1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
q1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p1 /. q1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom P2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
q1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
P2 /. q1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
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 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))
P2 /. 1 is V40(2) FinSequence-like V138() Element of 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
P2 /. (len P2) is V40(2) FinSequence-like V138() Element 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
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
p1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
p1 /. (len p1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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
L~ P2 is Element of bool the U1 of (TOP-REAL 2)
L~ p1 is Element of bool the U1 of (TOP-REAL 2)
P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
P2 is ext-real V14() V15() Element of REAL
p1 is ext-real V14() V15() Element of REAL
dom P1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
rng P1 is V146() V147() V148() set
[.P2,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
P1 . p2 is ext-real V14() V15() Element of REAL
p2 is set
q1 is set
P1 . q1 is ext-real V14() V15() Element of REAL
q2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
P1 . q2 is ext-real V14() V15() Element of REAL
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
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
dom P1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
dom P2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
X_axis P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
(X_axis P1) . 1 is ext-real V14() V15() Element of REAL
(X_axis P1) . (len P1) is ext-real V14() V15() Element of REAL
X_axis P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
(Y_axis P2) . 1 is ext-real V14() V15() Element of REAL
(Y_axis P2) . (len P2) is ext-real V14() V15() Element of REAL
L~ P1 is Element of bool the U1 of (TOP-REAL 2)
L~ P2 is Element of bool the U1 of (TOP-REAL 2)
p1 is non empty 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)
p2 is non empty 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)
p1 ^ p2 is non empty 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 non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len p2) is non empty V33() V40( len p2) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom p2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
p1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len p1 is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p1 /. (len p1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
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)
q1 is non empty 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)
X_axis q1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis q1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
X_axis p1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis p1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
X_axis p2 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis p2 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Seg (len p1) is non empty V33() V40( len p1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom p1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
q1 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len q1 is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len q1) is non empty V33() V40( len q1) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom q1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
GoB 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))
dom (X_axis q1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (X_axis q1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (X_axis q1)) is non empty V33() V40( len (X_axis q1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
len (X_axis p2) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (X_axis p2)) is non empty V33() V40( len (X_axis p2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (X_axis p2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
(len p1) + (len p2) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
len (X_axis p1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (X_axis p1)) is non empty V33() V40( len (X_axis p1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (X_axis p1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
(X_axis p1) . 1 is ext-real V14() V15() Element of REAL
q2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 `1 is ext-real V14() V15() Element of REAL
g1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(X_axis q1) . g1 is ext-real V14() V15() Element of REAL
p1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
m `1 is ext-real V14() V15() Element of REAL
(X_axis p1) . g1 is ext-real V14() V15() Element of REAL
g1 - (len p1) is ext-real V14() V15() Element of REAL
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
m + (len p1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
s is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p2 /. s is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p2 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 `1 is ext-real V14() V15() Element of REAL
(X_axis p2) . s is ext-real V14() V15() Element of REAL
2 + 2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(X_axis q1) . 1 is ext-real V14() V15() Element of REAL
Line ((GoB 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 (GoB q1)), the U1 of (TOP-REAL 2)))
width (GoB q1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
K180((width (GoB q1)), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Line ((GoB q1),1)) is set
q1 /. (len p1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(X_axis p1) . (len p1) is ext-real V14() V15() Element of REAL
f1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 `1 is ext-real V14() V15() Element of REAL
g1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(X_axis q1) . g1 is ext-real V14() V15() Element of REAL
p1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
m `1 is ext-real V14() V15() Element of REAL
(X_axis p1) . g1 is ext-real V14() V15() Element of REAL
g1 - (len p1) is ext-real V14() V15() Element of REAL
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
m + (len p1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
s is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p2 /. s is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p2 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 `1 is ext-real V14() V15() Element of REAL
(X_axis p2) . s is ext-real V14() V15() Element of REAL
(X_axis q1) . (len p1) is ext-real V14() V15() Element of REAL
len (GoB q1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Line ((GoB q1),(len (GoB 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 (GoB q1)), the U1 of (TOP-REAL 2)))
rng (Line ((GoB q1),(len (GoB q1)))) is set
g1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Indices (GoB q1) is set
q1 /. g1 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
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[g2,m] is set
{g2,m} is non empty V146() V147() V148() V149() V150() V151() set
{g2} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{g2,m},{g2}} is non empty set
(GoB q1) * (g2,m) 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
w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[s,w5] is set
{s,w5} is non empty V146() V147() V148() V149() V150() V151() set
{s} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{s,w5},{s}} is non empty set
p1 /. g1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(GoB q1) * (s,w5) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ p1 is Element of bool 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)
L~ g1 is Element of bool the U1 of (TOP-REAL 2)
g1 /. 1 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
g1 /. (len g1) 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
(len p1) + g2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 /. ((len p1) + g2) is V40(2) FinSequence-like V138() Element of 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
s is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[m,s] is set
{m,s} 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,s},{m}} is non empty set
(GoB q1) * (m,s) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
m1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
[w5,m1] is set
{w5,m1} is non empty V146() V147() V148() V149() V150() V151() set
{w5} is non empty trivial V40(1) V146() V147() V148() V149() V150() V151() set
{{w5,m1},{w5}} is non empty set
p2 /. g2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(GoB q1) * (w5,m1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ p2 is Element of bool the U1 of (TOP-REAL 2)
g2 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)
L~ g2 is Element of bool the U1 of (TOP-REAL 2)
g2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len g2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
g2 /. (len g2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(len p1) + 1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
q1 /. ((len p1) + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len (Y_axis q1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Y_axis q1)) is non empty V33() V40( len (Y_axis q1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Y_axis q1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (Y_axis p1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Y_axis p1)) is non empty V33() V40( len (Y_axis p1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Y_axis p1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (Y_axis p2) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Y_axis p2)) is non empty V33() V40( len (Y_axis p2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Y_axis p2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
(Y_axis p2) . 1 is ext-real V14() V15() Element of REAL
f1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 `2 is ext-real V14() V15() Element of REAL
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(Y_axis q1) . m is ext-real V14() V15() Element of REAL
p1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 `2 is ext-real V14() V15() Element of REAL
(Y_axis p1) . m is ext-real V14() V15() Element of REAL
m - (len p1) 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
w5 + (len p1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
m1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p2 /. m1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p2 /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u `2 is ext-real V14() V15() Element of REAL
(Y_axis p2) . m1 is ext-real V14() V15() Element of REAL
(Y_axis q1) . ((len p1) + 1) is ext-real V14() V15() Element of REAL
Col ((GoB 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 (GoB q1)), the U1 of (TOP-REAL 2)))
K180((len (GoB q1)), the U1 of (TOP-REAL 2)) is functional FinSequence-membered M10( the U1 of (TOP-REAL 2))
rng (Col ((GoB q1),1)) is set
q1 /. ((len p1) + (len p2)) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
(Y_axis p2) . (len p2) is ext-real V14() V15() Element of REAL
f2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f2 `2 is ext-real V14() V15() Element of REAL
m is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(Y_axis q1) . m is ext-real V14() V15() Element of REAL
p1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
w5 `2 is ext-real V14() V15() Element of REAL
(Y_axis p1) . m is ext-real V14() V15() Element of REAL
m - (len p1) 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
w5 + (len p1) is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
m1 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
p2 /. m1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 /. m is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p2 /. w5 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
u `2 is ext-real V14() V15() Element of REAL
(Y_axis p2) . m1 is ext-real V14() V15() Element of REAL
(Y_axis q1) . ((len p1) + (len p2)) is ext-real V14() V15() Element of REAL
Col ((GoB q1),(width (GoB 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 (GoB q1)), the U1 of (TOP-REAL 2)))
rng (Col ((GoB q1),(width (GoB q1)))) 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
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
X_axis P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
(X_axis P1) . 1 is ext-real V14() V15() Element of REAL
(X_axis P1) . (len P1) is ext-real V14() V15() Element of REAL
X_axis P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis P1 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis P2 is Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
(Y_axis P2) . 1 is ext-real V14() V15() Element of REAL
(Y_axis P2) . (len P2) is ext-real V14() V15() Element of REAL
L~ P1 is Element of bool the U1 of (TOP-REAL 2)
L~ P2 is Element of bool the U1 of (TOP-REAL 2)
dom P2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
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 ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
P2 /. p1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
P2 /. (p1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
dom P1 is V146() V147() V148() V149() V150() V151() Element of bool NAT
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 ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
P1 /. p1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
P1 /. (p1 + 1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
P1 is Element of bool the U1 of (TOP-REAL 2)
P2 is Element of bool the U1 of (TOP-REAL 2)
P1 \/ P2 is Element of bool the U1 of (TOP-REAL 2)
p1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p1 `1 is ext-real V14() V15() Element of REAL
p2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
p2 `2 is ext-real V14() V15() Element of REAL
q1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q1 `1 is ext-real V14() V15() Element of REAL
q2 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
q2 `2 is ext-real V14() V15() Element of REAL
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)
L~ f1 is Element of bool the U1 of (TOP-REAL 2)
f1 /. 1 is V40(2) FinSequence-like V138() Element 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 /. (len f1) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f1 is non empty 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 non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len f1) is non empty 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
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)
L~ f2 is Element of bool the U1 of (TOP-REAL 2)
f2 /. 1 is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
len f2 is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
f2 /. (len f2) is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
f2 is non empty 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 f2 is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len f2) is non empty V33() V40( len f2) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom f2 is V146() V147() V148() V149() V150() V151() Element of bool NAT
X_axis f1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis f1 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
X_axis f2 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
Y_axis f2 is non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like V136() V137() V138() FinSequence of REAL
len (X_axis f1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (X_axis f1)) is non empty V33() V40( len (X_axis f1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (X_axis f1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
dom (Y_axis f2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (Y_axis f2) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Y_axis f2)) is non empty V33() V40( len (Y_axis f2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
(Y_axis f2) . 1 is ext-real V14() V15() Element of REAL
(Y_axis f2) . (len f2) is ext-real V14() V15() Element of REAL
n is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(Y_axis f2) . n is ext-real V14() V15() Element of REAL
f2 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ f2 is Element of bool the U1 of (TOP-REAL 2)
(f2 /. n) `2 is ext-real V14() V15() Element of REAL
(X_axis f1) . 1 is ext-real V14() V15() Element of REAL
(X_axis f1) . (len f1) is ext-real V14() V15() Element of REAL
n is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(X_axis f1) . n is ext-real V14() V15() Element of REAL
f1 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ f1 is Element of bool the U1 of (TOP-REAL 2)
(f1 /. n) `1 is ext-real V14() V15() Element of REAL
dom (X_axis f2) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (X_axis f2) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (X_axis f2)) is non empty V33() V40( len (X_axis f2)) V146() V147() V148() V149() V150() V151() Element of bool NAT
n is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(X_axis f2) . n is ext-real V14() V15() Element of REAL
f2 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ f2 is Element of bool the U1 of (TOP-REAL 2)
(f2 /. n) `1 is ext-real V14() V15() Element of REAL
dom (Y_axis f1) is V146() V147() V148() V149() V150() V151() Element of bool NAT
len (Y_axis f1) is ext-real non empty V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
Seg (len (Y_axis f1)) is non empty V33() V40( len (Y_axis f1)) V146() V147() V148() V149() V150() V151() Element of bool NAT
n is ext-real V7() V8() V9() V13() V14() V15() V33() V38() V83() V84() V146() V147() V148() V149() V150() V151() Element of NAT
(Y_axis f1) . n is ext-real V14() V15() Element of REAL
f1 /. n is V40(2) FinSequence-like V138() Element of the U1 of (TOP-REAL 2)
L~ f1 is Element of bool the U1 of (TOP-REAL 2)
(f1 /. n) `2 is ext-real V14() V15() Element of REAL