:: MATRIX_9 semantic presentation

REAL is set

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

bool REAL is non empty cup-closed diff-closed preBoolean set

{} 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

COMPLEX is set

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

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

Fin NAT is non empty cup-closed diff-closed preBoolean 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

{ b

{1} is non empty trivial finite V47() V50(1) set

Seg 2 is non empty finite V50(2) Element of bool NAT

{ b

{1,2} is non empty finite V47() set

idseq 2 is Relation-like NAT -defined Function-like finite V50(2) FinSequence-like FinSubsequence-like set

id (Seg 2) is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg 2),(Seg 2):]

[:(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,2*> is Relation-like NAT -defined Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like set

<*1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,1] is set

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

<*2*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,2] is set

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

<*1*> ^ <*2*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

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

idseq 3 is Relation-like NAT -defined Function-like finite V50(3) FinSequence-like FinSubsequence-like set

Seg 3 is non empty finite V50(3) Element of bool NAT

{ b

id (Seg 3) is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg 3),(Seg 3):]

[:(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,2,3*> is Relation-like NAT -defined Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like set

<*3*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,3] is set

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

(<*1*> ^ <*2*>) ^ <*3*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like 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

idseq 1 is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

id (Seg 1) is Relation-like Seg 1 -defined Seg 1 -valued Function-like one-to-one non empty total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg 1),(Seg 1):]

