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
{ 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
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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= 3 ) } is set
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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations 2) ) } is set
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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is 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):]
[:(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
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 Relation-like Seg (len (Permutations F1())) -defined Seg (len (Permutations F1())) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations F1()
{a} is functional non empty trivial finite V47() V50(1) set
M is non empty finite Element of Fin (Permutations F1())
a is Relation-like Seg (len (Permutations F1())) -defined Seg (len (Permutations F1())) -valued Function-like one-to-one total quasi_total onto bijective finite Element of 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 Relation-like Seg (len (Permutations F1())) -defined Seg (len (Permutations F1())) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations F1()
{a} is functional non empty trivial finite V47() V50(1) set
K \/ {a} is non empty set
a is Relation-like Seg (len (Permutations F1())) -defined Seg (len (Permutations F1())) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations F1()
<*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
{ 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
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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is 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):]
[:(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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is 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):]
[:(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
{ 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 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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations n) ) } is 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
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
{ 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
<*<*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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations 1) ) } is set
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
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
(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:]
c9 is set
(K,n,(0. (n,K,K))) . c9 is set
((Permutations K) --> (0. n)) . c9 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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations K) ) } 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:]
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
{ 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
<*(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
{ 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 |-> (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
{ 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
(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
{ 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 |-> (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
{ 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 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
{ 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 ((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
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= len (Permutations K) ) } is set
c9 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
{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 (Permutations K)
k . {.c9.} is Element of the carrier of n
c9 is finite Element of Fin (Permutations K)
(FinOmega (Permutations K)) \ c9 is finite Element of Fin (Permutations K)
k . c9 is Element of 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
{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 (Permutations K)
c9 \/ {.x.} is non empty finite Element of Fin (Permutations K)
k . (c9 \/ {.x.}) is Element of the carrier of n
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
{ 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
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
c9 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
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 (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
<*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
{.c9,i.} is functional non empty finite V47() Element of Fin (Permutations 2)
the addF of n $$ ({.c9,i.},(Path_product ((K,a) ][ (M,N)))) 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 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
c9 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):]
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))) . 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
<*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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 1 } is set
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
{ b1 where b1 is Relation-like NAT -defined n -valued Function-like finite FinSequence-like FinSubsequence-like Element of n * : len b1 = 1 } is set
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
{ 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 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
{ 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
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
{ b1 where b1 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of NAT * : len b1 = 1 } is set
K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT