:: MATRIX_9 semantic presentation

REAL is set
NAT is non empty non trivial V29() V30() V31() non finite V48() V49() Element of bool REAL

{} is Function-like functional empty V29() V30() V31() V33() V34() V35() V36() ext-real non positive non negative V40() finite V47() V48() V50( {} ) FinSequence-membered set

NAT is non empty non trivial V29() V30() V31() non finite V48() V49() set

INT is set
1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
2 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
3 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
0 is Function-like functional empty V29() V30() V31() V33() V34() V35() V36() ext-real non positive non negative V40() finite V47() V48() V50( {} ) FinSequence-membered Element of NAT
Seg 1 is non empty trivial finite V50(1) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V47() V50(1) set
Seg 2 is non empty finite V50(2) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V47() set

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

[1,1] is set
{[1,1]} is Function-like non empty trivial finite V50(1) set

[1,2] is set
{[1,2]} is Function-like non empty trivial finite V50(1) set

1 + 1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT

Seg 3 is non empty finite V50(3) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set

[:(Seg 3),(Seg 3):] is non empty finite set
bool [:(Seg 3),(Seg 3):] is non empty cup-closed diff-closed preBoolean finite V47() set

[1,3] is set
{[1,3]} is Function-like non empty trivial finite V50(1) set

(1 + 1) + 1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
Permutations 1 is non empty permutational set

[:(Seg 1),(Seg 1):] is non empty finite set
bool [:(Seg 1),(Seg 1):] is non empty cup-closed diff-closed preBoolean finite V47() set
{()} is functional non empty trivial finite V47() V50(1) set
{1,2,3} is non empty finite set
Permutations 2 is non empty permutational set

{<*1,2*>,<*2,1*>} is functional non empty finite V47() set

the carrier of () is non empty set
len () is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len ()) is finite V50( len ()) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
n is set
K is set
{n} is non empty trivial finite V50(1) set

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set

Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set
{()} is functional non empty trivial finite V47() V50(1) set
F1() is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Permutations F1() is non empty permutational set
Fin (Permutations F1()) is non empty cup-closed diff-closed preBoolean set
len (Permutations F1()) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len (Permutations F1())) is finite V50( len (Permutations F1())) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations F1()) ) } is set
F2() is non empty finite Element of Fin (Permutations F1())
n is set
K is set
{n} is non empty trivial finite V50(1) set
K \/ {n} is non empty set

{a} is functional non empty trivial finite V47() V50(1) set
M is non empty finite Element of Fin (Permutations F1())

M is non empty finite Element of Fin (Permutations F1())
{a} is functional non empty trivial finite V47() V50(1) set
M \/ {a} is non empty finite set

{a} is functional non empty trivial finite V47() V50(1) set
K \/ {a} is non empty set

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set

dom K is finite set
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set
dom (id (Seg n)) is finite set

(Rev ()) . 1 is set
(Rev ()) . 2 is set

n . 1 is set

len n is non empty V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(Rev n) . (len n) is set
() . 1 is set
n . (len n) is set
(Rev n) . 1 is set
n . 2 is set
dom (Rev n) is finite Element of bool NAT

dom n is set
rng n is set
dom () is finite V50(2) Element of bool NAT
n . 1 is set
n . 2 is set
K is set
n . K is set
K is set
n . K is set
(Rev (id (Seg 2))) . K is set
dom (Rev (id (Seg 2))) is finite Element of bool NAT
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set

Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set

[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set

Permutations n is non empty permutational set

dom (Rev K) is finite Element of bool NAT
rng () is finite set
rng (Rev K) is finite set
rng K is finite set

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set

Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set

dom (Rev K) is finite Element of bool NAT
rng K is finite set
rng (Rev K) is finite set

{(),(Rev ())} is functional non empty finite V47() set
n is set

rng K is finite set
dom K is finite set

n 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 V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set
[:(), the carrier of K:] is non empty set
bool [:(), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
len () is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len ()) is finite V50( len ()) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total commutative associative having_a_unity Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
M is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of K:]

M . N is Element of the carrier of K

the multF of K \$\$ (Path_matrix (N,a)) is Element of the carrier of K
M is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of K:]
N is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of K:]

M . i is Element of the carrier of K

the multF of K \$\$ (Path_matrix (i,a)) is Element of the carrier of K
N . i is Element of the carrier of K

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 V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
FinOmega () is finite Element of Fin ()

(n,K,a) is Relation-like Permutations n -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(), the carrier of K:]
[:(), the carrier of K:] is non empty set
bool [:(), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the addF of K \$\$ ((),(n,K,a)) is Element of the carrier of K

the carrier of n is non empty non trivial set
K is Element of the carrier of n

1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = 1 } is set
[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,<*K*>] is set

(1,n,) is Element of the carrier of n
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
FinOmega () is finite Element of Fin ()

(1,n,) is Relation-like Permutations 1 -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 \$\$ ((),(1,n,)) is Element of the carrier of n
(1,n,) . () is set
len () is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len ()) is finite V50( len ()) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

len (Path_matrix (M,)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (M,)) is finite Element of bool NAT
M . 1 is set
(Path_matrix (M,)) . 1 is set
* (1,1) is Element of the carrier of n
(1,n,) . M is Element of the carrier of n
the multF 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 having_a_unity Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
the multF of n \$\$ (Path_matrix (M,)) is Element of the carrier of n

{K} is non empty trivial finite V50(1) set
[:(Seg 1),{K}:] is non empty finite set
bool [:(Seg 1),{K}:] is non empty cup-closed diff-closed preBoolean finite V47() set

0. n is V62(n) Element of the carrier of n
the carrier of n is non empty non trivial set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
0. (n,K,K) is Relation-like NAT -defined the carrier of n * -valued Function-like finite 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
(K,n,(0. (n,K,K))) is Element of the carrier of n
Permutations K is non empty permutational 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
FinOmega () is finite Element of Fin ()

(K,n,(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 \$\$ ((),(K,n,(0. (n,K,K)))) is Element of the carrier of n
[:(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:]
k 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:]
k . {} is set
c9 is Element of the carrier of n
the addF of n . ((0. n),c9) is Element of the carrier of n
dom (K,n,(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:]
c9 is set
(K,n,(0. (n,K,K))) . c9 is set
(() --> (0. n)) . c9 is set
len () is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len ()) is finite V50( len ()) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set
the multF 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 having_a_unity Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]

(() --> (0. n)) . x is Element of the carrier of n
Path_matrix (x,(0. (n,K,K))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n \$\$ (Path_matrix (x,(0. (n,K,K)))) is Element of the carrier of n
B is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
B + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(B + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like finite V50(B + 1) FinSequence-like FinSubsequence-like Element of (B + 1) -tuples_on the carrier of n
(B + 1) -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = B + 1 } is set
Seg (B + 1) is finite V50(B + 1) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= B + 1 ) } is set
(Seg (B + 1)) --> (0. n) is Relation-like Seg (B + 1) -defined {(0. n)} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (B + 1)),{(0. n)}:]
{(0. n)} is non empty trivial finite V50(1) set
[:(Seg (B + 1)),{(0. n)}:] is finite set
bool [:(Seg (B + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean finite V47() set
the multF of n \$\$ ((B + 1) |-> (0. n)) is Element of the carrier of n
(B + 1) + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
((B + 1) + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like finite V50((B + 1) + 1) FinSequence-like FinSubsequence-like Element of ((B + 1) + 1) -tuples_on the carrier of n
((B + 1) + 1) -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = (B + 1) + 1 } is set
Seg ((B + 1) + 1) is finite V50((B + 1) + 1) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= (B + 1) + 1 ) } is set
(Seg ((B + 1) + 1)) --> (0. n) is Relation-like Seg ((B + 1) + 1) -defined {(0. n)} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg ((B + 1) + 1)),{(0. n)}:]
[:(Seg ((B + 1) + 1)),{(0. n)}:] is finite set
bool [:(Seg ((B + 1) + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean finite V47() set
the multF of n \$\$ (((B + 1) + 1) |-> (0. n)) is Element of the carrier of n

1 -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = 1 } is set
[1,(0. n)] is set
{[1,(0. n)]} is Function-like non empty trivial finite V50(1) set
((B + 1) |-> (0. n)) ^ <*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite V50((B + 1) + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B + 1) + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(0. n) * (0. n) is Element of the carrier of n
the multF of n . ((0. n),(0. n)) is Element of the carrier of n

K -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = K } is set
Seg K is finite V50(K) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set

{(0. n)} is non empty trivial finite V50(1) set
[:(Seg K),{(0. n)}:] is finite set
bool [:(Seg K),{(0. n)}:] is non empty cup-closed diff-closed preBoolean finite V47() set
dom (K |-> (0. n)) is finite V50(K) Element of bool NAT
B is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
x . B is set
(K |-> (0. n)) . B is set
B is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
(0. (n,K,K)) * (B,B) is Element of the carrier of n
width (0. (n,K,K)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (width (0. (n,K,K))) is finite V50( width (0. (n,K,K))) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= width (0. (n,K,K)) ) } is set
dom (0. (n,K,K)) is finite Element of bool NAT
[B,B] is set
[:(dom (0. (n,K,K))),(Seg (width (0. (n,K,K)))):] is finite set
Indices (0. (n,K,K)) is set
len (K |-> (0. n)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
K -' 1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite V48() Element of NAT
(K -' 1) + 1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT

1 -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = 1 } is set

[:(Seg 1),{(0. n)}:] is non empty finite set
bool [:(Seg 1),{(0. n)}:] is non empty cup-closed diff-closed preBoolean finite V47() set

[1,(0. n)] is set
{[1,(0. n)]} is Function-like non empty trivial finite V50(1) set
0 + 1 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
(0 + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like finite V50(0 + 1) FinSequence-like FinSubsequence-like Element of (0 + 1) -tuples_on the carrier of n
(0 + 1) -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 finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = 0 + 1 } is set
Seg (0 + 1) is non empty finite V50(0 + 1) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= 0 + 1 ) } is set
(Seg (0 + 1)) --> (0. n) is Relation-like Seg (0 + 1) -defined {(0. n)} -valued Function-like non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg (0 + 1)),{(0. n)}:]
[:(Seg (0 + 1)),{(0. n)}:] is non empty finite set
bool [:(Seg (0 + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean finite V47() set
the multF of n \$\$ ((0 + 1) |-> (0. n)) is Element of the carrier of n
dom (() --> (0. n)) is set
len () is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len ()) is finite V50( len ()) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{c9} is functional non empty trivial finite V47() V50(1) set
k . {c9} is set
(K,n,(0. (n,K,K))) . c9 is Element of the carrier of n
{.c9.} is functional non empty trivial finite V47() V50(1) Element of Fin ()
k . {.c9.} is Element of the carrier of n
c9 is finite Element of Fin ()
() \ c9 is finite Element of Fin ()
k . c9 is Element of the carrier of n

{x} is functional non empty trivial finite V47() V50(1) set
c9 \/ {x} is non empty finite set
k . (c9 \/ {x}) is set
(K,n,(0. (n,K,K))) . x is Element of the carrier of n
the addF of n . ((k . c9),((K,n,(0. (n,K,K))) . x)) is Element of the carrier of n
{.x.} is functional non empty trivial finite V47() V50(1) Element of Fin ()
c9 \/ {.x.} is non empty finite Element of Fin ()
k . (c9 \/ {.x.}) is Element of the carrier of n
k . () is Element of the carrier of n

the carrier of n is non empty non trivial set
K is Element of the carrier of n
a is Element of the carrier of n
M is Element of the carrier of n
N is Element of the carrier of n
(K,a) ][ (M,N) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,N] is set
{[1,N]} is Function-like non empty trivial finite V50(1) set

Path_matrix (i,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (Path_matrix (i,((K,a) ][ (M,N)))) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (i,((K,a) ][ (M,N)))) is finite Element of bool NAT
i . 2 is set
(Path_matrix (i,((K,a) ][ (M,N)))) . 2 is set
((K,a) ][ (M,N)) * (2,2) is Element of the carrier of n
i . 1 is set
(Path_matrix (i,((K,a) ][ (M,N)))) . 1 is set
((K,a) ][ (M,N)) * (1,1) is Element of the carrier of n

the carrier of n is non empty non trivial set
K is Element of the carrier of n
a is Element of the carrier of n
M is Element of the carrier of n

[1,a] is set
{[1,a]} is Function-like non empty trivial finite V50(1) set

[1,M] is set
{[1,M]} is Function-like non empty trivial finite V50(1) set

N is Element of the carrier of n
(K,a) ][ (M,N) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

Path_matrix (i,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (Path_matrix (i,((K,a) ][ (M,N)))) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (i,((K,a) ][ (M,N)))) is finite Element of bool NAT
(Path_matrix (i,((K,a) ][ (M,N)))) . 1 is set
((K,a) ][ (M,N)) * (1,2) is Element of the carrier of n
(Path_matrix (i,((K,a) ][ (M,N)))) . 2 is set
((K,a) ][ (M,N)) * (2,1) is Element of the carrier of n

the carrier of n is non empty non trivial set
the multF 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 having_a_unity 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
K is Element of the carrier of n
a is Element of the carrier of n

[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,a] is set
{[1,a]} is Function-like non empty trivial finite V50(1) set

the multF of n \$\$ <*K,a*> is Element of the carrier of n
K * a is Element of the carrier of n
the multF of n . (K,a) is Element of the carrier of n
Product <*K,a*> is Element of the carrier of n

len K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len K) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product K is Element of the carrier of ()

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set

len K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len K) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product K is Element of the carrier of ()

the carrier of n is non empty non trivial set
K is Element of the carrier of n
a is Element of the carrier of n
M is Element of the carrier of n
a * M is Element of the carrier of n
the multF 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 having_a_unity 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
the multF of n . (a,M) is Element of the carrier of n
N is Element of the carrier of n
(K,a) ][ (M,N) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Det ((K,a) ][ (M,N)) is Element of the carrier of n
K * N is Element of the carrier of n
the multF of n . (K,N) is Element of the carrier of n
(K * N) - (a * M) is Element of the carrier of n
- (a * M) is Element of the carrier of n
(K * N) + (- (a * M)) is Element of the carrier of n
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 addF of n . ((K * N),(- (a * M))) is Element of the carrier of n
Path_product ((K,a) ][ (M,N)) is Relation-like Permutations 2 -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

(Path_product ((K,a) ][ (M,N))) . i is Element of the carrier of n
Path_matrix (i,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n \$\$ (Path_matrix (i,((K,a) ][ (M,N)))) is Element of the carrier of n
- (( the multF of n \$\$ (Path_matrix (i,((K,a) ][ (M,N))))),i) is Element of the carrier of n
- ( the multF of n \$\$ (Path_matrix (i,((K,a) ][ (M,N))))) is Element of the carrier of n

[1,a] is set
{[1,a]} is Function-like non empty trivial finite V50(1) set

[1,M] is set
{[1,M]} is Function-like non empty trivial finite V50(1) set

the multF of n \$\$ <*a,M*> is Element of the carrier of n
- ( the multF of n \$\$ <*a,M*>) is Element of the carrier of n

(Path_product ((K,a) ][ (M,N))) . k is set
Path_matrix (c9,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n \$\$ (Path_matrix (c9,((K,a) ][ (M,N)))) is Element of the carrier of n
- (( the multF of n \$\$ (Path_matrix (c9,((K,a) ][ (M,N))))),c9) is Element of the carrier of n

[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,N] is set
{[1,N]} is Function-like non empty trivial finite V50(1) set

the multF of n \$\$ <*K,N*> is Element of the carrier of n
FinOmega () is finite Element of Fin ()

{.c9,i.} is functional non empty finite V47() Element of Fin ()
the addF of n \$\$ ({.c9,i.},(Path_product ((K,a) ][ (M,N)))) is Element of the carrier of n

the carrier of n is non empty non trivial set
K is Element of the carrier of n
a is Element of the carrier of n
M is Element of the carrier of n
a * M is Element of the carrier of n
the multF 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 having_a_unity 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
the multF of n . (a,M) is Element of the carrier of n
N is Element of the carrier of n
(K,a) ][ (M,N) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
(2,n,((K,a) ][ (M,N))) is Element of the carrier of n
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:]
FinOmega () is finite Element of Fin ()

(2,n,((K,a) ][ (M,N))) is Relation-like Permutations 2 -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 \$\$ ((),(2,n,((K,a) ][ (M,N)))) is Element of the carrier of n
K * N is Element of the carrier of n
the multF of n . (K,N) is Element of the carrier of n
(K * N) + (a * M) is Element of the carrier of n
the addF of n . ((K * N),(a * M)) is Element of the carrier of n

(2,n,((K,a) ][ (M,N))) . i is Element of the carrier of n
Path_matrix (i,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n \$\$ (Path_matrix (i,((K,a) ][ (M,N)))) is Element of the carrier of n

[1,a] is set
{[1,a]} is Function-like non empty trivial finite V50(1) set

[1,M] is set
{[1,M]} is Function-like non empty trivial finite V50(1) set

the multF of n \$\$ <*a,M*> is Element of the carrier of n
(2,n,((K,a) ][ (M,N))) . c9 is set
Path_matrix (k,((K,a) ][ (M,N))) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n \$\$ (Path_matrix (k,((K,a) ][ (M,N)))) is Element of the carrier of n

[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,N] is set
{[1,N]} is Function-like non empty trivial finite V50(1) set

the multF of n \$\$ <*K,N*> is Element of the carrier of n

{ } is set

n is non empty set
K is Element of n
a is Element of n
M is Element of n

[1,K] is set
{[1,K]} is Function-like non empty trivial finite V50(1) set

[1,a] is set
{[1,a]} is Function-like non empty trivial finite V50(1) set

[1,M] is set
{[1,M]} is Function-like non empty trivial finite V50(1) set

{ } is set

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set

rng a is finite set
rng (Rev a) is finite set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set
dom (K ^ a) is finite Element of bool NAT
len K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len K) + (len a) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg ((len K) + (len a)) is finite V50((len K) + (len a)) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= (len K) + (len a) ) } is set
len (Rev a) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (K ^ (Rev a)) is finite Element of bool NAT
rng (K ^ a) is finite set
rng K is finite set
(rng K) \/ (rng a) is finite set
rng (K ^ (Rev a)) is finite set

n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational set

len (K ^ a) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len (K ^ a)) is finite V50( len (K ^ a)) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (K ^ a) ) } is set
dom (K ^ a) is finite Element of bool NAT
len K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len K) + (len a) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len (a ^ K) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (a ^ K) is finite Element of bool NAT
rng (K ^ a) is finite set
rng K is finite set
rng a is finite set
(rng K) \/ (rng a) is finite set
rng (a ^ K) is finite set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set

Permutations 3 is non empty permutational set

{<*1,2,3*>,<*3,2,1*>,<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} is non empty finite set

{ } is set