[:(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

{(idseq 1)} 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

<*2,1*> is Relation-like NAT -defined Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like set

<*2*> ^ <*1*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

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

Group_of_Perm 2 is non empty strict unital Group-like associative multMagma

the carrier of (Group_of_Perm 2) is non empty set

len (Permutations 2) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

Seg (len (Permutations 2)) is finite V50( len (Permutations 2)) Element of bool NAT

{ b

n is set

K is set

{n} is non empty trivial finite V50(1) set

Fin K is non empty cup-closed diff-closed preBoolean set

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

Permutations n is non empty permutational set

Fin (Permutations n) is non empty cup-closed diff-closed preBoolean set

idseq n is Relation-like NAT -defined Function-like finite V50(n) FinSequence-like FinSubsequence-like set

Seg n is finite V50(n) Element of bool NAT

{ b

id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is finite set

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

{(idseq n)} is functional non empty trivial finite V47() V50(1) set

F

Permutations F

Fin (Permutations F

len (Permutations F

Seg (len (Permutations F

{ b

F

n is set

K is set

{n} is non empty trivial finite V50(1) set

K \/ {n} is non empty set

a is Relation-like Seg (len (Permutations F

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

M is non empty finite Element of Fin (Permutations F

a is Relation-like Seg (len (Permutations F

M is non empty finite Element of Fin (Permutations F

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

M \/ {a} is non empty finite set

a is Relation-like Seg (len (Permutations F

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

K \/ {a} is non empty set

a is Relation-like Seg (len (Permutations F

<*1,2*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of NAT

<*2,1*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of NAT

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

Seg n is finite V50(n) Element of bool NAT

{ b

[:(Seg n),(Seg n):] is finite set

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

id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

K is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

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

{ b

id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

[:(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 (idseq 2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

(Rev (idseq 2)) . 1 is set

(Rev (idseq 2)) . 2 is set

n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 2),(Seg 2):]

n . 1 is set

Rev n is Relation-like NAT -defined Function-like one-to-one non empty finite FinSequence-like FinSubsequence-like 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

(idseq 2) . 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 finite Element of bool NAT

Rev (id (Seg 2)) is Relation-like NAT -defined Function-like one-to-one non empty finite FinSequence-like FinSubsequence-like set

n is Relation-like Function-like one-to-one set

dom n is set

rng n is set

dom (idseq 2) 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

idseq n is Relation-like NAT -defined Function-like finite V50(n) FinSequence-like FinSubsequence-like set

Seg n is finite V50(n) Element of bool NAT

{ b

id (Seg n) is Relation-like NAT -defined Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite FinSequence-like FinSubsequence-like V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

[:(Seg n),(Seg n):] is finite set

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

Rev (idseq n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Permutations n is non empty permutational set

K is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),(Seg n):]

dom K is finite Element of bool NAT

Rev K is Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like set

dom (Rev K) is finite Element of bool NAT

rng (idseq n) is finite set

rng (Rev K) is finite set

rng K is finite set

a is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),(Seg n):]

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

Permutations n is non empty permutational set

K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Rev K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Seg n is finite V50(n) Element of bool NAT

{ b

[:(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 Element of bool NAT

dom (Rev K) is finite Element of bool NAT

rng K is finite set

rng (Rev K) is finite set

a is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),(Seg n):]

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

n is set

K is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 2),(Seg 2):]

rng K is finite set

dom K is finite set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

n is set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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

[:(Permutations n), the carrier of K:] is non empty set

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

len (Permutations n) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

Seg (len (Permutations n)) is finite V50( len (Permutations n)) Element of bool NAT

{ b

a is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K

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 [:(Permutations n), the carrier of K:]

N is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations n

M . N is Element of the carrier of K

Path_matrix (N,a) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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 [:(Permutations n), 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 [:(Permutations n), the carrier of K:]

i is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations n

M . i is Element of the carrier of K

Path_matrix (i,a) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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

K is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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 (Permutations n) is finite Element of Fin (Permutations n)

Fin (Permutations n) is non empty cup-closed diff-closed preBoolean set

a is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K

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

[:(Permutations n), the carrier of K:] is non empty set

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

the addF of K $$ ((FinOmega (Permutations n)),(n,K,a)) is Element of the carrier of K

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

the carrier of n is non empty non trivial set

K is Element of the carrier of n

<*K*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on 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

{ b

[1,K] is set

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

<*<*K*>*> is Relation-like NAT -defined the carrier of n * -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like tabular Matrix of 1,1, the carrier of n

[1,<*K*>] is set

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

(1,n,<*<*K*>*>) 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 (Permutations 1) is finite Element of Fin (Permutations 1)

Fin (Permutations 1) is non empty cup-closed diff-closed preBoolean set

(1,n,<*<*K*>*>) is Relation-like Permutations 1 -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations 1), the carrier of n:]

[:(Permutations 1), the carrier of n:] is non empty set

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

the addF of n $$ ((FinOmega (Permutations 1)),(1,n,<*<*K*>*>)) is Element of the carrier of n

(1,n,<*<*K*>*>) . (idseq 1) is set

len (Permutations 1) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

Seg (len (Permutations 1)) is finite V50( len (Permutations 1)) Element of bool NAT

{ b

M is Relation-like Seg (len (Permutations 1)) -defined Seg (len (Permutations 1)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 1

Path_matrix (M,<*<*K*>*>) 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 (M,<*<*K*>*>)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

dom (Path_matrix (M,<*<*K*>*>)) is finite Element of bool NAT

M . 1 is set

(Path_matrix (M,<*<*K*>*>)) . 1 is set

<*<*K*>*> * (1,1) is Element of the carrier of n

(1,n,<*<*K*>*>) . 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,<*<*K*>*>)) is Element of the carrier of n

1 |-> K is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

(Seg 1) --> K is Relation-like Seg 1 -defined {K} -valued Function-like non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{K}:]

{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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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 (Permutations K) is finite Element of Fin (Permutations K)

Fin (Permutations K) is non empty cup-closed diff-closed preBoolean set

(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 [:(Permutations K), the carrier of n:]

[:(Permutations K), the carrier of n:] is non empty set

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

the addF of n $$ ((FinOmega (Permutations K)),(K,n,(0. (n,K,K)))) is Element of the carrier of n

[:(Fin (Permutations K)), the carrier of n:] is non empty set

bool [:(Fin (Permutations K)), the carrier of n:] is non empty cup-closed diff-closed preBoolean set

(Fin (Permutations K)) --> (0. n) is Relation-like Fin (Permutations K) -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Fin (Permutations K)), the carrier of n:]

k is Relation-like Fin (Permutations K) -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Fin (Permutations K)), the carrier of n:]

k . {} is set

c

the addF of n . ((0. n),c

dom (K,n,(0. (n,K,K))) is set

(Permutations K) --> (0. n) is Relation-like Permutations K -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations K), the carrier of n:]

c

(K,n,(0. (n,K,K))) . c

((Permutations K) --> (0. n)) . c

len (Permutations K) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

Seg (len (Permutations K)) is finite V50( len (Permutations K)) Element of bool NAT

{ b

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:]

x is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations K

((Permutations K) --> (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

{ b

Seg (B + 1) is finite V50(B + 1) Element of bool NAT

{ b

(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

{ b

Seg ((B + 1) + 1) is finite V50((B + 1) + 1) Element of bool NAT

{ b

(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

<*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

[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 |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like finite V50(K) FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n

K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

Seg K is finite V50(K) Element of bool NAT

{ b

(Seg K) --> (0. n) is Relation-like Seg K -defined {(0. n)} -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(0. n)}:]

{(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

{ b

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 |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n

{ b

(Seg 1) --> (0. n) is Relation-like Seg 1 -defined {(0. n)} -valued Function-like non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{(0. n)}:]

[:(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

<*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n

[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

{ b

Seg (0 + 1) is non empty finite V50(0 + 1) Element of bool NAT

{ b

(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 ((Permutations K) --> (0. n)) is set

len (Permutations K) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT

Seg (len (Permutations K)) is finite V50( len (Permutations K)) Element of bool NAT

{ b

c

{c

k . {c

(K,n,(0. (n,K,K))) . c

{.c

k . {.c

c

(FinOmega (Permutations K)) \ c

k . c

x is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations K

{x} is functional non empty trivial finite V47() V50(1) set

c

k . (c

(K,n,(0. (n,K,K))) . x is Element of the carrier of n

the addF of n . ((k . c

{.x.} is functional non empty trivial finite V47() V50(1) Element of Fin (Permutations K)

c

k . (c

k . (FinOmega (Permutations K)) is Element of the carrier of n

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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

<*K,N*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*K*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,K] is set

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

<*N*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,N] is set

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

<*K*> ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

i is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 2

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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 Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,a] is set

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

<*M*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,M] is set

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

<*a*> ^ <*M*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like 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

i is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 2

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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

<*K,a*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*K*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,K] is set

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

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,a] is set

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

<*K*> ^ <*a*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like 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

n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 2),(Seg 2):]

K is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)

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 (Group_of_Perm 2)

dom K 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

{ b

[:(Seg n),(Seg n):] is finite set

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

id (Seg n) is Relation-like NAT -defined Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite FinSequence-like FinSubsequence-like V115() V117() V118() V122() Element of bool [:(Seg n),(Seg n):]

K is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg n),(Seg n):]

n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 2),(Seg 2):]

K is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)

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 (Group_of_Perm 2)

dom K is finite Element of bool NAT

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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 [:(Permutations 2), the carrier of n:]

[:(Permutations 2), the carrier of n:] is non empty set

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

i is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 2

(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

<*a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,a] is set

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

<*M*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,M] is set

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

<*a*> ^ <*M*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like 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

c

k is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 2),(Seg 2):]

(Path_product ((K,a) ][ (M,N))) . k is set

Path_matrix (c

the multF of n $$ (Path_matrix (c

- (( the multF of n $$ (Path_matrix (c

<*K,N*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*K*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,K] is set

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

<*N*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,N] is set

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

<*K*> ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

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

FinOmega (Permutations 2) is finite Element of Fin (Permutations 2)

Fin (Permutations 2) is non empty cup-closed diff-closed preBoolean set

{.c

the addF of n $$ ({.c

n is non empty non degenerated non trivial right_complementable almost_left_invertible V105() unital associative commutative V158() V159() V160() right-distributive left-distributive right_unital well-unital V172() left_unital doubleLoopStr

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 (Permutations 2) is finite Element of Fin (Permutations 2)

Fin (Permutations 2) is non empty cup-closed diff-closed preBoolean set

(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 [:(Permutations 2), the carrier of n:]

[:(Permutations 2), the carrier of n:] is non empty set

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

the addF of n $$ ((FinOmega (Permutations 2)),(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

k is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 2

c

i is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 2

(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

<*a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,a] is set

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

<*M*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,M] is set

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

<*a*> ^ <*M*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

the multF of n $$ <*a,M*> is Element of the carrier of n

(2,n,((K,a) ][ (M,N))) . c

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

<*K,N*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*K*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,K] is set

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

<*N*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,N] is set

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

<*K*> ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

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

Rev (idseq 3) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

<*3,2,1*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*3*> ^ <*2*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

(<*3*> ^ <*2*>) ^ <*1*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

<*2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of NAT

<*2*> ^ <*3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

<*1*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on NAT

1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*1*> ^ n is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*1,2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

Rev n is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT

<*3,2*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of NAT

n is non empty set

K is Element of n

a is Element of n

M is Element of n

<*K,a,M*> is Relation-like NAT -defined n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of n

<*K*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,K] is set

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

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,a] is set

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

<*K*> ^ <*a*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

<*M*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set

[1,M] is set

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

(<*K*> ^ <*a*>) ^ <*M*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

<*M,a,K*> is Relation-like NAT -defined n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of n

<*M*> ^ <*a*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

(<*M*> ^ <*a*>) ^ <*K*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

N is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

Rev N is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

<*a,M*> is Relation-like NAT -defined n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of n

<*a*> ^ <*M*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

<*K*> is Relation-like NAT -defined n -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on n

1 -tuples_on n is functional non empty FinSequence-membered FinSequenceSet of n

n * is functional non empty FinSequence-membered FinSequenceSet of n

{ b

i is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

<*K*> ^ i is Relation-like NAT -defined n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of n

Rev i is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of n

<*M,a*> is Relation-like NAT -defined n -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of n

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

Permutations n is non empty permutational set

K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

K ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

Rev a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

K ^ (Rev a) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng a is finite set

rng (Rev a) is finite set

Seg n is finite V50(n) Element of bool NAT

{ b

[:(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

{ b

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 Relation-like Seg n -defined Seg n -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),(Seg n):]

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

Permutations n is non empty permutational set

K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

K ^ a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

a ^ K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like 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

{ b

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

{ b

[:(Seg n),(Seg n):] is finite set

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

M is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg n),(Seg n):]

Permutations 3 is non empty permutational set

<*1,2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*1,3,2*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*1*> ^ <*3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

(<*1*> ^ <*3*>) ^ <*2*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

<*2,3,1*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*2*> ^ <*3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

(<*2*> ^ <*3*>) ^ <*1*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

<*2,1,3*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

(<*2*> ^ <*1*>) ^ <*3*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

<*3,1,2*> is Relation-like NAT -defined NAT -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of NAT

<*3*> ^ <*1*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set

(<*3*> ^ <*1*>) ^ <*2*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set

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

<*3*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on NAT

1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT

NAT * is functional non empty FinSequence-membered FinSequenceSet of NAT

{ b

K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT