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
<*3*> ^ K is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*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
a is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 3),(Seg 3):]
<*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
K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ K is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*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
K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
Rev K 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
a is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 3),(Seg 3):]
<*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
<*1*> ^ K is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*1*> ^ (Rev K) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*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
<*3*> ^ K is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
Rev K is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ (Rev K) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
n is set
{<*1,2,3*>,<*3,2,1*>} is functional non empty finite V47() set
{<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} is non empty finite set
{<*1,2,3*>,<*3,2,1*>} \/ {<*1,3,2*>,<*2,3,1*>,<*2,1,3*>,<*3,1,2*>} is non empty finite set
{<*1,3,2*>,<*2,3,1*>} is functional non empty finite V47() set
{<*2,1,3*>,<*3,1,2*>} is functional non empty finite V47() set
{<*1,3,2*>,<*2,3,1*>} \/ {<*2,1,3*>,<*3,1,2*>} is non empty finite V47() set
n is set
K is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
rng K is finite set
K . 3 is set
K . 2 is set
dom K is finite set
K . 1 is set
a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len (Permutations 3) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len (Permutations 3)) is finite V50( len (Permutations 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 <= len (Permutations 3) ) } is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*K,i,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*K*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*K*> ^ <*i*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,1) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 1 is set
[3,3] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,3) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 3 is set
[2,2] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,2) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 2 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*M,i,k*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*M*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*M*> ^ <*i*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,3) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 3 is set
[3,1] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,1) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 1 is set
[2,2] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,2) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 2 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*K,p,c9*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*K*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*K*> ^ <*p*>) ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,1) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 1 is set
[3,2] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,2) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 2 is set
[2,3] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,3) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 3 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*a,p,k*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*a*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*a*> ^ <*p*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,2) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 2 is set
[3,1] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,1) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 1 is set
[2,3] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,3) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 3 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*a,N,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*a*> ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*a*> ^ <*N*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,2) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 2 is set
[3,3] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,3) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 3 is set
[2,1] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,1) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 1 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite 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
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
N is Element of the carrier of n
i is Element of the carrier of n
p is Element of the carrier of n
<*N,i,p*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*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
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
(<*N*> ^ <*i*>) ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
k is Element of the carrier of n
c9 is Element of the carrier of n
x is Element of the carrier of n
<*k,c9,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*k*> ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
(<*k*> ^ <*c9*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*K,a,M*>,<*N,i,p*>,<*k,c9,x*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*K,a,M*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*K,a,M*>] is set
{[1,<*K,a,M*>]} is Function-like non empty trivial finite V50(1) set
<*<*N,i,p*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*N,i,p*>] is set
{[1,<*N,i,p*>]} is Function-like non empty trivial finite V50(1) set
<*<*K,a,M*>*> ^ <*<*N,i,p*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*k,c9,x*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*k,c9,x*>] is set
{[1,<*k,c9,x*>]} is Function-like non empty trivial finite V50(1) set
(<*<*K,a,M*>*> ^ <*<*N,i,p*>*>) ^ <*<*k,c9,x*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*M,N,c9*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*M*> ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*M*> ^ <*N*>) ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Indices B is set
B . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (1,3) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B . 3 is set
[3,2] is set
B . 3 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (3,2) is Element of the carrier of n
a3 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a3 . 2 is set
[2,1] is set
B . 2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B * (2,1) is Element of the carrier of n
a4 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a4 . 1 is set
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
Path_matrix (a5,B) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
a5 . 1 is set
a5 . 3 is set
a5 . 2 is set
len (Path_matrix (a5,B)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a5,B)) is finite Element of bool NAT
(Path_matrix (a5,B)) . 2 is set
(Path_matrix (a5,B)) . 3 is set
(Path_matrix (a5,B)) . 1 is 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
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 Element of the carrier of n
the multF of n . (K,a) is Element of the carrier of n
M is Element of the carrier of n
<*K,a,M*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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
<*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
the multF of n $$ <*K,a,M*> is Element of the carrier of n
(K * a) * M is Element of the carrier of n
the multF of n . ((K * a),M) is Element of the carrier of n
Product <*K,a,M*> is Element of the carrier of n
<*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
<*3*> ^ <*1,2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V50(1 + 2) FinSequence-like FinSubsequence-like FinSequence of NAT
1 + 2 is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
<*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
Rev <*2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty 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
<*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*> ^ (Rev <*2,3*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
K is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 3),(Seg 3):]
<*1*> ^ <*2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V50(1 + 2) FinSequence-like FinSubsequence-like FinSequence of NAT
Rev <*1,2*> is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
<*3*> ^ (Rev <*1,2*>) is Relation-like NAT -defined NAT -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of NAT
K is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total finite FinSequence-like FinSubsequence-like Element of bool [:(Seg 3),(Seg 3):]
<*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
<*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
<*1*> ^ <*2,3*> is Relation-like NAT -defined NAT -valued Function-like non empty finite V50(1 + 2) FinSequence-like FinSubsequence-like FinSequence of NAT
<*2,3,1*> " is Relation-like Function-like set
rng <*2,3,1*> is finite set
{2,3,1} is non empty finite set
dom <*2,3,1*> is non trivial finite V50(3) Element of bool NAT
dom <*3,1,2*> is non trivial finite V50(3) Element of bool NAT
<*3,1,2*> * <*2,3,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is non empty non trivial non finite set
bool [:NAT,NAT:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
dom (<*3,1,2*> * <*2,3,1*>) is finite set
id {1,2,3} is Relation-like {1,2,3} -defined {1,2,3} -valued Function-like one-to-one non empty total quasi_total onto bijective finite V115() V117() V118() V122() Element of bool [:{1,2,3},{1,2,3}:]
[:{1,2,3},{1,2,3}:] is non empty finite set
bool [:{1,2,3},{1,2,3}:] is non empty cup-closed diff-closed preBoolean finite V47() set
a is set
(<*3,1,2*> * <*2,3,1*>) . a is set
(id {1,2,3}) . a is set
<*2,3,1*> . a is set
<*3,1,2*> . (<*2,3,1*> . a) is set
<*3,1,2*> . 2 is set
<*2,3,1*> . a is set
<*3,1,2*> . (<*2,3,1*> . a) is set
<*3,1,2*> . 3 is set
<*2,3,1*> . a is set
<*3,1,2*> . (<*2,3,1*> . a) is set
<*3,1,2*> . 1 is set
dom (id {1,2,3}) is finite set
Group_of_Perm 3 is non empty strict unital Group-like associative multMagma
the carrier of (Group_of_Perm 3) is non empty set
n is Element of the carrier of (Group_of_Perm 3)
n " is Element of the carrier of (Group_of_Perm 3)
K is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
K " is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):]
[:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is finite set
bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is non empty cup-closed diff-closed preBoolean finite V47() set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
dom n is finite set
K is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . K is set
a is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . a is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . K is set
n . a is set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
dom n is finite set
K is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . K is set
a is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . a is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . K is set
n . a is set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
dom n is finite set
K is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . K is set
a is non empty V29() V30() V31() V35() V36() ext-real positive non negative V40() finite V48() Element of NAT
n . a is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . K is set
n . a is set
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set
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):]
dom K is finite set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
K . a is set
K . M is set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
dom n is finite set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . K is set
n . a is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
dom n is finite set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . K is set
n . a is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
n . M is set
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Seg n is finite V50(n) Element of bool NAT
{ b1 where b1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V47() set
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):]
rng K is finite set
dom K is finite set
<*2,1,3*> * <*1,3,2*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
[:NAT,NAT:] is non empty non trivial non finite set
bool [:NAT,NAT:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
<*1,3,2*> * <*2,1,3*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*2,1,3*> * <*3,2,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*3,2,1*> * <*2,1,3*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*3,2,1*> * <*3,2,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*2,1,3*> * <*2,1,3*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*1,3,2*> * <*1,3,2*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*1,3,2*> * <*2,3,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*2,3,1*> * <*2,3,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*2,3,1*> * <*3,1,2*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*3,1,2*> * <*2,3,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*3,1,2*> * <*3,1,2*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*1,3,2*> * <*3,2,1*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
<*3,2,1*> * <*1,3,2*> is Relation-like NAT -defined NAT -valued Function-like finite Element of bool [:NAT,NAT:]
dom <*1,3,2*> is non trivial finite V50(3) Element of bool NAT
dom <*3,1,2*> is non trivial finite V50(3) Element of bool NAT
dom <*2,1,3*> is non trivial finite V50(3) Element of bool NAT
dom <*3,2,1*> is non trivial finite V50(3) Element of bool NAT
dom <*2,3,1*> is non trivial finite V50(3) Element of bool NAT
p is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
len p is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
i is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
p * i is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
[:NAT,(Seg 3):] is non empty non trivial non finite set
bool [:NAT,(Seg 3):] is non empty non trivial cup-closed diff-closed preBoolean non finite set
B is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
B . 1 is set
i . 1 is set
p . (i . 1) is set
p . 1 is set
p * p is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
B is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
B . 1 is set
p . (p . 1) is set
p . 2 is set
len i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
i * p is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
a3 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
a3 . 2 is set
i . (p . 2) is set
B . 3 is set
i . 3 is set
p . (i . 3) is set
B . 2 is set
i . 2 is set
p . (i . 2) is set
p . 3 is set
i * i is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
len B is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a3 . 1 is set
i . (p . 1) is set
a3 . 3 is set
i . (p . 3) is set
len a3 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a4 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
a4 . 2 is set
i . (i . 2) is set
B . 3 is set
p . (p . 3) is set
B . 2 is set
p . (p . 2) is set
k is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
p * k is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
a5 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
a5 . 1 is set
k . 1 is set
p . (k . 1) is set
a5 . 3 is set
k . 3 is set
p . (k . 3) is set
a5 . 2 is set
k . 2 is set
p . (k . 2) is set
len k is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
k * i is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
k * k is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
id3 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
id3 . 1 is set
k . (k . 1) is set
i * k is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
Id3 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
Id3 . 1 is set
i . (k . 1) is set
Id3 . 3 is set
i . (k . 3) is set
c9 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
i * c9 is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
B1 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
B1 . 1 is set
c9 . 1 is set
i . (c9 . 1) is set
B1 . 2 is set
c9 . 2 is set
i . (c9 . 2) is set
k * p is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
B2 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
B2 . 1 is set
k . (p . 1) is set
B2 . 2 is set
k . (p . 2) is set
id3 . 3 is set
k . (k . 3) is set
id3 . 2 is set
k . (k . 2) is set
len a5 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a4 . 3 is set
i . (i . 3) is set
B2 . 3 is set
k . (p . 3) is set
len B2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len id3 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len B is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a4 . 1 is set
i . (i . 1) is set
B1 . 3 is set
c9 . 3 is set
i . (c9 . 3) is set
len a4 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len B1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Id3 . 2 is set
i . (k . 2) is set
len c9 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
c9 * c9 is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
x is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
c9 * x is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
F is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
F . 1 is set
x . 1 is set
c9 . (x . 1) is set
F . 2 is set
x . 2 is set
c9 . (x . 2) is set
r is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
r . 3 is set
c9 . (c9 . 3) is set
F . 3 is set
x . 3 is set
c9 . (x . 3) is set
r . 2 is set
c9 . (c9 . 2) is set
r . 1 is set
c9 . (c9 . 1) is set
len x is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
x * c9 is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
x * x is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
r2 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
r2 . 1 is set
x . (x . 1) is set
r2 . 2 is set
x . (x . 2) is set
r1 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
r1 . 3 is set
x . (c9 . 3) is set
r2 . 3 is set
x . (x . 3) is set
r1 . 2 is set
x . (c9 . 2) is set
r1 . 1 is set
x . (c9 . 1) is set
len r is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len F is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a6 is Relation-like NAT -defined Seg 3 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of Seg 3
a6 . 3 is set
k . (i . 3) is set
len r1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len r2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a6 . 2 is set
k . (i . 2) is set
len Id3 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a6 . 1 is set
k . (i . 1) is set
len a6 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational 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 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
K 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
K * a is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):]
[:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is finite set
bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is non empty cup-closed diff-closed preBoolean finite V47() 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
N 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):]
M 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):]
M * N 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 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
a is Element of the carrier of (Group_of_Perm 3)
K is Element of the carrier of (Group_of_Perm 3)
<*a,K*> is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
<*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*> 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*> ^ <*K*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
M is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product M is Element of the carrier of (Group_of_Perm 3)
dom M is finite Element of bool NAT
2 * 1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite V48() Element of NAT
a * K is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) is Relation-like [: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty total quasi_total associative having_a_unity V156( the carrier of (Group_of_Perm 3)) Element of bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):]
[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] is non empty set
[:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty set
bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 3) . (a,K) is Element of the carrier of (Group_of_Perm 3)
N is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
i is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
i * N is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):]
[:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is finite set
bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is non empty cup-closed diff-closed preBoolean finite V47() set
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . p is set
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . p is set
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
K is Element of the carrier of (Group_of_Perm 3)
a is Element of the carrier of (Group_of_Perm 3)
<*K,a*> is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty non trivial finite V50(2) FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
<*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 the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product M is Element of the carrier of (Group_of_Perm 3)
dom M is finite Element of bool NAT
2 * 1 is V29() V30() V31() V35() V36() ext-real non negative V40() finite V48() Element of NAT
K * a is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) is Relation-like [: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty total quasi_total associative having_a_unity V156( the carrier of (Group_of_Perm 3)) Element of bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):]
[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] is non empty set
[:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty set
bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 3) . (K,a) is Element of the carrier of (Group_of_Perm 3)
i is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
N is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
N * i is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):]
[:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is finite set
bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is non empty cup-closed diff-closed preBoolean finite V47() set
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . p is set
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . p is set
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Group_of_Perm n is non empty strict unital Group-like associative multMagma
the carrier of (Group_of_Perm n) is non empty set
Permutations n is non empty permutational 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
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
K is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len K) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom K is finite Element of bool NAT
Product K is Element of the carrier of (Group_of_Perm n)
a 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):]
M is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product M is Element of the carrier of (Group_of_Perm n)
dom M is finite Element of bool NAT
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . N is set
M is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Product M is Element of the carrier of (Group_of_Perm n)
dom M is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
n * <*1,2,3*> is Relation-like NAT -defined Seg 3 -valued Function-like finite Element of bool [:NAT,(Seg 3):]
[:NAT,(Seg 3):] is non empty non trivial non finite set
bool [:NAT,(Seg 3):] is non empty non trivial cup-closed diff-closed preBoolean non finite set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
<*1,2,3*> * n is Relation-like Seg 3 -defined NAT -valued Function-like finite Element of bool [:(Seg 3),NAT:]
[:(Seg 3),NAT:] is non empty non trivial non finite set
bool [:(Seg 3),NAT:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
n is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len n is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len n) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom n is finite Element of bool NAT
Product n is Element of the carrier of (Group_of_Perm 3)
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
2 * K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
K + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
2 * (K + 1) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom a is finite Element of bool NAT
Product a is Element of the carrier of (Group_of_Perm 3)
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
2 * M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(2 * M) + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (2 * M) is finite V50(2 * M) 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 * M ) } is set
a | (Seg (2 * M)) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like Element of bool [:NAT, the carrier of (Group_of_Perm 3):]
[:NAT, the carrier of (Group_of_Perm 3):] is non empty non trivial non finite set
bool [:NAT, the carrier of (Group_of_Perm 3):] is non empty non trivial cup-closed diff-closed preBoolean non finite set
rng (a | (Seg (2 * M))) is finite set
Seg ((2 * M) + 1) is finite V50((2 * M) + 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 <= (2 * M) + 1 ) } is set
a | (Seg ((2 * M) + 1)) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like Element of bool [:NAT, the carrier of (Group_of_Perm 3):]
(a | (Seg ((2 * M) + 1))) | (Seg (2 * M)) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like Element of bool [:NAT, the carrier of (Group_of_Perm 3):]
a | ((2 * M) + 1) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
a | (Seg ((2 * M) + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(a | ((2 * M) + 1)) | (2 * M) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
(a | ((2 * M) + 1)) | (Seg (2 * M)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
a | (2 * M) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
a | (Seg (2 * M)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
i is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
dom i is finite Element of bool NAT
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
i . p is set
a . p is set
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
((2 * M) + 1) + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
len (a | (Seg ((2 * M) + 1))) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(a | (Seg ((2 * M) + 1))) . ((2 * M) + 1) is set
<*((a | (Seg ((2 * M) + 1))) . ((2 * M) + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,((a | (Seg ((2 * M) + 1))) . ((2 * M) + 1))] is set
{[1,((a | (Seg ((2 * M) + 1))) . ((2 * M) + 1))]} is Function-like non empty trivial finite V50(1) set
((a | (Seg ((2 * M) + 1))) | (Seg (2 * M))) ^ <*((a | (Seg ((2 * M) + 1))) . ((2 * M) + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
M + 1 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
2 * (M + 1) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (2 * (M + 1)) is finite V50(2 * (M + 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 <= 2 * (M + 1) ) } is set
(2 * M) + 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
a . ((2 * M) + 2) is set
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
a . (((2 * M) + 1) + 1) is set
a /. ((2 * M) + 2) is Element of the carrier of (Group_of_Perm 3)
a . ((2 * M) + 1) is set
c9 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
k * c9 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):]
[:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is finite set
bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):] is non empty cup-closed diff-closed preBoolean finite V47() set
a /. ((2 * M) + 1) is Element of the carrier of (Group_of_Perm 3)
<*(a . (((2 * M) + 1) + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,(a . (((2 * M) + 1) + 1))] is set
{[1,(a . (((2 * M) + 1) + 1))]} is Function-like non empty trivial finite V50(1) set
(a | (Seg ((2 * M) + 1))) ^ <*(a . (((2 * M) + 1) + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*(a /. ((2 * M) + 1))*> is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of (Group_of_Perm 3)
1 -tuples_on the carrier of (Group_of_Perm 3) is functional non empty FinSequence-membered FinSequenceSet of the carrier of (Group_of_Perm 3)
the carrier of (Group_of_Perm 3) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (Group_of_Perm 3)
{ b1 where b1 is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of (Group_of_Perm 3) * : len b1 = 1 } is set
[1,(a /. ((2 * M) + 1))] is set
{[1,(a /. ((2 * M) + 1))]} is Function-like non empty trivial finite V50(1) set
<*(a /. ((2 * M) + 2))*> is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of (Group_of_Perm 3)
[1,(a /. ((2 * M) + 2))] is set
{[1,(a /. ((2 * M) + 2))]} is Function-like non empty trivial finite V50(1) set
<*(a /. ((2 * M) + 1))*> ^ <*(a /. ((2 * M) + 2))*> is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
i ^ (<*(a /. ((2 * M) + 1))*> ^ <*(a /. ((2 * M) + 2))*>) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
Product i is Element of the carrier of (Group_of_Perm 3)
Product (<*(a /. ((2 * M) + 1))*> ^ <*(a /. ((2 * M) + 2))*>) is Element of the carrier of (Group_of_Perm 3)
(Product i) * (Product (<*(a /. ((2 * M) + 1))*> ^ <*(a /. ((2 * M) + 2))*>)) is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) is Relation-like [: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] -defined the carrier of (Group_of_Perm 3) -valued Function-like non empty total quasi_total associative having_a_unity V156( the carrier of (Group_of_Perm 3)) Element of bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):]
[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):] is non empty set
[:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty set
bool [:[: the carrier of (Group_of_Perm 3), the carrier of (Group_of_Perm 3):], the carrier of (Group_of_Perm 3):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 3) . ((Product i),(Product (<*(a /. ((2 * M) + 1))*> ^ <*(a /. ((2 * M) + 2))*>))) is Element of the carrier of (Group_of_Perm 3)
Product <*(a /. ((2 * M) + 1))*> is Element of the carrier of (Group_of_Perm 3)
(Product <*(a /. ((2 * M) + 1))*>) * (a /. ((2 * M) + 2)) is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) . ((Product <*(a /. ((2 * M) + 1))*>),(a /. ((2 * M) + 2))) is Element of the carrier of (Group_of_Perm 3)
(Product i) * ((Product <*(a /. ((2 * M) + 1))*>) * (a /. ((2 * M) + 2))) is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) . ((Product i),((Product <*(a /. ((2 * M) + 1))*>) * (a /. ((2 * M) + 2)))) is Element of the carrier of (Group_of_Perm 3)
(a /. ((2 * M) + 1)) * (a /. ((2 * M) + 2)) is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) . ((a /. ((2 * M) + 1)),(a /. ((2 * M) + 2))) is Element of the carrier of (Group_of_Perm 3)
(Product i) * ((a /. ((2 * M) + 1)) * (a /. ((2 * M) + 2))) is Element of the carrier of (Group_of_Perm 3)
the multF of (Group_of_Perm 3) . ((Product i),((a /. ((2 * M) + 1)) * (a /. ((2 * M) + 2)))) is Element of the carrier of (Group_of_Perm 3)
B is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
x is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
x * B is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations 3))),(Seg (len (Permutations 3))):]
len i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
2 * 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
a is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom a is finite Element of bool NAT
Product a is Element of the carrier of (Group_of_Perm 3)
1_ (Group_of_Perm 3) is non being_of_order_0 Element of the carrier of (Group_of_Perm 3)
<*> the carrier of (Group_of_Perm 3) is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like one-to-one constant functional empty proper V29() V30() V31() V33() V34() V35() V36() ext-real non positive non negative V40() finite finite-yielding V47() V48() V50( {} ) FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of (Group_of_Perm 3)
[:NAT, the carrier of (Group_of_Perm 3):] is non empty non trivial non finite set
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
2 * K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(2 * K) + 0 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
n is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
len n is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len n) mod 2 is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom n is finite Element of bool NAT
Product n is Element of the carrier of (Group_of_Perm 3)
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
n . K is set
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
K is Relation-like NAT -defined the carrier of (Group_of_Perm 3) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 3)
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 3)
dom K is finite Element of bool NAT
n is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite non even Element of bool [:(Seg 3),(Seg 3):]
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 carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
i is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
c9 is Element of the carrier of n
x is Element of the carrier of n
B is Element of the carrier of n
<*c9,x,B*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
<*c9*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*B*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,B] is set
{[1,B]} is Function-like non empty trivial finite V50(1) set
(<*c9*> ^ <*x*>) ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
B is Element of the carrier of n
a3 is Element of the carrier of n
a4 is Element of the carrier of n
<*B,a3,a4*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*B*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,B] is set
{[1,B]} is Function-like non empty trivial finite V50(1) set
<*a3*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,a3] is set
{[1,a3]} is Function-like non empty trivial finite V50(1) set
<*B*> ^ <*a3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*a4*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,a4] is set
{[1,a4]} is Function-like non empty trivial finite V50(1) set
(<*B*> ^ <*a3*>) ^ <*a4*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
a5 is Element of the carrier of n
a6 is Element of the carrier of n
id3 is Element of the carrier of n
<*a5,a6,id3*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*a5*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,a5] is set
{[1,a5]} is Function-like non empty trivial finite V50(1) set
<*a6*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,a6] is set
{[1,a6]} is Function-like non empty trivial finite V50(1) set
<*a5*> ^ <*a6*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*id3*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,id3] is set
{[1,id3]} is Function-like non empty trivial finite V50(1) set
(<*a5*> ^ <*a6*>) ^ <*id3*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*c9,x,B*>,<*B,a3,a4*>,<*a5,a6,id3*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*c9,x,B*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*c9,x,B*>] is set
{[1,<*c9,x,B*>]} is Function-like non empty trivial finite V50(1) set
<*<*B,a3,a4*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*B,a3,a4*>] is set
{[1,<*B,a3,a4*>]} is Function-like non empty trivial finite V50(1) set
<*<*c9,x,B*>*> ^ <*<*B,a3,a4*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*a5,a6,id3*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*a5,a6,id3*>] is set
{[1,<*a5,a6,id3*>]} is Function-like non empty trivial finite V50(1) set
(<*<*c9,x,B*>*> ^ <*<*B,a3,a4*>*>) ^ <*<*a5,a6,id3*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
c9 * a3 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 . (c9,a3) is Element of the carrier of n
(c9 * a3) * id3 is Element of the carrier of n
the multF of n . ((c9 * a3),id3) is Element of the carrier of n
B * a3 is Element of the carrier of n
the multF of n . (B,a3) is Element of the carrier of n
(B * a3) * a5 is Element of the carrier of n
the multF of n . ((B * a3),a5) is Element of the carrier of n
((c9 * a3) * id3) - ((B * a3) * a5) is Element of the carrier of n
- ((B * a3) * a5) is Element of the carrier of n
((c9 * a3) * id3) + (- ((B * a3) * a5)) 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 . (((c9 * a3) * id3),(- ((B * a3) * a5))) is Element of the carrier of n
c9 * a4 is Element of the carrier of n
the multF of n . (c9,a4) is Element of the carrier of n
(c9 * a4) * a6 is Element of the carrier of n
the multF of n . ((c9 * a4),a6) is Element of the carrier of n
(((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6) is Element of the carrier of n
- ((c9 * a4) * a6) is Element of the carrier of n
(((c9 * a3) * id3) - ((B * a3) * a5)) + (- ((c9 * a4) * a6)) is Element of the carrier of n
the addF of n . ((((c9 * a3) * id3) - ((B * a3) * a5)),(- ((c9 * a4) * a6))) is Element of the carrier of n
x * a4 is Element of the carrier of n
the multF of n . (x,a4) is Element of the carrier of n
(x * a4) * a5 is Element of the carrier of n
the multF of n . ((x * a4),a5) is Element of the carrier of n
((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5) is Element of the carrier of n
the addF of n . (((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)),((x * a4) * a5)) is Element of the carrier of n
x * B is Element of the carrier of n
the multF of n . (x,B) is Element of the carrier of n
(x * B) * id3 is Element of the carrier of n
the multF of n . ((x * B),id3) is Element of the carrier of n
(((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5)) - ((x * B) * id3) is Element of the carrier of n
- ((x * B) * id3) is Element of the carrier of n
(((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5)) + (- ((x * B) * id3)) is Element of the carrier of n
the addF of n . ((((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5)),(- ((x * B) * id3))) is Element of the carrier of n
B * B is Element of the carrier of n
the multF of n . (B,B) is Element of the carrier of n
(B * B) * a6 is Element of the carrier of n
the multF of n . ((B * B),a6) is Element of the carrier of n
((((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5)) - ((x * B) * id3)) + ((B * B) * a6) is Element of the carrier of n
the addF of n . (((((((c9 * a3) * id3) - ((B * a3) * a5)) - ((c9 * a4) * a6)) + ((x * a4) * a5)) - ((x * B) * id3)),((B * B) * a6)) is Element of the carrier of n
Id3 is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
Det Id3 is Element of the carrier of n
FinOmega (Permutations 3) is finite Element of Fin (Permutations 3)
Fin (Permutations 3) is non empty cup-closed diff-closed preBoolean set
p is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
k is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
K is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
a is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
M is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
N is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
{p,k,K,a,M,N} is non empty finite set
{.p,k,K.} is non empty finite Element of Fin (Permutations 3)
{.a,M,N.} is non empty finite Element of Fin (Permutations 3)
B1 is finite Element of Fin (Permutations 3)
{p,k,K} is non empty finite set
{a,M,N} is non empty finite set
{p,k,K} \/ {a,M,N} is non empty finite set
r1 is set
B2 is finite Element of Fin (Permutations 3)
r is finite Element of Fin (Permutations 3)
B2 \ r is finite Element of Fin (Permutations 3)
r1 is set
Path_product Id3 is Relation-like Permutations 3 -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations 3), the carrier of n:]
[:(Permutations 3), the carrier of n:] is non empty set
bool [:(Permutations 3), the carrier of n:] is non empty cup-closed diff-closed preBoolean set
(Path_product Id3) . i is set
(Path_product Id3) . k is Element of the carrier of n
(Path_product Id3) . K is Element of the carrier of n
(Path_product Id3) . a is Element of the carrier of n
(Path_product Id3) . M is Element of the carrier of n
(Path_product Id3) . N is Element of the carrier of n
Path_matrix (p,Id3) 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 (p,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (p,Id3))),p) is Element of the carrier of n
<*c9,a3,id3*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*c9*> ^ <*a3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*c9*> ^ <*a3*>) ^ <*id3*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*c9,a3,id3*> is Element of the carrier of n
Path_matrix (N,Id3) 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 (N,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (N,Id3))),N) is Element of the carrier of n
<*B,B,a6*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*B*> ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*B*> ^ <*B*>) ^ <*a6*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*B,B,a6*> is Element of the carrier of n
Path_matrix (M,Id3) 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 (M,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (M,Id3))),M) is Element of the carrier of n
- ( the multF of n $$ (Path_matrix (M,Id3))) is Element of the carrier of n
<*x,B,id3*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*x*> ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*x*> ^ <*B*>) ^ <*id3*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*x,B,id3*> is Element of the carrier of n
- ( the multF of n $$ <*x,B,id3*>) is Element of the carrier of n
Path_matrix (a,Id3) 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 (a,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (a,Id3))),a) is Element of the carrier of n
<*x,a4,a5*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*x*> ^ <*a4*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*x*> ^ <*a4*>) ^ <*a5*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*x,a4,a5*> is Element of the carrier of n
Path_matrix (K,Id3) 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,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (K,Id3))),K) is Element of the carrier of n
- ( the multF of n $$ (Path_matrix (K,Id3))) is Element of the carrier of n
<*c9,a4,a6*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*c9*> ^ <*a4*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*c9*> ^ <*a4*>) ^ <*a6*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*c9,a4,a6*> is Element of the carrier of n
- ( the multF of n $$ <*c9,a4,a6*>) is Element of the carrier of n
Path_matrix (k,Id3) 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,Id3)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (k,Id3))),k) is Element of the carrier of n
- ( the multF of n $$ (Path_matrix (k,Id3))) is Element of the carrier of n
<*B,a3,a5*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*B*> ^ <*a3*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*B*> ^ <*a3*>) ^ <*a5*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*B,a3,a5*> is Element of the carrier of n
- ( the multF of n $$ <*B,a3,a5*>) is Element of the carrier of n
the addF of n $$ (B2,(Path_product Id3)) is Element of the carrier of n
r2 is Element of the carrier of n
r3 is Element of the carrier of n
r2 + r3 is Element of the carrier of n
the addF of n . (r2,r3) is Element of the carrier of n
r4 is Element of the carrier of n
(r2 + r3) + r4 is Element of the carrier of n
the addF of n . ((r2 + r3),r4) is Element of the carrier of n
the addF of n $$ (r,(Path_product Id3)) is Element of the carrier of n
r5 is Element of the carrier of n
r6 is Element of the carrier of n
r5 + r6 is Element of the carrier of n
the addF of n . (r5,r6) is Element of the carrier of n
X is Element of the carrier of n
(r5 + r6) + X is Element of the carrier of n
the addF of n . ((r5 + r6),X) is Element of the carrier of n
the addF of n $$ ((FinOmega (Permutations 3)),(Path_product Id3)) is Element of the carrier of n
the addF of n . (( the addF of n $$ (B2,(Path_product Id3))),( the addF of n $$ (r,(Path_product Id3)))) is Element of the carrier of n
r6 + X is Element of the carrier of n
the addF of n . (r6,X) is Element of the carrier of n
r5 + (r6 + X) is Element of the carrier of n
the addF of n . (r5,(r6 + X)) is Element of the carrier of n
((r2 + r3) + r4) + (r5 + (r6 + X)) is Element of the carrier of n
the addF of n . (((r2 + r3) + r4),(r5 + (r6 + X))) is Element of the carrier of n
((r2 + r3) + r4) + r5 is Element of the carrier of n
the addF of n . (((r2 + r3) + r4),r5) is Element of the carrier of n
(((r2 + r3) + r4) + r5) + (r6 + X) is Element of the carrier of n
the addF of n . ((((r2 + r3) + r4) + r5),(r6 + X)) 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 carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial non finite set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean non finite set
a is Element of the carrier of n
M is Element of the carrier of n
N is Element of the carrier of n
<*a,M,N*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) 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 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
(<*a*> ^ <*M*>) ^ <*N*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
i is Element of the carrier of n
p is Element of the carrier of n
k is Element of the carrier of n
<*i,p,k*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*i*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,i] is set
{[1,i]} is Function-like non empty trivial finite V50(1) set
<*p*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,p] is set
{[1,p]} is Function-like non empty trivial finite V50(1) set
<*i*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*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
(<*i*> ^ <*p*>) ^ <*k*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
c9 is Element of the carrier of n
x is Element of the carrier of n
B is Element of the carrier of n
<*c9,x,B*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*c9*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,c9] is set
{[1,c9]} is Function-like non empty trivial finite V50(1) set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,x] is set
{[1,x]} is Function-like non empty trivial finite V50(1) set
<*c9*> ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*B*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,B] is set
{[1,B]} is Function-like non empty trivial finite V50(1) set
(<*c9*> ^ <*x*>) ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
<*<*a,M,N*>,<*i,p,k*>,<*c9,x,B*>*> is Relation-like NAT -defined bool [:NAT, the carrier of n:] -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of bool [:NAT, the carrier of n:]
<*<*a,M,N*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*a,M,N*>] is set
{[1,<*a,M,N*>]} is Function-like non empty trivial finite V50(1) set
<*<*i,p,k*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*i,p,k*>] is set
{[1,<*i,p,k*>]} is Function-like non empty trivial finite V50(1) set
<*<*a,M,N*>*> ^ <*<*i,p,k*>*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
<*<*c9,x,B*>*> is Relation-like NAT -defined Function-like constant non empty trivial finite V50(1) FinSequence-like FinSubsequence-like set
[1,<*c9,x,B*>] is set
{[1,<*c9,x,B*>]} is Function-like non empty trivial finite V50(1) set
(<*<*a,M,N*>*> ^ <*<*i,p,k*>*>) ^ <*<*c9,x,B*>*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
a * p 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,p) is Element of the carrier of n
(a * p) * B is Element of the carrier of n
the multF of n . ((a * p),B) is Element of the carrier of n
N * p is Element of the carrier of n
the multF of n . (N,p) is Element of the carrier of n
(N * p) * c9 is Element of the carrier of n
the multF of n . ((N * p),c9) is Element of the carrier of n
((a * p) * B) + ((N * p) * c9) 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 . (((a * p) * B),((N * p) * c9)) is Element of the carrier of n
a * k is Element of the carrier of n
the multF of n . (a,k) is Element of the carrier of n
(a * k) * x is Element of the carrier of n
the multF of n . ((a * k),x) is Element of the carrier of n
(((a * p) * B) + ((N * p) * c9)) + ((a * k) * x) is Element of the carrier of n
the addF of n . ((((a * p) * B) + ((N * p) * c9)),((a * k) * x)) is Element of the carrier of n
M * k is Element of the carrier of n
the multF of n . (M,k) is Element of the carrier of n
(M * k) * c9 is Element of the carrier of n
the multF of n . ((M * k),c9) is Element of the carrier of n
((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)) + ((M * k) * c9) is Element of the carrier of n
the addF of n . (((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)),((M * k) * c9)) is Element of the carrier of n
M * i is Element of the carrier of n
the multF of n . (M,i) is Element of the carrier of n
(M * i) * B is Element of the carrier of n
the multF of n . ((M * i),B) is Element of the carrier of n
(((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)) + ((M * k) * c9)) + ((M * i) * B) is Element of the carrier of n
the addF of n . ((((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)) + ((M * k) * c9)),((M * i) * B)) is Element of the carrier of n
N * i is Element of the carrier of n
the multF of n . (N,i) is Element of the carrier of n
(N * i) * x is Element of the carrier of n
the multF of n . ((N * i),x) is Element of the carrier of n
((((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)) + ((M * k) * c9)) + ((M * i) * B)) + ((N * i) * x) is Element of the carrier of n
the addF of n . (((((((a * p) * B) + ((N * p) * c9)) + ((a * k) * x)) + ((M * k) * c9)) + ((M * i) * B)),((N * i) * x)) is Element of the carrier of n
B is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of 3,3, the carrier of n
(3,n,B) is Element of the carrier of n
FinOmega (Permutations 3) is finite Element of Fin (Permutations 3)
Fin (Permutations 3) is non empty cup-closed diff-closed preBoolean set
(3,n,B) is Relation-like Permutations 3 -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations 3), the carrier of n:]
[:(Permutations 3), the carrier of n:] is non empty set
bool [:(Permutations 3), the carrier of n:] is non empty cup-closed diff-closed preBoolean set
the addF of n $$ ((FinOmega (Permutations 3)),(3,n,B)) is Element of the carrier of n
Id3 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
K is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
a3 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
{.Id3,K,a3.} is non empty finite Element of Fin (Permutations 3)
a4 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
a5 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
a6 is Relation-like Seg (len (Permutations 3)) -defined Seg (len (Permutations 3)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations 3
{.a4,a5,a6.} is non empty finite Element of Fin (Permutations 3)
id3 is Relation-like Seg 3 -defined Seg 3 -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 3),(Seg 3):]
(3,n,B) . id3 is set
Path_matrix (Id3,B) 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 (Id3,B)) is Element of the carrier of n
<*a,p,B*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*a*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*a*> ^ <*p*>) ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*a,p,B*> is Element of the carrier of n
(3,n,B) . a6 is Element of the carrier of n
Path_matrix (a6,B) 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 (a6,B)) is Element of the carrier of n
<*N,i,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*N*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*N*> ^ <*i*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*N,i,x*> is Element of the carrier of n
(3,n,B) . a5 is Element of the carrier of n
Path_matrix (a5,B) 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 (a5,B)) is Element of the carrier of n
<*M,i,B*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*M*> ^ <*i*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*M*> ^ <*i*>) ^ <*B*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*M,i,B*> is Element of the carrier of n
(3,n,B) . a4 is Element of the carrier of n
Path_matrix (a4,B) 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 (a4,B)) is Element of the carrier of n
<*M,k,c9*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*M*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*M*> ^ <*k*>) ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*M,k,c9*> is Element of the carrier of n
F is set
B1 is finite Element of Fin (Permutations 3)
B2 is finite Element of Fin (Permutations 3)
B1 \ B2 is finite Element of Fin (Permutations 3)
F is set
(3,n,B) . K is Element of the carrier of n
(3,n,B) . a3 is Element of the carrier of n
{Id3,K,a3,a4,a5,a6} is non empty finite set
the addF of n $$ (B1,(3,n,B)) is Element of the carrier of n
r1 is Element of the carrier of n
r2 is Element of the carrier of n
r1 + r2 is Element of the carrier of n
the addF of n . (r1,r2) is Element of the carrier of n
r3 is Element of the carrier of n
(r1 + r2) + r3 is Element of the carrier of n
the addF of n . ((r1 + r2),r3) is Element of the carrier of n
the addF of n $$ (B2,(3,n,B)) is Element of the carrier of n
r4 is Element of the carrier of n
r5 is Element of the carrier of n
r4 + r5 is Element of the carrier of n
the addF of n . (r4,r5) is Element of the carrier of n
r6 is Element of the carrier of n
(r4 + r5) + r6 is Element of the carrier of n
the addF of n . ((r4 + r5),r6) is Element of the carrier of n
Path_matrix (K,B) 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,B)) is Element of the carrier of n
<*N,p,c9*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*N*> ^ <*p*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*N*> ^ <*p*>) ^ <*c9*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*N,p,c9*> is Element of the carrier of n
Path_matrix (a3,B) 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 (a3,B)) is Element of the carrier of n
<*a,k,x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty non trivial finite V50(3) FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*a*> ^ <*k*> is Relation-like NAT -defined Function-like non empty finite V50(1 + 1) FinSequence-like FinSubsequence-like set
(<*a*> ^ <*k*>) ^ <*x*> is Relation-like NAT -defined Function-like non empty finite V50((1 + 1) + 1) FinSequence-like FinSubsequence-like set
the multF of n $$ <*a,k,x*> is Element of the carrier of n
X is finite Element of Fin (Permutations 3)
{Id3,K,a3} is non empty finite set
{a4,a5,a6} is non empty finite set
{Id3,K,a3} \/ {a4,a5,a6} is non empty finite set
the addF of n . (( the addF of n $$ (B1,(3,n,B))),( the addF of n $$ (B2,(3,n,B)))) is Element of the carrier of n
r5 + r6 is Element of the carrier of n
the addF of n . (r5,r6) is Element of the carrier of n
r4 + (r5 + r6) is Element of the carrier of n
the addF of n . (r4,(r5 + r6)) is Element of the carrier of n
((r1 + r2) + r3) + (r4 + (r5 + r6)) is Element of the carrier of n
the addF of n . (((r1 + r2) + r3),(r4 + (r5 + r6))) is Element of the carrier of n
((r1 + r2) + r3) + r4 is Element of the carrier of n
the addF of n . (((r1 + r2) + r3),r4) is Element of the carrier of n
(((r1 + r2) + r3) + r4) + (r5 + r6) is Element of the carrier of n
the addF of n . ((((r1 + r2) + r3) + r4),(r5 + r6)) is Element of the carrier of n
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Permutations K is non empty permutational 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
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
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
a 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
[:(Seg K),(Seg K):] is finite set
bool [:(Seg K),(Seg K):] is non empty cup-closed diff-closed preBoolean finite V47() set
dom a is finite set
M is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng M is finite set
dom M is finite Element of bool NAT
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
M . N is 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
Permutations n is non empty permutational 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
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
0. K is V62(K) Element of the carrier of K
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
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,M) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,M) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
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
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
i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
N . i is set
dom a is finite Element of bool NAT
(Path_matrix (N,a)) . i is set
len (Path_matrix (N,a)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (N,a)) is finite Element of bool NAT
a * (i,M) is Element of the carrier of K
(Col (a,M)) . i is set
n is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
Permutations n is non empty permutational 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
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
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
0. K is V62(K) Element of the carrier of K
a 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 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
Path_product 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:]
[:(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
(Path_product M) . a is Element of the carrier of K
Path_matrix (a,M) 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 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
the multF of K $$ (Path_matrix (a,M)) is Element of the carrier of K
- (( the multF of K $$ (Path_matrix (a,M))),a) is Element of the carrier of K
Product (Path_matrix (a,M)) is Element of the carrier of K
- ((Product (Path_matrix (a,M))),a) is Element of the carrier of K
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (M,N) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of K
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len M } is set
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(Path_matrix (a,M)) . N is set
len (Path_matrix (a,M)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a,M)) is finite Element of bool NAT
- (Product (Path_matrix (a,M))) is Element of the carrier of K
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
Permutations n is non empty permutational set
FinOmega (Permutations n) is finite Element of Fin (Permutations n)
Fin (Permutations n) is non empty cup-closed diff-closed preBoolean 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
0. K is V62(K) Element of the carrier of K
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
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
Path_product 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)),(Path_product a)) is Element of the carrier of K
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
N is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of M,M, the carrier of K
Path_product N is Relation-like Permutations M -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Permutations M), the carrier of K:]
Permutations M is non empty permutational set
[:(Permutations M), the carrier of K:] is non empty set
bool [:(Permutations M), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Fin (Permutations M) is non empty cup-closed diff-closed preBoolean set
len (Permutations M) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len (Permutations M)) is finite V50( len (Permutations M)) 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 M) ) } is set
x is non empty finite Element of Fin (Permutations M)
B is Relation-like Seg (len (Permutations M)) -defined Seg (len (Permutations M)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations M
{.B.} is functional non empty trivial finite V47() V50(1) Element of Fin (Permutations M)
B is non empty finite Element of Fin (Permutations M)
the addF of K $$ (B,(Path_product N)) is Element of the carrier of K
B \/ {.B.} is non empty finite Element of Fin (Permutations M)
the addF of K $$ ((B \/ {.B.}),(Path_product N)) is Element of the carrier of K
(Path_product N) . B is Element of the carrier of K
the addF of K . (( the addF of K $$ (B,(Path_product N))),((Path_product N) . B)) is Element of the carrier of K
( the addF of K $$ (B,(Path_product N))) + (0. K) is Element of the carrier of K
the addF of K . (( the addF of K $$ (B,(Path_product N))),(0. K)) is Element of the carrier of K
B is Relation-like Seg (len (Permutations M)) -defined Seg (len (Permutations M)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations M
{.B.} is functional non empty trivial finite V47() V50(1) Element of Fin (Permutations M)
the addF of K $$ ({.B.},(Path_product N)) is Element of the carrier of K
(Path_product N) . B is Element of the carrier of K
the addF of K $$ (x,(Path_product N)) is Element 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
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
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
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
0. K is V62(K) Element of the carrier of K
a 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 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,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:]
[:(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
(n,K,M) . a is Element of the carrier of K
Path_matrix (a,M) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (M,N) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of K
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len M } is set
N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(Path_matrix (a,M)) . N is set
len (Path_matrix (a,M)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (a,M)) is finite Element of bool NAT
Product (Path_matrix (a,M)) is Element of 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
the multF of K $$ (Path_matrix (a,M)) is Element of the carrier of K
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
Permutations n is non empty permutational set
FinOmega (Permutations n) is finite Element of Fin (Permutations n)
Fin (Permutations n) is non empty cup-closed diff-closed preBoolean 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
0. K is V62(K) Element of the carrier of K
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
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
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
N is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of M,M, the carrier of K
(M,K,N) is Relation-like Permutations M -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Permutations M), the carrier of K:]
Permutations M is non empty permutational set
[:(Permutations M), the carrier of K:] is non empty set
bool [:(Permutations M), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
FinOmega (Permutations M) is finite Element of Fin (Permutations M)
Fin (Permutations M) is non empty cup-closed diff-closed preBoolean set
len (Permutations M) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Seg (len (Permutations M)) is finite V50( len (Permutations M)) 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 M) ) } is set
c9 is non empty finite Element of Fin (Permutations M)
x is Relation-like Seg (len (Permutations M)) -defined Seg (len (Permutations M)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations M
{.x.} is functional non empty trivial finite V47() V50(1) Element of Fin (Permutations M)
B is non empty finite Element of Fin (Permutations M)
the addF of K $$ (B,(M,K,N)) is Element of the carrier of K
B \/ {.x.} is non empty finite Element of Fin (Permutations M)
the addF of K $$ ((B \/ {.x.}),(M,K,N)) is Element of the carrier of K
(M,K,N) . x is Element of the carrier of K
the addF of K . (( the addF of K $$ (B,(M,K,N))),((M,K,N) . x)) is Element of the carrier of K
( the addF of K $$ (B,(M,K,N))) + (0. K) is Element of the carrier of K
the addF of K . (( the addF of K $$ (B,(M,K,N))),(0. K)) is Element of the carrier of K
B is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,B) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
x is Relation-like Seg (len (Permutations M)) -defined Seg (len (Permutations M)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations M
{.x.} is functional non empty trivial finite V47() V50(1) Element of Fin (Permutations M)
the addF of K $$ ({.x.},(M,K,N)) is Element of the carrier of K
(M,K,N) . x is Element of the carrier of K
B is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,B) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
the addF of K $$ (c9,(M,K,N)) is Element of the carrier of K
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
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
0. K is V62(K) Element of the carrier of K
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
Det a is Element of the carrier of K
Path_product 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 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
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
the addF of K $$ ((FinOmega (Permutations n)),(Path_product a)) is Element of the carrier of K
i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (a,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } 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
M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
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
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
Col (a,M) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len a) FinSequence-like FinSubsequence-like Element of (len a) -tuples_on the carrier of K
len a is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len a) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len a } is set
0. K is V62(K) Element of the carrier of K
(n,K,a) is Element of the carrier of K
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
(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 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
Permutations n is non empty permutational 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
K is V29() V30() V31() V35() V36() ext-real V40() finite V48() set
a 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 a is non empty non trivial set
the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a
N is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of a
Col (N,K) is Relation-like NAT -defined the carrier of a -valued Function-like finite V50( len N) FinSequence-like FinSubsequence-like Element of (len N) -tuples_on the carrier of a
len N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len N) -tuples_on the carrier of a is functional non empty FinSequence-membered FinSequenceSet of the carrier of a
{ b1 where b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of a * : len b1 = len N } is set
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
Path_matrix (i,N) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of a
p is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
i . p is set
len (Path_matrix (i,N)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (i,N)) is finite Element of bool NAT
(Path_matrix (i,N)) . p is set
N * (p,K) is Element of the carrier of a
(Path_matrix (i,N)) /. p is Element of the carrier of a
(Col (N,K)) /. p is Element of the carrier of a
dom N is finite Element of bool NAT
(Col (N,K)) . p is set
len (Col (N,K)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Col (N,K)) is finite V50( len N) 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
Permutations n is non empty permutational 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
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
a is Element of the carrier of K
M 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 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
i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (M,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of K
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len M } is set
Col (N,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len N) FinSequence-like FinSubsequence-like Element of (len N) -tuples_on the carrier of K
len N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len N) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len N } is set
i is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
Col (M,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len M) FinSequence-like FinSubsequence-like Element of (len M) -tuples_on the carrier of K
len M is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len M) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len M } is set
Col (N,i) is Relation-like NAT -defined the carrier of K -valued Function-like finite V50( len N) FinSequence-like FinSubsequence-like Element of (len N) -tuples_on the carrier of K
len N is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
(len N) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = len N } is set
p 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
Path_matrix (p,M) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
Path_matrix (p,N) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
k is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
p . k is set
len (Path_matrix (p,N)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (p,N)) is finite Element of bool NAT
(Path_matrix (p,N)) . k is set
N * (k,i) is Element of the carrier of K
(Path_matrix (p,N)) /. k is Element of the carrier of K
len (Col (N,i)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Col (N,i)) is finite V50( len N) Element of bool NAT
dom N is finite Element of bool NAT
(Col (N,i)) . k is set
(Col (N,i)) /. k is Element of the carrier of K
dom M is finite Element of bool NAT
(Path_matrix (p,M)) /. k is Element of the carrier of K
a * ((Path_matrix (p,N)) /. k) is Element of 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
the multF of K . (a,((Path_matrix (p,N)) /. k)) is Element of the carrier of K
len (Path_matrix (p,M)) is V29() V30() V31() V35() V36() ext-real V40() finite V48() Element of NAT
dom (Path_matrix (p,M)) is finite Element of bool NAT
(Path_matrix (p,M)) . k is set
M * (k,i) is Element of the carrier of K
(Col (M,i)) . k is set