REAL is non empty V46() V185() V186() V187() V191() set
NAT is non empty V18() V19() V20() V46() V51() V52() V185() V186() V187() V188() V189() V190() V191() Element of bool REAL
bool REAL is V46() set
INT is non empty V46() V185() V186() V187() V188() V189() V191() set
COMPLEX is non empty V46() V185() V191() set
NAT is non empty V18() V19() V20() V46() V51() V52() V185() V186() V187() V188() V189() V190() V191() set
bool NAT is V46() set
bool NAT is V46() set
1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
2 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
[:1,1:] is Relation-like RAT -valued INT -valued V147() V148() V149() V150() set
RAT is non empty V46() V185() V186() V187() V188() V191() set
bool [:1,1:] is set
[:[:1,1:],1:] is Relation-like RAT -valued INT -valued V147() V148() V149() V150() set
bool [:[:1,1:],1:] is set
[:[:1,1:],REAL:] is Relation-like V147() V148() V149() set
bool [:[:1,1:],REAL:] is set
[:REAL,REAL:] is Relation-like V46() V147() V148() V149() set
[:[:REAL,REAL:],REAL:] is Relation-like V46() V147() V148() V149() set
bool [:[:REAL,REAL:],REAL:] is V46() set
[:2,2:] is Relation-like RAT -valued INT -valued V147() V148() V149() V150() set
[:[:2,2:],REAL:] is Relation-like V147() V148() V149() set
bool [:[:2,2:],REAL:] is set
bool [:REAL,REAL:] is V46() set
TOP-REAL 2 is non empty V88() V119() V120() V121() V122() V123() V124() V125() TopSpace-like V200() L16()
the carrier of (TOP-REAL 2) is non empty set
bool the carrier of (TOP-REAL 2) is set
{} is set
the Relation-like non-empty empty-yielding RAT -valued functional empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() V46() V51() V53( {} ) FinSequence-like FinSequence-membered V147() V148() V149() V150() V185() V186() V187() V188() V189() V190() V191() set is Relation-like non-empty empty-yielding RAT -valued functional empty ext-real non positive non negative V18() V19() V20() V22() V23() V24() V25() V32() V46() V51() V53( {} ) FinSequence-like FinSequence-membered V147() V148() V149() V150() V185() V186() V187() V188() V189() V190() V191() set
3 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
0 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg 1 is non empty trivial V46() V53(1) V185() V186() V187() V188() V189() V190() Element of bool NAT
{1} is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() set
Seg 2 is non empty V46() V53(2) V185() V186() V187() V188() V189() V190() Element of bool NAT
{1,2} is V185() V186() V187() V188() V189() V190() set
len {} is V18() V19() V20() V51() set
k is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
n is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
k /. n is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. n) `1 is ext-real V25() V32() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
dom n is V185() V186() V187() V188() V189() V190() Element of bool NAT
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
n . G is ext-real V25() V32() Element of REAL
k /. G is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. G) `1 is ext-real V25() V32() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom n is V185() V186() V187() V188() V189() V190() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom G is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len G) is V46() V53( len G) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len n) is V46() V53( len n) V185() V186() V187() V188() V189() V190() Element of bool NAT
f is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
n . f is ext-real V25() V32() Element of REAL
k /. f is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. f) `1 is ext-real V25() V32() Element of REAL
G . f is ext-real V25() V32() Element of REAL
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
n is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
k /. n is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. n) `2 is ext-real V25() V32() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
dom n is V185() V186() V187() V188() V189() V190() Element of bool NAT
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
n . G is ext-real V25() V32() Element of REAL
k /. G is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. G) `2 is ext-real V25() V32() Element of REAL
n is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom n is V185() V186() V187() V188() V189() V190() Element of bool NAT
G is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom G is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len G) is V46() V53( len G) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len n) is V46() V53( len n) V185() V186() V187() V188() V189() V190() Element of bool NAT
f is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
n . f is ext-real V25() V32() Element of REAL
k /. f is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k /. f) `2 is ext-real V25() V32() Element of REAL
G . f is ext-real V25() V32() Element of REAL
k is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
L~ k is Element of bool the carrier of (TOP-REAL 2)
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k /. n is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
n - 1 is ext-real V25() V32() set
1 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k /. (G + 1) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
LSeg (k,G) is Element of bool the carrier of (TOP-REAL 2)
n + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
LSeg (k,n) is Element of bool the carrier of (TOP-REAL 2)
k is non empty set
K196(k) is functional non empty FinSequence-membered M10(k)
n is Relation-like NAT -defined K196(k) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular FinSequence of K196(k)
dom n is V185() V186() V187() V188() V189() V190() Element of bool NAT
width n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width n) is V46() V53( width n) V185() V186() V187() V188() V189() V190() Element of bool NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (n,G) is Relation-like NAT -defined k -valued Function-like V46() FinSequence-like FinSubsequence-like M11(k,K197((len n),k))
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len n),k) is functional FinSequence-membered M10(k)
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
(Col (n,G)) . f is set
Line (n,f) is Relation-like NAT -defined k -valued Function-like V46() FinSequence-like FinSubsequence-like M11(k,K197((width n),k))
K197((width n),k) is functional FinSequence-membered M10(k)
(Line (n,f)) . G is set
n * (f,G) is Element of k
k is non empty set
K196(k) is functional non empty FinSequence-membered M10(k)
n is Relation-like NAT -defined K196(k) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular FinSequence of K196(k)
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
width n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
rng n is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
the Element of rng n is Element of rng n
j is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
f is set
i is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
j is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
j is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K196( the carrier of (TOP-REAL 2)) is functional non empty FinSequence-membered M10( the carrier of (TOP-REAL 2))
k is non empty set
K196(k) is functional non empty FinSequence-membered M10(k)
n is Relation-like NAT -defined K196(k) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular FinSequence of K196(k)
len n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
width n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
the V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
<* the V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)*> is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197(1, the carrier of (TOP-REAL 2)))
K197(1, the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
<*<* the V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)*>*> is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of (TOP-REAL 2)
n is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like non empty trivial V46() V53(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of (TOP-REAL 2)
len n is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
width n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom n is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() Element of bool NAT
Line (n,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width n), the carrier of (TOP-REAL 2)))
K197((width n), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Line (n,G))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Line (n,G))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
((Line (n,G))) . i is ext-real V25() V32() set
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
((Line (n,G))) . j is ext-real V25() V32() set
len ((Line (n,G))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Line (n,G)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len ((Line (n,G)))) is V46() V53( len ((Line (n,G)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
((Line (n,G))) . i is ext-real V25() V32() Element of REAL
((Line (n,G))) . j is ext-real V25() V32() Element of REAL
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width n) is V46() V53( width n) V185() V186() V187() V188() V189() V190() Element of bool NAT
Col (n,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len n), the carrier of (TOP-REAL 2)))
K197((len n), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Col (n,G))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Col (n,G))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
((Col (n,G))) . i is ext-real V25() V32() set
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
((Col (n,G))) . j is ext-real V25() V32() set
len ((Col (n,G))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Col (n,G)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len ((Col (n,G)))) is V46() V53( len ((Col (n,G)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
((Col (n,G))) . i is ext-real V25() V32() Element of REAL
((Col (n,G))) . j is ext-real V25() V32() Element of REAL
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom n is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() Element of bool NAT
Line (n,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width n), the carrier of (TOP-REAL 2)))
K197((width n), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Line (n,G))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Line (n,G))) is set
((Line (n,G))) . i is ext-real V25() V32() Element of REAL
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
((Line (n,G))) . j is ext-real V25() V32() Element of REAL
dom ((Line (n,G))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
len ((Line (n,G))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Line (n,G)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len ((Line (n,G)))) is V46() V53( len ((Line (n,G)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width n) is V46() V53( width n) V185() V186() V187() V188() V189() V190() Element of bool NAT
Col (n,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len n), the carrier of (TOP-REAL 2)))
K197((len n), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Col (n,G))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Col (n,G))) is set
((Col (n,G))) . i is ext-real V25() V32() Element of REAL
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
((Col (n,G))) . j is ext-real V25() V32() Element of REAL
dom ((Col (n,G))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
len ((Col (n,G))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Col (n,G)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len ((Col (n,G)))) is V46() V53( len ((Col (n,G)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
k is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () FinSequence of K196( the carrier of (TOP-REAL 2))
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
n is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
width k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Line (k,G)) is set
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
rng (Line (k,f)) is set
n is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
width k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Line (k,G)) is set
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
rng (Line (k,f)) is set
((Line (k,f))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
i is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom i is V185() V186() V187() V188() V189() V190() Element of bool NAT
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
i . c7 is set
Col (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Col (k,c7))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
(Col (k,c7)) . G is set
k * (G,c7) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
len (Col (k,c7)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Col (k,c7)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
w is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
w /. G is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(Col (k,c7)) . f is set
k * (f,c7) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
w /. f is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
j is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom j is V185() V186() V187() V188() V189() V190() Element of bool NAT
f1 is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
j . f1 is set
len ((Col (k,c7))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Col (k,c7))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len ((Col (k,c7)))) is V46() V53( len ((Col (k,c7)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len i) is V46() V53( len i) V185() V186() V187() V188() V189() V190() Element of bool NAT
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
j . c7 is set
j /. c7 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(j) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
dom (j) is V185() V186() V187() V188() V189() V190() Element of bool NAT
len (j) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (j)) is V46() V53( len (j)) V185() V186() V187() V188() V189() V190() Element of bool NAT
j /. f1 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
g is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Seg (len j) is V46() V53( len j) V185() V186() V187() V188() V189() V190() Element of bool NAT
(j) . c7 is ext-real V25() V32() Element of REAL
(j) . f1 is ext-real V25() V32() Element of REAL
(k * (f,c7)) `1 is ext-real V25() V32() Element of REAL
g `1 is ext-real V25() V32() Element of REAL
(k * (G,c7)) `1 is ext-real V25() V32() Element of REAL
((Col (k,c7))) . G is ext-real V25() V32() Element of REAL
((Col (k,c7))) . f is ext-real V25() V32() Element of REAL
k is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () FinSequence of K196( the carrier of (TOP-REAL 2))
width k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width k) is V46() V53( width k) V185() V186() V187() V188() V189() V190() Element of bool NAT
n is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Col (k,G)) is set
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
rng (Col (k,f)) is set
n is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Col (k,G)) is set
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
rng (Col (k,f)) is set
i is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom i is V185() V186() V187() V188() V189() V190() Element of bool NAT
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
i . c7 is set
len i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
j is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom j is V185() V186() V187() V188() V189() V190() Element of bool NAT
Line (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Line (k,c7))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
Seg (len i) is V46() V53( len i) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
j . c7 is set
k * (c7,f) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
j /. c7 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(j) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
len (j) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
w is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
j . w is set
dom (j) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (j)) is V46() V53( len (j)) V185() V186() V187() V188() V189() V190() Element of bool NAT
k * (c7,G) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
j /. w is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
f1 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Seg (len j) is V46() V53( len j) V185() V186() V187() V188() V189() V190() Element of bool NAT
((Col (k,f))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
(j) . c7 is ext-real V25() V32() Element of REAL
(j) . w is ext-real V25() V32() Element of REAL
(k * (c7,f)) `2 is ext-real V25() V32() Element of REAL
f1 `2 is ext-real V25() V32() Element of REAL
len ((Line (k,c7))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Line (k,c7)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom ((Line (k,c7))) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len ((Line (k,c7)))) is V46() V53( len ((Line (k,c7)))) V185() V186() V187() V188() V189() V190() Element of bool NAT
(Line (k,c7)) . f is set
dom (Line (k,c7)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
g is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
g /. f is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(Line (k,c7)) . G is set
g /. G is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(k * (c7,G)) `2 is ext-real V25() V32() Element of REAL
((Line (k,c7))) . G is ext-real V25() V32() Element of REAL
((Line (k,c7))) . f is ext-real V25() V32() Element of REAL
k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
[k,n] is set
{k,n} is V185() V186() V187() V188() V189() V190() set
{k} is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() set
{{k,n},{k}} is set
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
[G,f] is set
{G,f} is V185() V186() V187() V188() V189() V190() set
{G} is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() set
{{G,f},{G}} is set
i is set
j is Relation-like non empty-yielding NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () () () FinSequence of K196( the carrier of (TOP-REAL 2))
j * (k,n) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
j * (G,f) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Indices j is set
Line (j,k) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width j), the carrier of (TOP-REAL 2)))
width j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((width j), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
len (Line (j,k)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Line (j,k)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (Line (j,k))) is V46() V53( len (Line (j,k))) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom j is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (width j) is V46() V53( width j) V185() V186() V187() V188() V189() V190() Element of bool NAT
[:(dom j),(Seg (width j)):] is Relation-like INT -valued RAT -valued V147() V148() V149() V150() set
(Line (j,k)) . n is set
rng (Line (j,k)) is set
Col (j,n) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len j), the carrier of (TOP-REAL 2)))
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len j), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
len (Col (j,n)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Col (j,n)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (Col (j,n))) is V46() V53( len (Col (j,n))) V185() V186() V187() V188() V189() V190() Element of bool NAT
Line (j,G) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width j), the carrier of (TOP-REAL 2)))
len (Line (j,G)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Line (j,G)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (Line (j,G))) is V46() V53( len (Line (j,G))) V185() V186() V187() V188() V189() V190() Element of bool NAT
Col (j,f) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len j), the carrier of (TOP-REAL 2)))
len (Col (j,f)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Col (j,f)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (Col (j,f))) is V46() V53( len (Col (j,f))) V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len j) is V46() V53( len j) V185() V186() V187() V188() V189() V190() Element of bool NAT
(Line (j,G)) . f is set
rng (Line (j,G)) is set
(Col (j,f)) . G is set
rng (Col (j,f)) is set
(Col (j,n)) . k is set
rng (Col (j,n)) is set
k is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
k /. 1 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k | n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(k | n) /. 1 is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
G is Relation-like non empty-yielding NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () () () FinSequence of K196( the carrier of (TOP-REAL 2))
Col (G,1) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len G), the carrier of (TOP-REAL 2)))
len G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len G), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Col (G,1)) is set
Seg n is V46() V53(n) V185() V186() V187() V188() V189() V190() Element of bool NAT
k is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k /. n is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
k | n is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len (k | n) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
(k | n) /. (len (k | n)) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
G is Relation-like non empty-yielding NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () () () FinSequence of K196( the carrier of (TOP-REAL 2))
width G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (G,(width G)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len G), the carrier of (TOP-REAL 2)))
len G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len G), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Col (G,(width G))) is set
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg n is V46() V53(n) V185() V186() V187() V188() V189() V190() Element of bool NAT
k is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
rng k is set
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k /. G is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
j is Relation-like non empty-yielding NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () () () FinSequence of K196( the carrier of (TOP-REAL 2))
Col (j,n) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len j), the carrier of (TOP-REAL 2)))
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
K197((len j), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
rng (Col (j,n)) is set
j * (f,i) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
dom j is V185() V186() V187() V188() V189() V190() Element of bool NAT
(rng k) /\ (rng (Col (j,n))) is set
k . G is set
j * (f,n) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Seg (len j) is V46() V53( len j) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom (Col (j,n)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
len (Col (j,n)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (Col (j,n))) is V46() V53( len (Col (j,n))) V185() V186() V187() V188() V189() V190() Element of bool NAT
(Col (j,n)) . f is set
n is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
k is Relation-like non empty-yielding NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular () () () () FinSequence of K196( the carrier of (TOP-REAL 2))
width k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width k) is V46() V53( width k) V185() V186() V187() V188() V189() V190() Element of bool NAT
len k is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom k is V185() V186() V187() V188() V189() V190() Element of bool NAT
G is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
G + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len k) is V46() V53( len k) V185() V186() V187() V188() V189() V190() Element of bool NAT
f is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,i) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Del ((Line (k,i)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
len (Del ((Line (k,i)),n)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Line (k,i)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Line (k,i)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
j is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
j + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg f is V46() V53(f) V185() V186() V187() V188() V189() V190() Element of bool NAT
[:(Seg (len k)),(Seg f):] is Relation-like INT -valued RAT -valued V147() V148() V149() V150() set
i is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
j is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
[i,j] is set
{i,j} is V185() V186() V187() V188() V189() V190() set
{i} is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() set
{{i,j},{i}} is set
Line (k,i) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Del ((Line (k,i)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(Del ((Line (k,i)),n)) . j is set
c7 is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
len c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom c7 is V185() V186() V187() V188() V189() V190() Element of bool NAT
c7 . j is set
l is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
i is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular Matrix of len k,f, the carrier of (TOP-REAL 2)
Indices i is set
len i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len i) is V46() V53( len i) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom i is V185() V186() V187() V188() V189() V190() Element of bool NAT
width i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
[:(dom k),(Seg f):] is Relation-like INT -valued RAT -valued V147() V148() V149() V150() set
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Del ((Line (k,j)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
i * (j,c7) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(Del ((Line (k,j)),n)) . c7 is set
[j,c7] is set
{j,c7} is V185() V186() V187() V188() V189() V190() set
{j} is non empty trivial V53(1) V185() V186() V187() V188() V189() V190() set
{{j,c7},{j}} is set
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (k,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
i * (j,c7) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(Line (k,j)) . c7 is set
c7 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
(Line (k,j)) . (c7 + 1) is set
Del ((Line (k,j)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(Del ((Line (k,j)),n)) . c7 is set
len (Line (k,j)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
f + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (Line (k,j))) is V46() V53( len (Line (k,j))) V185() V186() V187() V188() V189() V190() Element of bool NAT
dom (Line (k,j)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (i,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len i), the carrier of (TOP-REAL 2)))
K197((len i), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Col (k,j) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
K197((len k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
j + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,(j + 1)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
f + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Col (i,j)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Col (k,j)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (Col (k,(j + 1))) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
(Col (i,j)) . c7 is set
i * (c7,j) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Line (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Del ((Line (k,c7)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(Del ((Line (k,c7)),n)) . j is set
(Line (k,c7)) . j is set
(Col (k,j)) . c7 is set
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V46() V51() set
Line (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
len (Line (k,c7)) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (Line (k,c7)) is V185() V186() V187() V188() V189() V190() Element of bool NAT
Seg (len (Line (k,c7))) is V46() V53( len (Line (k,c7))) V185() V186() V187() V188() V189() V190() Element of bool NAT
(Col (i,j)) . c7 is set
i * (c7,j) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
Del ((Line (k,c7)),n) is Relation-like NAT -defined Function-like V46() FinSequence-like FinSubsequence-like set
(Del ((Line (k,c7)),n)) . j is set
(Line (k,c7)) . (j + 1) is set
(Col (k,(j + 1))) . c7 is set
1 - 1 is ext-real V25() V32() set
j is Relation-like NAT -defined K196( the carrier of (TOP-REAL 2)) -valued Function-like V46() FinSequence-like FinSubsequence-like tabular FinSequence of K196( the carrier of (TOP-REAL 2))
len j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
width j is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom j is V185() V186() V187() V188() V189() V190() Element of bool NAT
Line (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
K197((width k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
((Line (k,c7))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
f + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (j,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width j), the carrier of (TOP-REAL 2)))
K197((width j), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
l is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(l) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
w is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(w) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
ww is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (l) is V185() V186() V187() V188() V189() V190() Element of bool NAT
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (l) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (l)) is V46() V53( len (l)) V185() V186() V187() V188() V189() V190() Element of bool NAT
len l is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (w) is V185() V186() V187() V188() V189() V190() Element of bool NAT
len (w) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (w)) is V46() V53( len (w)) V185() V186() V187() V188() V189() V190() Element of bool NAT
len w is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
l . ww is set
j * (c7,ww) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
l . i is set
j * (c7,i) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
w . ww is set
ww + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
w . (ww + 1) is set
w . i is set
i + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
w . (i + 1) is set
dom l is V185() V186() V187() V188() V189() V190() Element of bool NAT
l /. ww is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
l /. i is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(l) . ww is ext-real V25() V32() Element of REAL
(j * (c7,ww)) `1 is ext-real V25() V32() Element of REAL
(l) . i is ext-real V25() V32() Element of REAL
(j * (c7,i)) `1 is ext-real V25() V32() Element of REAL
k * (c7,ww) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
k * (c7,(ww + 1)) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
k * (c7,i) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
k * (c7,(i + 1)) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
dom w is V185() V186() V187() V188() V189() V190() Element of bool NAT
w /. ww is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
w /. (ww + 1) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
w /. i is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
w /. (i + 1) is V53(2) FinSequence-like V149() Element of the carrier of (TOP-REAL 2)
(w) . ww is ext-real V25() V32() Element of REAL
(k * (c7,ww)) `1 is ext-real V25() V32() Element of REAL
(w) . (ww + 1) is ext-real V25() V32() Element of REAL
(k * (c7,(ww + 1))) `1 is ext-real V25() V32() Element of REAL
(w) . i is ext-real V25() V32() Element of REAL
(k * (c7,i)) `1 is ext-real V25() V32() Element of REAL
(w) . (i + 1) is ext-real V25() V32() Element of REAL
(k * (c7,(i + 1))) `1 is ext-real V25() V32() Element of REAL
((Line (j,c7))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (width j) is V46() V53( width j) V185() V186() V187() V188() V189() V190() Element of bool NAT
Col (j,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len j), the carrier of (TOP-REAL 2)))
K197((len j), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
Col (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
K197((len k), the carrier of (TOP-REAL 2)) is functional FinSequence-membered M10( the carrier of (TOP-REAL 2))
c7 + 1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Col (k,(c7 + 1)) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((len k), the carrier of (TOP-REAL 2)))
((Col (j,c7))) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
c7 is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Line (j,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width j), the carrier of (TOP-REAL 2)))
Line (k,c7) is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like M11( the carrier of (TOP-REAL 2),K197((width k), the carrier of (TOP-REAL 2)))
l is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(l) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
w is Relation-like NAT -defined the carrier of (TOP-REAL 2) -valued Function-like V46() FinSequence-like FinSubsequence-like FinSequence of the carrier of (TOP-REAL 2)
(w) is Relation-like NAT -defined REAL -valued Function-like V46() FinSequence-like FinSubsequence-like V147() V148() V149() FinSequence of REAL
ww is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
dom (l) is V185() V186() V187() V188() V189() V190() Element of bool NAT
i is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
len (l) is ext-real non negative V18() V19() V20() V24() V25() V32() V45() V46() V51() V169() V185() V186() V187() V188() V189() V190() Element of NAT
Seg (len (l)) is V46() V53( len (l)) V185() V186() V187()