:: MATRIX_7 semantic presentation

REAL is set
NAT is non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal Element of bool REAL

{} is set

NAT is non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal set

INT is set
1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
3 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg 1 is non empty trivial V40() 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial V40() V44() 1 -element set
Seg 2 is non empty V40() 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is V40() V44() set

[:(Seg 2),(Seg 2):] is non empty V40() set
bool [:(Seg 2),(Seg 2):] is non empty cup-closed diff-closed preBoolean V40() V44() set

[1,1] is set
{1,1} is V40() V44() set
{{1,1},{1}} is V40() V44() set
{[1,1]} is Function-like non empty trivial V40() 1 -element set

[1,2] is set
{{1,2},{1}} is V40() V44() set
{[1,2]} is Function-like non empty trivial V40() 1 -element set

1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT

rng n is V40() set
n . 2 is set
dom n is V40() set

len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
n . 1 is set

len <*1,2*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
len <*2,1*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
dom n is V40() Element of bool NAT
rng n is V40() set
K is set
n . 1 is set
n . 2 is set
A is set
n . A is set
A is set
f is set
n . A is set
n . f is set
A is set
f is set
n . f is set
len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is set
n . 1 is set
n . 2 is set

A is set
f is set
n . A is set
n . f is set
A is set
f is set
n . f is set
len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is set
n . 2 is set
n . 1 is set

Permutations 2 is non empty permutational set
{<*1,2*>,<*2,1*>} is functional V40() V44() set
n is set
{(),<*2,1*>} is functional V40() V44() set
n is set

dom n is V40() set
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
n . A is set
n . f is set
len <*1,2*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
n is non empty set

len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

A + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT

(mid (K,1,A)) ^ (mid (K,(A + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n

n is non empty set

len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) -' 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

Seg ((len K) -' 2) is V40() (len K) -' 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= (len K) -' 2 ) } is set

(len K) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
mid (K,((len K) -' 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(K | ((len K) -' 2)) ^ (mid (K,((len K) -' 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(len K) - 2 is V33() V34() ext-real set
((len K) -' 2) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) - 1 is V33() V34() ext-real set
((len K) - 1) - 1 is V33() V34() ext-real set
(((len K) - 1) - 1) + 1 is V33() V34() ext-real set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 2) - 2 is V33() V34() ext-real set

mid (K,(((len K) -' 2) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(mid (K,1,((len K) -' 2))) ^ (mid (K,(((len K) -' 2) + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
mid (K,(((len K) -' 2) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n

[:NAT,n:] is non empty non trivial V40() set

{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

((len K) - 2) + 1 is V33() V34() ext-real set
n is non empty set

len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

Seg ((len K) -' 1) is V40() (len K) -' 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= (len K) -' 1 ) } is set

(K | ((len K) -' 1)) ^ (mid (K,(len K),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(len K) - 1 is V33() V34() ext-real set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 1) - 1 is V33() V34() ext-real set

((len K) -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
mid (K,(((len K) -' 1) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(mid (K,1,((len K) -' 1))) ^ (mid (K,(((len K) -' 1) + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n

[:NAT,n:] is non empty non trivial V40() set

{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= 0 ) } is set

((len K) -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
mid (K,(((len K) -' 1) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n

the carrier of () is non empty set
len () is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len ()) is V40() len () -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
n is Element of the carrier of ()

dom K is V40() set

f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
K . f is set
K . f2 is set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

the carrier of () is non empty set
Permutations n is non empty permutational set
len () is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len ()) is V40() len () -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
K is Element of the carrier of ()

A is Element of the carrier of ()

K * A is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of ()) associative Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the multF of () . (K,A) is Element of the carrier of ()
[K,A] is set
{K,A} is V40() set
{K} is non empty trivial V40() 1 -element set
{{K,A},{K}} is V40() V44() set
the multF of () . [K,A] is set
f2 * f is Relation-like Seg (len ()) -defined Seg (len ()) -defined Seg (len ()) -valued Seg (len ()) -valued Function-like one-to-one total quasi_total onto bijective bijective V40() Element of bool [:(Seg (len ())),(Seg (len ())):]
[:(Seg (len ())),(Seg (len ())):] is V40() set
bool [:(Seg (len ())),(Seg (len ())):] is non empty cup-closed diff-closed preBoolean V40() V44() set
n is Element of the carrier of ()
K is Element of the carrier of ()
n * K is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of ()) associative Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the multF of () . (n,K) is Element of the carrier of ()
[n,K] is set
{n,K} is V40() set
{n} is non empty trivial V40() 1 -element set
{{n,K},{n}} is V40() V44() set
the multF of () . [n,K] is set

len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len f) is V40() len f -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
dom f is V40() Element of bool NAT

F . 2 is set
f2 * A is Relation-like Seg (len ()) -defined Seg (len ()) -defined Seg (len ()) -valued Seg (len ()) -valued Function-like one-to-one total quasi_total onto bijective bijective V40() Element of bool [:(Seg (len ())),(Seg (len ())):]
[:(Seg (len ())),(Seg (len ())):] is V40() set
bool [:(Seg (len ())),(Seg (len ())):] is non empty cup-closed diff-closed preBoolean V40() V44() set
f . 1 is set
(f2 * A) . 1 is set

len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len n) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom n is V40() Element of bool NAT
Product n is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of ()) associative Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the multF of () "**" n is Element of the carrier of ()
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
2 * K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(2 * K) + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
2 * K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
2 * A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
2 * (A + 1) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of ()
the multF of () "**" f is Element of the carrier of ()
(2 * A) + 2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len f) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len f) - 1 is V33() V34() ext-real set
(len f) - ((len f) -' 1) is V33() V34() ext-real set
((len f) - ((len f) -' 1)) + 1 is V33() V34() ext-real set
(len f) - ((len f) - 1) is V33() V34() ext-real set
((len f) - ((len f) - 1)) + 1 is V33() V34() ext-real set
mid (f,((len f) -' 1),(len f)) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Seg (len f) is V40() len f -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len f ) } is set
f . (len f) is set
len (mid (f,((len f) -' 1),(len f))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Element of the carrier of ()
the multF of () "**" (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Element of the carrier of ()
(len (mid (f,((len f) -' 1),(len f)))) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Seg ((len (mid (f,((len f) -' 1),(len f)))) -' 1) is V40() (len (mid (f,((len f) -' 1),(len f)))) -' 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= (len (mid (f,((len f) -' 1),(len f)))) -' 1 ) } is set
(mid (f,((len f) -' 1),(len f))) | (Seg ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Element of the carrier of ()
the multF of () "**" ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Element of the carrier of ()
1 + ((len f) -' 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + ((len f) -' 1)) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(1 + ((len f) -' 1)) - 1 is V33() V34() ext-real set
1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + 1) - 1 is V33() V34() ext-real set
(len f) -' ((len f) -' 1) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len f) -' ((len f) -' 1)) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len (mid (f,((len f) -' 1),(len f)))) - 1 is V33() V34() ext-real set
((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 is set
(mid (f,((len f) -' 1),(len f))) . 1 is set
f . ((len f) -' 1) is set
(len f) -' 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f | ((len f) -' 2) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Seg ((len f) -' 2) is V40() (len f) -' 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= (len f) -' 2 ) } is set

dom (f | ((len f) -' 2)) is V40() Element of bool NAT
X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(f | ((len f) -' 2)) . X is set
len (f | ((len f) -' 2)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (f | ((len f) -' 2))) is V40() len (f | ((len f) -' 2)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (f | ((len f) -' 2)) ) } is set
f . X is set

len (f | ((len f) -' 2)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product (f | ((len f) -' 2)) is Element of the carrier of ()
the multF of () "**" (f | ((len f) -' 2)) is Element of the carrier of ()
1_ () is non being_of_order_0 Element of the carrier of ()
(f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
Product (mid (f,((len f) -' 1),(len f))) is Element of the carrier of ()
the multF of () "**" (mid (f,((len f) -' 1),(len f))) is Element of the carrier of ()
(Product (f | ((len f) -' 2))) * (Product (mid (f,((len f) -' 1),(len f)))) is Element of the carrier of ()
the multF of () . ((Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))) is Element of the carrier of ()
[(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))] is set
{(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))} is V40() set
{(Product (f | ((len f) -' 2)))} is non empty trivial V40() 1 -element set
{{(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))},{(Product (f | ((len f) -' 2)))}} is V40() V44() set
the multF of () . [(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))] is set
2 + ((len f) -' 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(2 + ((len f) -' 1)) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(2 + ((len f) -' 1)) - 1 is V33() V34() ext-real set
1 + (len (mid (f,((len f) -' 1),(len f)))) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(1 + (len (mid (f,((len f) -' 1),(len f))))) - 1 is V33() V34() ext-real set
len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) is V40() len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ) } is set
dom ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V40() Element of bool NAT
rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V40() set
Y is Element of the carrier of ()
X is Element of the carrier of ()

1 -tuples_on the carrier of () is functional non empty FinSequence-membered FinSequenceSet of the carrier of ()
the carrier of () * is functional non empty FinSequence-membered FinSequenceSet of the carrier of ()
{ b1 where b1 is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of () * : len b1 = 1 } is set
[1,X] is set
{1,X} is V40() set
{{1,X},{1}} is V40() V44() set
{[1,X]} is Function-like non empty trivial V40() 1 -element set
Product <*X*> is Element of the carrier of ()
the multF of () "**" <*X*> is Element of the carrier of ()
(len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f)))) is V33() V34() ext-real set
((len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f))))) + 1 is V33() V34() ext-real set
(mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 is set
(mid (f,((len f) -' 1),(len f))) . ((1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1) is set
len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f))))) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
Seg (len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) is V40() len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) ) } is set
dom (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V40() Element of bool NAT
rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V40() set
F is Element of the carrier of ()
B is Element of the carrier of ()

[1,B] is set
{1,B} is V40() set
{{1,B},{1}} is V40() V44() set
{[1,B]} is Function-like non empty trivial V40() 1 -element set
Product <*B*> is Element of the carrier of ()
the multF of () "**" <*B*> is Element of the carrier of ()
((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ^ (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Relation-like NAT -defined the carrier of () -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of ()
(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) * (Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) is Element of the carrier of ()
the multF of () . ((Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))) is Element of the carrier of ()
[(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))] is set
{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))} is V40() set
{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)))} is non empty trivial V40() 1 -element set
{{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))},{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)))}} is V40() V44() set
the multF of () . [(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))] is set

len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of ()
the multF of () "**" f is Element of the carrier of ()
2 * 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of ()
the multF of () "**" f is Element of the carrier of ()
1_ () is non being_of_order_0 Element of the carrier of ()

[:NAT, the carrier of ():] is non empty non trivial V40() set

len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom A is V40() Element of bool NAT
Product A is Element of the carrier of ()
the multF of () "**" A is Element of the carrier of ()
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
2 * A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT

the carrier of A is non empty non trivial set
the carrier of A * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A

Det f is Element of the carrier of A
f * (1,1) is Element of the carrier of A
f * (2,2) is Element of the carrier of A
(f * (1,1)) * (f * (2,2)) is Element of the carrier of A
the multF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty cup-closed diff-closed preBoolean set
the multF of A . ((f * (1,1)),(f * (2,2))) is Element of the carrier of A
[(f * (1,1)),(f * (2,2))] is set
{(f * (1,1)),(f * (2,2))} is V40() set
{(f * (1,1))} is non empty trivial V40() 1 -element set
{{(f * (1,1)),(f * (2,2))},{(f * (1,1))}} is V40() V44() set
the multF of A . [(f * (1,1)),(f * (2,2))] is set
f * (1,2) is Element of the carrier of A
f * (2,1) is Element of the carrier of A
(f * (1,2)) * (f * (2,1)) is Element of the carrier of A
the multF of A . ((f * (1,2)),(f * (2,1))) is Element of the carrier of A
[(f * (1,2)),(f * (2,1))] is set
{(f * (1,2)),(f * (2,1))} is V40() set
{(f * (1,2))} is non empty trivial V40() 1 -element set
{{(f * (1,2)),(f * (2,1))},{(f * (1,2))}} is V40() V44() set
the multF of A . [(f * (1,2)),(f * (2,1))] is set
((f * (1,1)) * (f * (2,2))) - ((f * (1,2)) * (f * (2,1))) is Element of the carrier of A
- ((f * (1,2)) * (f * (2,1))) is Element of the carrier of A
((f * (1,1)) * (f * (2,2))) + (- ((f * (1,2)) * (f * (2,1)))) is Element of the carrier of A
the addF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
the addF of A . (((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))) is Element of the carrier of A
[((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))] is set
{((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))} is V40() set
{((f * (1,1)) * (f * (2,2)))} is non empty trivial V40() 1 -element set
{{((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))},{((f * (1,1)) * (f * (2,2)))}} is V40() V44() set
the addF of A . [((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))] is set

n . 1 is set

{n,K} is functional V40() V44() set

[:(), the carrier of A:] is non empty set
bool [:(), the carrier of A:] is non empty cup-closed diff-closed preBoolean set

the multF of A "**" (Path_matrix (X,f)) is Element of the carrier of A
FinOmega () is V40() Element of Fin ()

the addF of A \$\$ ((),()) is Element of the carrier of A
[:(Fin ()), the carrier of A:] is non empty set
bool [:(Fin ()), the carrier of A:] is non empty cup-closed diff-closed preBoolean set
s is Relation-like Fin () -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:(Fin ()), the carrier of A:]
s . () is Element of the carrier of A
s . {} is set
{X} is functional non empty trivial V40() V44() 1 -element set
s . {X} is set
() . X is Element of the carrier of A

() . B is Element of the carrier of A
the addF of A . ((() . X),(() . B)) is Element of the carrier of A
[(() . X),(() . B)] is set
{(() . X),(() . B)} is V40() set
{(() . X)} is non empty trivial V40() 1 -element set
{{(() . X),(() . B)},{(() . X)}} is V40() V44() set
the addF of A . [(() . X),(() . B)] is set
{.X.} is functional non empty trivial V40() V44() 1 -element Element of Fin ()
x is V40() Element of Fin ()
px is set
() \ x is V40() Element of Fin ()
{K} is functional non empty trivial V40() V44() 1 -element set
{B} is functional non empty trivial V40() V44() 1 -element set
x \/ {B} is V40() set
s . (x \/ {B}) is set
s . x is Element of the carrier of A
the addF of A . ((s . x),(() . B)) is Element of the carrier of A
[(s . x),(() . B)] is set
{(s . x),(() . B)} is V40() set
{(s . x)} is non empty trivial V40() 1 -element set
{{(s . x),(() . B)},{(s . x)}} is V40() V44() set
the addF of A . [(s . x),(() . B)] is set

the multF of A "**" (Path_matrix (B,f)) is Element of the carrier of A
X . 2 is set
B . 2 is set
len (Path_matrix (X,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
[:NAT, the carrier of A:] is non empty non trivial V40() set
bool [:NAT, the carrier of A:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
(Path_matrix (X,f)) . 1 is set
px is Relation-like NAT -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of A:]
px . 1 is Element of the carrier of A
px . 2 is Element of the carrier of A
dom (Path_matrix (X,f)) is V40() Element of bool NAT
X . 1 is set
(Path_matrix (X,f)) . 2 is set
len (Path_matrix (B,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Path_matrix (B,f)) . 1 is set
y is Relation-like NAT -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of A:]
y . 1 is Element of the carrier of A
y . 2 is Element of the carrier of A
dom (Path_matrix (B,f)) is V40() Element of bool NAT
B . 1 is set
(Path_matrix (B,f)) . 2 is set
1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . (1 + 1) is Element of the carrier of A
(Path_matrix (B,f)) . (1 + 1) is set
the multF of A . ((y . 1),((Path_matrix (B,f)) . (1 + 1))) is set
[(y . 1),((Path_matrix (B,f)) . (1 + 1))] is set
{(y . 1),((Path_matrix (B,f)) . (1 + 1))} is V40() set
{(y . 1)} is non empty trivial V40() 1 -element set
{{(y . 1),((Path_matrix (B,f)) . (1 + 1))},{(y . 1)}} is V40() V44() set
the multF of A . [(y . 1),((Path_matrix (B,f)) . (1 + 1))] is set

len pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len pd) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product pd is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of ()) associative Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the multF of () "**" pd is Element of the carrier of ()
dom pd is V40() Element of bool NAT
- (( the multF of A "**" (Path_matrix (B,f))),B) is Element of the carrier of A
- ( the multF of A "**" (Path_matrix (B,f))) is Element of the carrier of A

Product F is Element of the carrier of ()
the multF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of ()) associative Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty cup-closed diff-closed preBoolean set
the multF of () "**" F is Element of the carrier of ()

[:NAT, the carrier of ():] is non empty non trivial V40() set
Product (<*> the carrier of ()) is Element of the carrier of ()
the multF of () "**" (<*> the carrier of ()) is Element of the carrier of ()
1_ () is non being_of_order_0 Element of the carrier of ()
0 mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len F is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len F) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom F is V40() Element of bool NAT
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
F . pd is set
- (( the multF of A "**" (Path_matrix (X,f))),X) is Element of the carrier of A

len pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len pd) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product pd is Element of the carrier of ()
the multF of () "**" pd is Element of the carrier of ()
dom pd is V40() Element of bool NAT
px . (1 + 1) is Element of the carrier of A
(Path_matrix (X,f)) . (1 + 1) is set
the multF of A . ((px . 1),((Path_matrix (X,f)) . (1 + 1))) is set
[(px . 1),((Path_matrix (X,f)) . (1 + 1))] is set
{(px . 1),((Path_matrix (X,f)) . (1 + 1))} is V40() set
{(px . 1)} is non empty trivial V40() 1 -element set
{{(px . 1),((Path_matrix (X,f)) . (1 + 1))},{(px . 1)}} is V40() V44() set
the multF of A . [(px . 1),((Path_matrix (X,f)) . (1 + 1))] is set

the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set

f is Element of the carrier of K

width (f * A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
width A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (f * A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (f * A)) is V40() len (f * A) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len (f * A) ) } is set
rng (f * A) is V40() set

len f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (f * A) is V40() Element of bool NAT
F is set

K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
0. (n,K,A) is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,A, the carrier of n
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
len (0. (n,K,A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (0. (n,K,A)) is V40() Element of bool NAT
Seg K is V40() K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
A -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = A } is set
0. n is V59(n) Element of the carrier of n

Seg A is V40() A -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= A ) } is set

{(0. n)} is non empty trivial V40() 1 -element set
[:(Seg A),{(0. n)}:] is V40() set
bool [:(Seg A),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
K |-> (A |-> (0. n)) is Relation-like NAT -defined A -tuples_on the carrier of n -valued Function-like V40() K -element FinSequence-like FinSubsequence-like Element of K -tuples_on (A -tuples_on the carrier of n)
K -tuples_on (A -tuples_on the carrier of n) is functional non empty FinSequence-membered FinSequenceSet of A -tuples_on the carrier of n
(A -tuples_on the carrier of n) * is functional non empty FinSequence-membered FinSequenceSet of A -tuples_on the carrier of n
{ b1 where b1 is Relation-like NAT -defined A -tuples_on the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of (A -tuples_on the carrier of n) * : len b1 = K } is set
(Seg K) --> (A |-> (0. n)) is Relation-like Seg K -defined {(A |-> (0. n))} -valued Function-like total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(A |-> (0. n))}:]
{(A |-> (0. n))} is functional non empty trivial V40() V44() 1 -element set
[:(Seg K),{(A |-> (0. n))}:] is V40() set
bool [:(Seg K),{(A |-> (0. n))}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
len (K |-> (A |-> (0. n))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations K is non empty permutational set
len () is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len ()) is V40() len () -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
Seg K is V40() K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b1 & b1 <= K ) } is set

f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A . f is set
[:(Seg K),(Seg K):] is V40() set
bool [:(Seg K),(Seg K):] is non empty cup-closed diff-closed preBoolean V40() V44() set

0. n is V59(n) Element of the carrier of n
the carrier of n is non empty non trivial set
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
0. (n,K,K) is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Det (0. (n,K,K)) is Element of the carrier of n
Permutations K is non empty permutational set
FinOmega () is V40() Element of Fin ()

Path_product (0. (n,K,K)) is Relation-like Permutations K -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of n:]
[:(), the carrier of n:] is non empty set
bool [:(), the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
[:(Fin ()), the carrier of n:] is non empty set
bool [:(Fin ()), the carrier of n:] is non empty cup-closed diff-closed preBoolean set
(Fin ()) --> (0. n) is Relation-like Fin () -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Fin ()), the carrier of n:]
X is Relation-like Fin () -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Fin ()), the carrier of n:]
X . () is Element of the carrier of n
X . {} is set
B is Element of the carrier of n
the addF of n . ((0. n),B) is Element of the carrier of n
[(0. n),B] is set
{(0. n),B} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),B},{(0. n)}} is V40() V44() set
the addF of n . [(0. n),B] is set
dom (Path_product (0. (n,K,K))) is set
() --> (0. n) is Relation-like Permutations K -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of n:]
B is set
(Path_product (0. (n,K,K))) . B is set
(() --> (0. n)) . B is set
len () is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (