:: MATRIX_7 semantic presentation

REAL is set
NAT is non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty cup-closed diff-closed preBoolean set
{} is set
the Function-like functional empty V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V44() cardinal {} -element FinSequence-membered set is Function-like functional empty V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V44() cardinal {} -element FinSequence-membered set
COMPLEX is set
NAT is non empty non trivial V26() V27() V28() V40() cardinal limit_cardinal set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean V40() set
bool NAT is non empty non trivial cup-closed diff-closed preBoolean V40() set
Fin NAT is non empty cup-closed diff-closed preBoolean set
INT is set
1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
3 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg 1 is non empty trivial V40() 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 1 ) } is set
{1} is non empty trivial V40() V44() 1 -element set
Seg 2 is non empty V40() 2 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 2 ) } is set
{1,2} is V40() V44() set
idseq 2 is Relation-like NAT -defined Function-like V40() 2 -element 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 V40() V112() V114() V115() V119() Element of bool [:(Seg 2),(Seg 2):]
[:(Seg 2),(Seg 2):] is non empty V40() set
bool [:(Seg 2),(Seg 2):] is non empty cup-closed diff-closed preBoolean V40() V44() set
<*1,2*> is Relation-like NAT -defined Function-like non empty V40() 2 -element FinSequence-like FinSubsequence-like set
<*1*> is Relation-like NAT -defined Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like set
[1,1] is set
{1,1} is V40() V44() set
{{1,1},{1}} is V40() V44() set
{[1,1]} is Function-like non empty trivial V40() 1 -element set
<*2*> is Relation-like NAT -defined Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like set
[1,2] is set
{{1,2},{1}} is V40() V44() set
{[1,2]} is Function-like non empty trivial V40() 1 -element set
<*1*> ^ <*2*> is Relation-like NAT -defined Function-like non empty V40() 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
<*2,1*> is Relation-like NAT -defined Function-like non empty V40() 2 -element FinSequence-like FinSubsequence-like set
<*2*> ^ <*1*> is Relation-like NAT -defined Function-like non empty V40() 1 + 1 -element FinSequence-like FinSubsequence-like set
n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective V40() Element of bool [:(Seg 2),(Seg 2):]
rng n is V40() set
n . 2 is set
dom n is V40() set
K is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
n . 1 is set
n is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
len <*1,2*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
len <*2,1*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
dom n is V40() Element of bool NAT
rng n is V40() set
K is set
n . 1 is set
n . 2 is set
A is set
n . A is set
A is set
f is set
n . A is set
n . f is set
A is set
f is set
n . f is set
len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is set
n . 1 is set
n . 2 is set
K is Relation-like Seg 2 -defined Seg 2 -valued Function-like non empty total quasi_total V40() Element of bool [:(Seg 2),(Seg 2):]
A is set
f is set
n . A is set
n . f is set
A is set
f is set
n . f is set
len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is set
n . 2 is set
n . 1 is set
K is Relation-like Seg 2 -defined Seg 2 -valued Function-like non empty total quasi_total V40() Element of bool [:(Seg 2),(Seg 2):]
Permutations 2 is non empty permutational set
{<*1,2*>,<*2,1*>} is functional V40() V44() set
n is set
{(idseq 2),<*2,1*>} is functional V40() V44() 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 V40() Element of bool [:(Seg 2),(Seg 2):]
n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective V40() Element of bool [:(Seg 2),(Seg 2):]
dom n is V40() set
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
n . A is set
n . f is set
len <*1,2*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
n is non empty set
K is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
mid (K,1,A) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
A + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
mid (K,(A + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(mid (K,1,A)) ^ (mid (K,(A + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
mid (K,1,(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
n is non empty set
K is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) -' 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K | ((len K) -' 2) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
Seg ((len K) -' 2) is V40() (len K) -' 2 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (len K) -' 2 ) } is set
K | (Seg ((len K) -' 2)) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
(len K) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
mid (K,((len K) -' 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(K | ((len K) -' 2)) ^ (mid (K,((len K) -' 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(len K) - 2 is V33() V34() ext-real set
((len K) -' 2) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) - 1 is V33() V34() ext-real set
((len K) - 1) - 1 is V33() V34() ext-real set
(((len K) - 1) - 1) + 1 is V33() V34() ext-real set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 2) - 2 is V33() V34() ext-real set
mid (K,1,((len K) -' 2)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
mid (K,(((len K) -' 2) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(mid (K,1,((len K) -' 2))) ^ (mid (K,(((len K) -' 2) + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
mid (K,(((len K) -' 2) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
K | 0 is Relation-like NAT -defined n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of n
[:NAT,n:] is non empty non trivial V40() set
Seg 0 is Function-like functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V44() cardinal 0 -element FinSequence-membered Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
K | (Seg 0) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
((len K) - 2) + 1 is V33() V34() ext-real set
n is non empty set
K is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K | ((len K) -' 1) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
Seg ((len K) -' 1) is V40() (len K) -' 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (len K) -' 1 ) } is set
K | (Seg ((len K) -' 1)) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
mid (K,(len K),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(K | ((len K) -' 1)) ^ (mid (K,(len K),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(len K) - 1 is V33() V34() ext-real set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len K) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((len K) + 1) - 1 is V33() V34() ext-real set
mid (K,1,((len K) -' 1)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
((len K) -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
mid (K,(((len K) -' 1) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
(mid (K,1,((len K) -' 1))) ^ (mid (K,(((len K) -' 1) + 1),(len K))) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
K | 0 is Relation-like NAT -defined n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of n
[:NAT,n:] is non empty non trivial V40() set
Seg 0 is Function-like functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V44() cardinal 0 -element FinSequence-membered Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 0 ) } is set
K | (Seg 0) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
((len K) -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
mid (K,(((len K) -' 1) + 1),(len K)) is Relation-like NAT -defined n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of n
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 V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations 2)) is V40() len (Permutations 2) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations 2) ) } is set
n is Element of the carrier of (Group_of_Perm 2)
K is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
dom K is V40() set
A is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective V40() Element of bool [:(Seg 2),(Seg 2):]
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
K . f is set
K . f2 is set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
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 V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is Element of the carrier of (Group_of_Perm n)
f is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
A is Element of the carrier of (Group_of_Perm n)
f2 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
K * A is Element of the carrier of (Group_of_Perm n)
the multF of (Group_of_Perm n) is Relation-like [: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] -defined the carrier of (Group_of_Perm n) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm n)) associative Element of bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):]
[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] is non empty set
[:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty set
bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm n) . (K,A) is Element of the carrier of (Group_of_Perm n)
[K,A] is set
{K,A} is V40() set
{K} is non empty trivial V40() 1 -element set
{{K,A},{K}} is V40() V44() set
the multF of (Group_of_Perm n) . [K,A] is set
f2 * f 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 V40() Element of bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):]
[:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is V40() set
bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is non empty cup-closed diff-closed preBoolean V40() V44() set
n is Element of the carrier of (Group_of_Perm 2)
K is Element of the carrier of (Group_of_Perm 2)
n * K is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) is Relation-like [: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] -defined the carrier of (Group_of_Perm 2) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm 2)) associative Element of bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):]
[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] is non empty set
[:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty set
bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 2) . (n,K) is Element of the carrier of (Group_of_Perm 2)
[n,K] is set
{n,K} is V40() set
{n} is non empty trivial V40() 1 -element set
{{n,K},{n}} is V40() V44() set
the multF of (Group_of_Perm 2) . [n,K] is set
A is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
A is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
f2 is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
f is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len f) is V40() len f -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
dom f is V40() Element of bool NAT
f2 is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
f2 is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
Y is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
F is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
F . 2 is set
f2 * A is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective bijective V40() Element of bool [:(Seg (len (Permutations 2))),(Seg (len (Permutations 2))):]
[:(Seg (len (Permutations 2))),(Seg (len (Permutations 2))):] is V40() set
bool [:(Seg (len (Permutations 2))),(Seg (len (Permutations 2))):] is non empty cup-closed diff-closed preBoolean V40() V44() set
f . 1 is set
(f2 * A) . 1 is set
n is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len n) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom n is V40() Element of bool NAT
Product n is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) is Relation-like [: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] -defined the carrier of (Group_of_Perm 2) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm 2)) associative Element of bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):]
[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] is non empty set
[:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty set
bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 2) "**" n is Element of the carrier of (Group_of_Perm 2)
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
2 * K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(2 * K) + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
2 * K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
2 * A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
2 * (A + 1) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" f is Element of the carrier of (Group_of_Perm 2)
(2 * A) + 2 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len f) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len f) - 1 is V33() V34() ext-real set
(len f) - ((len f) -' 1) is V33() V34() ext-real set
((len f) - ((len f) -' 1)) + 1 is V33() V34() ext-real set
(len f) - ((len f) - 1) is V33() V34() ext-real set
((len f) - ((len f) - 1)) + 1 is V33() V34() ext-real set
mid (f,((len f) -' 1),(len f)) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Seg (len f) is V40() len f -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
f . (len f) is set
len (mid (f,((len f) -' 1),(len f))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Element of the carrier of (Group_of_Perm 2)
(len (mid (f,((len f) -' 1),(len f)))) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Seg ((len (mid (f,((len f) -' 1),(len f)))) -' 1) is V40() (len (mid (f,((len f) -' 1),(len f)))) -' 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (len (mid (f,((len f) -' 1),(len f)))) -' 1 ) } is set
(mid (f,((len f) -' 1),(len f))) | (Seg ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is Element of the carrier of (Group_of_Perm 2)
1 + ((len f) -' 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + ((len f) -' 1)) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(1 + ((len f) -' 1)) - 1 is V33() V34() ext-real set
1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + 1) - 1 is V33() V34() ext-real set
(len f) -' ((len f) -' 1) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len f) -' ((len f) -' 1)) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len (mid (f,((len f) -' 1),(len f)))) - 1 is V33() V34() ext-real set
((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) . 1 is set
(mid (f,((len f) -' 1),(len f))) . 1 is set
f . ((len f) -' 1) is set
(len f) -' 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f | ((len f) -' 2) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Seg ((len f) -' 2) is V40() (len f) -' 2 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (len f) -' 2 ) } is set
f | (Seg ((len f) -' 2)) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
dom (f | ((len f) -' 2)) is V40() Element of bool NAT
X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(f | ((len f) -' 2)) . X is set
len (f | ((len f) -' 2)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (f | ((len f) -' 2))) is V40() len (f | ((len f) -' 2)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (f | ((len f) -' 2)) ) } is set
f . X is set
B is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
len (f | ((len f) -' 2)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product (f | ((len f) -' 2)) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" (f | ((len f) -' 2)) is Element of the carrier of (Group_of_Perm 2)
1_ (Group_of_Perm 2) is non being_of_order_0 Element of the carrier of (Group_of_Perm 2)
(f | ((len f) -' 2)) ^ (mid (f,((len f) -' 1),(len f))) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Product (mid (f,((len f) -' 1),(len f))) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" (mid (f,((len f) -' 1),(len f))) is Element of the carrier of (Group_of_Perm 2)
(Product (f | ((len f) -' 2))) * (Product (mid (f,((len f) -' 1),(len f)))) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) . ((Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))) is Element of the carrier of (Group_of_Perm 2)
[(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))] is set
{(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))} is V40() set
{(Product (f | ((len f) -' 2)))} is non empty trivial V40() 1 -element set
{{(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))},{(Product (f | ((len f) -' 2)))}} is V40() V44() set
the multF of (Group_of_Perm 2) . [(Product (f | ((len f) -' 2))),(Product (mid (f,((len f) -' 1),(len f))))] is set
2 + ((len f) -' 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(2 + ((len f) -' 1)) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(2 + ((len f) -' 1)) - 1 is V33() V34() ext-real set
1 + (len (mid (f,((len f) -' 1),(len f)))) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(1 + (len (mid (f,((len f) -' 1),(len f))))) - 1 is V33() V34() ext-real set
len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) is V40() len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ) } is set
dom ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V40() Element of bool NAT
rng ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) is V40() set
Y is Element of the carrier of (Group_of_Perm 2)
X is Element of the carrier of (Group_of_Perm 2)
<*X*> is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of (Group_of_Perm 2)
1 -tuples_on the carrier of (Group_of_Perm 2) is functional non empty FinSequence-membered FinSequenceSet of the carrier of (Group_of_Perm 2)
the carrier of (Group_of_Perm 2) * is functional non empty FinSequence-membered FinSequenceSet of the carrier of (Group_of_Perm 2)
{ b₁ where b₁ is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of (Group_of_Perm 2) * : len b₁ = 1 } is set
[1,X] is set
{1,X} is V40() set
{{1,X},{1}} is V40() V44() set
{[1,X]} is Function-like non empty trivial V40() 1 -element set
Product <*X*> is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" <*X*> is Element of the carrier of (Group_of_Perm 2)
(len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f)))) is V33() V34() ext-real set
((len (mid (f,((len f) -' 1),(len f)))) - (len (mid (f,((len f) -' 1),(len f))))) + 1 is V33() V34() ext-real set
(mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) . 1 is set
(mid (f,((len f) -' 1),(len f))) . ((1 + (len (mid (f,((len f) -' 1),(len f))))) -' 1) is set
len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len (mid (f,((len f) -' 1),(len f)))) -' (len (mid (f,((len f) -' 1),(len f))))) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
Seg (len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) is V40() len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) ) } is set
dom (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V40() Element of bool NAT
rng (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is V40() set
F is Element of the carrier of (Group_of_Perm 2)
B is Element of the carrier of (Group_of_Perm 2)
<*B*> is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of (Group_of_Perm 2)
[1,B] is set
{1,B} is V40() set
{{1,B},{1}} is V40() V44() set
{[1,B]} is Function-like non empty trivial V40() 1 -element set
Product <*B*> is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" <*B*> is Element of the carrier of (Group_of_Perm 2)
((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)) ^ (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))) * (Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f))))))) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) . ((Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))) is Element of the carrier of (Group_of_Perm 2)
[(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))] is set
{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))} is V40() set
{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)))} is non empty trivial V40() 1 -element set
{{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))},{(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1)))}} is V40() V44() set
the multF of (Group_of_Perm 2) . [(Product ((mid (f,((len f) -' 1),(len f))) | ((len (mid (f,((len f) -' 1),(len f)))) -' 1))),(Product (mid ((mid (f,((len f) -' 1),(len f))),(len (mid (f,((len f) -' 1),(len f)))),(len (mid (f,((len f) -' 1),(len f)))))))] is set
I is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
G0 is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
f is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" f is Element of the carrier of (Group_of_Perm 2)
2 * 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom f is V40() Element of bool NAT
Product f is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" f is Element of the carrier of (Group_of_Perm 2)
1_ (Group_of_Perm 2) is non being_of_order_0 Element of the carrier of (Group_of_Perm 2)
<*> the carrier of (Group_of_Perm 2) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of (Group_of_Perm 2)
[:NAT, the carrier of (Group_of_Perm 2):] is non empty non trivial V40() set
A is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom A is V40() Element of bool NAT
Product A is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" A is Element of the carrier of (Group_of_Perm 2)
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
2 * A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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
f is Relation-like NAT -defined the carrier of A * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of 2,2, the carrier of A
Det f is Element of the carrier of A
f * (1,1) is Element of the carrier of A
f * (2,2) is Element of the carrier of A
(f * (1,1)) * (f * (2,2)) is Element of the carrier of A
the multF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
[: the carrier of A, the carrier of A:] is non empty set
[:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty set
bool [:[: the carrier of A, the carrier of A:], the carrier of A:] is non empty cup-closed diff-closed preBoolean set
the multF of A . ((f * (1,1)),(f * (2,2))) is Element of the carrier of A
[(f * (1,1)),(f * (2,2))] is set
{(f * (1,1)),(f * (2,2))} is V40() set
{(f * (1,1))} is non empty trivial V40() 1 -element set
{{(f * (1,1)),(f * (2,2))},{(f * (1,1))}} is V40() V44() set
the multF of A . [(f * (1,1)),(f * (2,2))] is set
f * (1,2) is Element of the carrier of A
f * (2,1) is Element of the carrier of A
(f * (1,2)) * (f * (2,1)) is Element of the carrier of A
the multF of A . ((f * (1,2)),(f * (2,1))) is Element of the carrier of A
[(f * (1,2)),(f * (2,1))] is set
{(f * (1,2)),(f * (2,1))} is V40() set
{(f * (1,2))} is non empty trivial V40() 1 -element set
{{(f * (1,2)),(f * (2,1))},{(f * (1,2))}} is V40() V44() set
the multF of A . [(f * (1,2)),(f * (2,1))] is set
((f * (1,1)) * (f * (2,2))) - ((f * (1,2)) * (f * (2,1))) is Element of the carrier of A
- ((f * (1,2)) * (f * (2,1))) is Element of the carrier of A
((f * (1,1)) * (f * (2,2))) + (- ((f * (1,2)) * (f * (2,1)))) is Element of the carrier of A
the addF of A is Relation-like [: the carrier of A, the carrier of A:] -defined the carrier of A -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of A, the carrier of A:], the carrier of A:]
the addF of A . (((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))) is Element of the carrier of A
[((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))] is set
{((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))} is V40() set
{((f * (1,1)) * (f * (2,2)))} is non empty trivial V40() 1 -element set
{{((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))},{((f * (1,1)) * (f * (2,2)))}} is V40() V44() set
the addF of A . [((f * (1,1)) * (f * (2,2))),(- ((f * (1,2)) * (f * (2,1))))] is set
n is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective V40() Element of bool [:(Seg 2),(Seg 2):]
n . 1 is set
K is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty total quasi_total onto bijective V40() Element of bool [:(Seg 2),(Seg 2):]
{n,K} is functional V40() V44() set
<*> {n,K} is Relation-like NAT -defined {n,K} -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of {n,K}
Path_product f is Relation-like Permutations 2 -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:(Permutations 2), the carrier of A:]
[:(Permutations 2), the carrier of A:] is non empty set
bool [:(Permutations 2), the carrier of A:] is non empty cup-closed diff-closed preBoolean set
X is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
Path_matrix (X,f) is Relation-like NAT -defined the carrier of A -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of A
the multF of A "**" (Path_matrix (X,f)) is Element of the carrier of A
FinOmega (Permutations 2) is V40() Element of Fin (Permutations 2)
Fin (Permutations 2) is non empty cup-closed diff-closed preBoolean set
the addF of A $$ ((FinOmega (Permutations 2)),(Path_product f)) is Element of the carrier of A
[:(Fin (Permutations 2)), the carrier of A:] is non empty set
bool [:(Fin (Permutations 2)), the carrier of A:] is non empty cup-closed diff-closed preBoolean set
s is Relation-like Fin (Permutations 2) -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:(Fin (Permutations 2)), the carrier of A:]
s . (FinOmega (Permutations 2)) is Element of the carrier of A
s . {} is set
{X} is functional non empty trivial V40() V44() 1 -element set
s . {X} is set
(Path_product f) . X is Element of the carrier of A
B is Relation-like Seg (len (Permutations 2)) -defined Seg (len (Permutations 2)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations 2
(Path_product f) . B is Element of the carrier of A
the addF of A . (((Path_product f) . X),((Path_product f) . B)) is Element of the carrier of A
[((Path_product f) . X),((Path_product f) . B)] is set
{((Path_product f) . X),((Path_product f) . B)} is V40() set
{((Path_product f) . X)} is non empty trivial V40() 1 -element set
{{((Path_product f) . X),((Path_product f) . B)},{((Path_product f) . X)}} is V40() V44() set
the addF of A . [((Path_product f) . X),((Path_product f) . B)] is set
{.X.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations 2)
x is V40() Element of Fin (Permutations 2)
px is set
(FinOmega (Permutations 2)) \ x is V40() Element of Fin (Permutations 2)
{K} is functional non empty trivial V40() V44() 1 -element set
{B} is functional non empty trivial V40() V44() 1 -element set
x \/ {B} is V40() set
s . (x \/ {B}) is set
s . x is Element of the carrier of A
the addF of A . ((s . x),((Path_product f) . B)) is Element of the carrier of A
[(s . x),((Path_product f) . B)] is set
{(s . x),((Path_product f) . B)} is V40() set
{(s . x)} is non empty trivial V40() 1 -element set
{{(s . x),((Path_product f) . B)},{(s . x)}} is V40() V44() set
the addF of A . [(s . x),((Path_product f) . B)] is set
Path_matrix (B,f) is Relation-like NAT -defined the carrier of A -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of A
the multF of A "**" (Path_matrix (B,f)) is Element of the carrier of A
X . 2 is set
B . 2 is set
len (Path_matrix (X,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
[:NAT, the carrier of A:] is non empty non trivial V40() set
bool [:NAT, the carrier of A:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
(Path_matrix (X,f)) . 1 is set
px is Relation-like NAT -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of A:]
px . 1 is Element of the carrier of A
px . 2 is Element of the carrier of A
dom (Path_matrix (X,f)) is V40() Element of bool NAT
X . 1 is set
(Path_matrix (X,f)) . 2 is set
len (Path_matrix (B,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Path_matrix (B,f)) . 1 is set
y is Relation-like NAT -defined the carrier of A -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of A:]
y . 1 is Element of the carrier of A
y . 2 is Element of the carrier of A
dom (Path_matrix (B,f)) is V40() Element of bool NAT
B . 1 is set
(Path_matrix (B,f)) . 2 is set
1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . (1 + 1) is Element of the carrier of A
(Path_matrix (B,f)) . (1 + 1) is set
the multF of A . ((y . 1),((Path_matrix (B,f)) . (1 + 1))) is set
[(y . 1),((Path_matrix (B,f)) . (1 + 1))] is set
{(y . 1),((Path_matrix (B,f)) . (1 + 1))} is V40() set
{(y . 1)} is non empty trivial V40() 1 -element set
{{(y . 1),((Path_matrix (B,f)) . (1 + 1))},{(y . 1)}} is V40() V44() set
the multF of A . [(y . 1),((Path_matrix (B,f)) . (1 + 1))] is set
pd is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len pd) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product pd is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) is Relation-like [: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] -defined the carrier of (Group_of_Perm 2) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm 2)) associative Element of bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):]
[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] is non empty set
[:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty set
bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 2) "**" pd is Element of the carrier of (Group_of_Perm 2)
dom pd is V40() Element of bool NAT
- (( the multF of A "**" (Path_matrix (B,f))),B) is Element of the carrier of A
- ( the multF of A "**" (Path_matrix (B,f))) is Element of the carrier of A
F is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
Product F is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) is Relation-like [: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] -defined the carrier of (Group_of_Perm 2) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm 2)) associative Element of bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):]
[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):] is non empty set
[:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty set
bool [:[: the carrier of (Group_of_Perm 2), the carrier of (Group_of_Perm 2):], the carrier of (Group_of_Perm 2):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm 2) "**" F is Element of the carrier of (Group_of_Perm 2)
<*> the carrier of (Group_of_Perm 2) is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of (Group_of_Perm 2)
[:NAT, the carrier of (Group_of_Perm 2):] is non empty non trivial V40() set
Product (<*> the carrier of (Group_of_Perm 2)) is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" (<*> the carrier of (Group_of_Perm 2)) is Element of the carrier of (Group_of_Perm 2)
1_ (Group_of_Perm 2) is non being_of_order_0 Element of the carrier of (Group_of_Perm 2)
0 mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len F is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len F) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom F is V40() Element of bool NAT
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
F . pd is set
- (( the multF of A "**" (Path_matrix (X,f))),X) is Element of the carrier of A
pd is Relation-like NAT -defined the carrier of (Group_of_Perm 2) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm 2)
len pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len pd) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product pd is Element of the carrier of (Group_of_Perm 2)
the multF of (Group_of_Perm 2) "**" pd is Element of the carrier of (Group_of_Perm 2)
dom pd is V40() Element of bool NAT
px . (1 + 1) is Element of the carrier of A
(Path_matrix (X,f)) . (1 + 1) is set
the multF of A . ((px . 1),((Path_matrix (X,f)) . (1 + 1))) is set
[(px . 1),((Path_matrix (X,f)) . (1 + 1))] is set
{(px . 1),((Path_matrix (X,f)) . (1 + 1))} is V40() set
{(px . 1)} is non empty trivial V40() 1 -element set
{{(px . 1),((Path_matrix (X,f)) . (1 + 1))},{(px . 1)}} is V40() V44() set
the multF of A . [(px . 1),((Path_matrix (X,f)) . (1 + 1))] is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
A is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
f is Element of the carrier of K
f * A is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
width (f * A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
width A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (f * A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (f * A)) is V40() len (f * A) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (f * A) ) } is set
rng (f * A) is V40() set
f2 is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (f * A) is V40() Element of bool NAT
F is set
(f * A) . F is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
0. (n,K,A) is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,A, the carrier of n
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
len (0. (n,K,A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (0. (n,K,A)) is V40() Element of bool NAT
Seg K is V40() K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= K ) } is set
A -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = A } is set
0. n is V59(n) Element of the carrier of n
A |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() A -element FinSequence-like FinSubsequence-like Element of A -tuples_on the carrier of n
Seg A is V40() A -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
(Seg A) --> (0. n) is Relation-like Seg A -defined {(0. n)} -valued Function-like total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg A),{(0. n)}:]
{(0. n)} is non empty trivial V40() 1 -element set
[:(Seg A),{(0. n)}:] is V40() set
bool [:(Seg A),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
K |-> (A |-> (0. n)) is Relation-like NAT -defined A -tuples_on the carrier of n -valued Function-like V40() K -element FinSequence-like FinSubsequence-like Element of K -tuples_on (A -tuples_on the carrier of n)
K -tuples_on (A -tuples_on the carrier of n) is functional non empty FinSequence-membered FinSequenceSet of A -tuples_on the carrier of n
(A -tuples_on the carrier of n) * is functional non empty FinSequence-membered FinSequenceSet of A -tuples_on the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined A -tuples_on the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of (A -tuples_on the carrier of n) * : len b₁ = K } is set
(Seg K) --> (A |-> (0. n)) is Relation-like Seg K -defined {(A |-> (0. n))} -valued Function-like total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(A |-> (0. n))}:]
{(A |-> (0. n))} is functional non empty trivial V40() V44() 1 -element set
[:(Seg K),{(A |-> (0. n))}:] is V40() set
bool [:(Seg K),{(A |-> (0. n))}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
len (K |-> (A |-> (0. n))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations K is non empty permutational set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations K) ) } is set
Seg K is V40() K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 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 V40() Element of Permutations K
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A . f is set
[:(Seg K),(Seg K):] is V40() set
bool [:(Seg K),(Seg K):] is non empty cup-closed diff-closed preBoolean V40() V44() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
0. n is V59(n) Element of the carrier of n
the carrier of n is non empty non trivial set
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
0. (n,K,K) is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Det (0. (n,K,K)) is Element of the carrier of n
Permutations K is non empty permutational set
FinOmega (Permutations K) is V40() Element of Fin (Permutations K)
Fin (Permutations K) is non empty cup-closed diff-closed preBoolean set
Path_product (0. (n,K,K)) is Relation-like Permutations K -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(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 is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty cup-closed diff-closed preBoolean set
[:(Fin (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:]
X 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:]
X . (FinOmega (Permutations K)) is Element of the carrier of n
X . {} is set
B is Element of the carrier of n
the addF of n . ((0. n),B) is Element of the carrier of n
[(0. n),B] is set
{(0. n),B} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),B},{(0. n)}} is V40() V44() set
the addF of n . [(0. n),B] is set
dom (Path_product (0. (n,K,K))) is set
(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:]
B is set
(Path_product (0. (n,K,K))) . B is set
((Permutations K) --> (0. n)) . B is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 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 having_a_unity commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
I is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
((Permutations K) --> (0. n)) . I is Element of the carrier of n
Path_matrix (I,(0. (n,K,K))) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n "**" (Path_matrix (I,(0. (n,K,K)))) is Element of the carrier of n
- (( the multF of n "**" (Path_matrix (I,(0. (n,K,K))))),I) is Element of the carrier of n
G0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
G0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(G0 + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() G0 + 1 -element FinSequence-like FinSubsequence-like Element of (G0 + 1) -tuples_on the carrier of n
(G0 + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = G0 + 1 } is set
Seg (G0 + 1) is non empty V40() G0 + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= G0 + 1 ) } is set
(Seg (G0 + 1)) --> (0. n) is Relation-like Seg (G0 + 1) -defined {(0. n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg (G0 + 1)),{(0. n)}:]
{(0. n)} is non empty trivial V40() 1 -element set
[:(Seg (G0 + 1)),{(0. n)}:] is non empty V40() set
bool [:(Seg (G0 + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" ((G0 + 1) |-> (0. n)) is Element of the carrier of n
(G0 + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((G0 + 1) + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() (G0 + 1) + 1 -element FinSequence-like FinSubsequence-like Element of ((G0 + 1) + 1) -tuples_on the carrier of n
((G0 + 1) + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = (G0 + 1) + 1 } is set
Seg ((G0 + 1) + 1) is non empty V40() (G0 + 1) + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (G0 + 1) + 1 ) } is set
(Seg ((G0 + 1) + 1)) --> (0. n) is Relation-like Seg ((G0 + 1) + 1) -defined {(0. n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg ((G0 + 1) + 1)),{(0. n)}:]
[:(Seg ((G0 + 1) + 1)),{(0. n)}:] is non empty V40() set
bool [:(Seg ((G0 + 1) + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" (((G0 + 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 V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,(0. n)] is set
{1,(0. n)} is V40() set
{{1,(0. n)},{1}} is V40() V44() set
{[1,(0. n)]} is Function-like non empty trivial V40() 1 -element set
((G0 + 1) |-> (0. n)) ^ <*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() (G0 + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(G0 + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal 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
[(0. n),(0. n)] is set
{(0. n),(0. n)} is V40() set
{{(0. n),(0. n)},{(0. n)}} is V40() V44() set
the multF of n . [(0. n),(0. n)] is set
1 |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
(Seg 1) --> (0. n) is Relation-like Seg 1 -defined {(0. n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{(0. n)}:]
{(0. n)} is non empty trivial V40() 1 -element set
[:(Seg 1),{(0. n)}:] is non empty V40() set
bool [:(Seg 1),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
<*(0. n)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,(0. n)] is set
{1,(0. n)} is V40() set
{{1,(0. n)},{1}} is V40() V44() set
{[1,(0. n)]} is Function-like non empty trivial V40() 1 -element set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(0 + 1) |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() 0 + 1 -element FinSequence-like FinSubsequence-like Element of (0 + 1) -tuples_on the carrier of n
(0 + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 0 + 1 } is set
Seg (0 + 1) is non empty V40() 0 + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 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 V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg (0 + 1)),{(0. n)}:]
[:(Seg (0 + 1)),{(0. n)}:] is non empty V40() set
bool [:(Seg (0 + 1)),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" ((0 + 1) |-> (0. n)) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- (0. n) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
K |-> (0. n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n
K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = K } is set
Seg K is V40() K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= K ) } is set
(Seg K) --> (0. n) is Relation-like Seg K -defined {(0. n)} -valued Function-like total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(0. n)}:]
[:(Seg K),{(0. n)}:] is V40() set
bool [:(Seg K),{(0. n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
dom (K |-> (0. n)) is V40() K -element Element of bool NAT
G0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
I . G0 is set
(K |-> (0. n)) . G0 is set
G1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(0. (n,K,K)) * (G0,G1) is Element of the carrier of n
width (0. (n,K,K)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (width (0. (n,K,K))) is V40() width (0. (n,K,K)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= width (0. (n,K,K)) ) } is set
dom (0. (n,K,K)) is V40() Element of bool NAT
[G0,G1] is set
{G0,G1} is V40() V44() set
{G0} is non empty trivial V40() V44() 1 -element set
{{G0,G1},{G0}} is V40() V44() set
Indices (0. (n,K,K)) is set
[:(dom (0. (n,K,K))),(Seg (width (0. (n,K,K)))):] is V40() set
len (K |-> (0. n)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K - 1 is V33() V34() ext-real set
(K -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
dom ((Permutations K) --> (0. n)) is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations K) ) } is set
B is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{B} is functional non empty trivial V40() V44() 1 -element set
X . {B} is set
(Path_product (0. (n,K,K))) . B is Element of the carrier of n
{.B.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
X . {.B.} is Element of the carrier of n
B is V40() Element of Fin (Permutations K)
(FinOmega (Permutations K)) \ B is V40() Element of Fin (Permutations K)
X . B is Element of the carrier of n
I is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{I} is functional non empty trivial V40() V44() 1 -element set
B \/ {I} is V40() set
X . (B \/ {I}) is set
(Path_product (0. (n,K,K))) . I is Element of the carrier of n
the addF of n . ((X . B),((Path_product (0. (n,K,K))) . I)) is Element of the carrier of n
[(X . B),((Path_product (0. (n,K,K))) . I)] is set
{(X . B),((Path_product (0. (n,K,K))) . I)} is V40() set
{(X . B)} is non empty trivial V40() 1 -element set
{{(X . B),((Path_product (0. (n,K,K))) . I)},{(X . B)}} is V40() V44() set
the addF of n . [(X . B),((Path_product (0. (n,K,K))) . I)] is set
{.I.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B \/ {.I.} is V40() Element of Fin (Permutations K)
X . (B \/ {.I.}) is Element of the carrier of n
the addF of n $$ ((FinOmega (Permutations K)),(Path_product (0. (n,K,K)))) is Element of the carrier of n
n is set
K is set
A is set
f is set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
1_ n is Element of the carrier of n
the carrier of n is non empty non trivial set
1. n is V59(n) Element of the carrier of n
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
1. (n,K) is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
Det (1. (n,K)) is Element of the carrier of n
idseq K is Relation-like NAT -defined Function-like V40() K -element FinSequence-like FinSubsequence-like set
Seg K is V40() K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= K ) } is set
id (Seg K) is Relation-like Seg K -defined Seg K -valued Function-like one-to-one total quasi_total onto bijective V40() V112() V114() V115() V119() Element of bool [:(Seg K),(Seg K):]
[:(Seg K),(Seg K):] is V40() set
bool [:(Seg K),(Seg K):] is non empty cup-closed diff-closed preBoolean V40() V44() set
0. n is V59(n) Element of the carrier of n
Permutations K is non empty permutational set
f2 is set
IFEQ ((idseq K),f2,(1_ n),(0. n)) is Element of 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
f2 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:]
f2 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:]
Path_product (1. (n,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:]
dom (Path_product (1. (n,K))) is set
F is set
(Path_product (1. (n,K))) . F is set
f2 . F is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 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 having_a_unity 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
Y is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
f2 . Y is Element of the carrier of n
Path_matrix (Y,(1. (n,K))) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n "**" (Path_matrix (Y,(1. (n,K)))) is Element of the carrier of n
- (( the multF of n "**" (Path_matrix (Y,(1. (n,K))))),Y) is Element of the carrier of n
X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
X + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(X + 1) |-> (1_ n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() X + 1 -element FinSequence-like FinSubsequence-like Element of (X + 1) -tuples_on the carrier of n
(X + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = X + 1 } is set
Seg (X + 1) is non empty V40() X + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= X + 1 ) } is set
(Seg (X + 1)) --> (1_ n) is Relation-like Seg (X + 1) -defined {(1_ n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg (X + 1)),{(1_ n)}:]
{(1_ n)} is non empty trivial V40() 1 -element set
[:(Seg (X + 1)),{(1_ n)}:] is non empty V40() set
bool [:(Seg (X + 1)),{(1_ n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" ((X + 1) |-> (1_ n)) is Element of the carrier of n
(X + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
((X + 1) + 1) |-> (1_ n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() (X + 1) + 1 -element FinSequence-like FinSubsequence-like Element of ((X + 1) + 1) -tuples_on the carrier of n
((X + 1) + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = (X + 1) + 1 } is set
Seg ((X + 1) + 1) is non empty V40() (X + 1) + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= (X + 1) + 1 ) } is set
(Seg ((X + 1) + 1)) --> (1_ n) is Relation-like Seg ((X + 1) + 1) -defined {(1_ n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg ((X + 1) + 1)),{(1_ n)}:]
[:(Seg ((X + 1) + 1)),{(1_ n)}:] is non empty V40() set
bool [:(Seg ((X + 1) + 1)),{(1_ n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" (((X + 1) + 1) |-> (1_ n)) is Element of the carrier of n
<*(1_ n)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,(1_ n)] is set
{1,(1_ n)} is V40() set
{{1,(1_ n)},{1}} is V40() V44() set
{[1,(1_ n)]} is Function-like non empty trivial V40() 1 -element set
((X + 1) |-> (1_ n)) ^ <*(1_ n)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() (X + 1) + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(X + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1_ n) * (1_ n) is Element of the carrier of n
the multF of n . ((1_ n),(1_ n)) is Element of the carrier of n
[(1_ n),(1_ n)] is set
{(1_ n),(1_ n)} is V40() set
{{(1_ n),(1_ n)},{(1_ n)}} is V40() V44() set
the multF of n . [(1_ n),(1_ n)] is set
- ((0. n),Y) is Element of the carrier of n
- ((0. n),Y) is Element of the carrier of n
- (0. n) is Element of the carrier of n
- ((0. n),Y) is Element of the carrier of n
- ((0. n),Y) is Element of the carrier of n
K -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K - 1 is V33() V34() ext-real set
(K -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
1 |-> (1_ n) is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
(Seg 1) --> (1_ n) is Relation-like Seg 1 -defined {(1_ n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg 1),{(1_ n)}:]
{(1_ n)} is non empty trivial V40() 1 -element set
[:(Seg 1),{(1_ n)}:] is non empty V40() set
bool [:(Seg 1),{(1_ n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
<*(1_ n)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,(1_ n)] is set
{1,(1_ n)} is V40() set
{{1,(1_ n)},{1}} is V40() V44() set
{[1,(1_ n)]} is Function-like non empty trivial V40() 1 -element set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(0 + 1) |-> (1_ n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() 0 + 1 -element FinSequence-like FinSubsequence-like Element of (0 + 1) -tuples_on the carrier of n
(0 + 1) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 0 + 1 } is set
Seg (0 + 1) is non empty V40() 0 + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= 0 + 1 ) } is set
(Seg (0 + 1)) --> (1_ n) is Relation-like Seg (0 + 1) -defined {(1_ n)} -valued Function-like non empty total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg (0 + 1)),{(1_ n)}:]
[:(Seg (0 + 1)),{(1_ n)}:] is non empty V40() set
bool [:(Seg (0 + 1)),{(1_ n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
the multF of n "**" ((0 + 1) |-> (1_ n)) is Element of the carrier of n
K |-> (1_ n) is Relation-like NAT -defined the carrier of n -valued Function-like V40() K -element FinSequence-like FinSubsequence-like Element of K -tuples_on the carrier of n
K -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = K } is set
(Seg K) --> (1_ n) is Relation-like Seg K -defined {(1_ n)} -valued Function-like total quasi_total V40() FinSequence-like FinSubsequence-like Element of bool [:(Seg K),{(1_ n)}:]
[:(Seg K),{(1_ n)}:] is V40() set
bool [:(Seg K),{(1_ n)}:] is non empty cup-closed diff-closed preBoolean V40() V44() set
len (K |-> (1_ n)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
the multF of n "**" (K |-> (1_ n)) is Element of the carrier of n
dom (K |-> (1_ n)) is V40() K -element Element of bool NAT
Indices (1. (n,K)) is set
dom (1. (n,K)) is V40() Element of bool NAT
width (1. (n,K)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (width (1. (n,K))) is V40() width (1. (n,K)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= width (1. (n,K)) ) } is set
[:(dom (1. (n,K))),(Seg (width (1. (n,K)))):] is V40() set
X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Y . X is set
(K |-> (1_ n)) . X is set
B is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(1. (n,K)) * (X,B) is Element of the carrier of n
[X,B] is set
{X,B} is V40() V44() set
{X} is non empty trivial V40() V44() 1 -element set
{{X,B},{X}} is V40() V44() set
IFEQ ((idseq K),Y,(1_ n),(0. n)) is Element of the carrier of n
(Path_matrix (Y,(1. (n,K)))) . 1 is set
rng (Path_matrix (Y,(1. (n,K)))) is V40() set
len (Path_matrix (Y,(1. (n,K)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Path_matrix (Y,(1. (n,K))))) is V40() len (Path_matrix (Y,(1. (n,K)))) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Path_matrix (Y,(1. (n,K)))) ) } is set
dom (Path_matrix (Y,(1. (n,K)))) is V40() Element of bool NAT
B is Element of the carrier of n
<*B*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,B] is set
{1,B} is V40() set
{{1,B},{1}} is V40() V44() set
{[1,B]} is Function-like non empty trivial V40() 1 -element set
I is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
G0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
G0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
I . (G0 + 1) is set
I . G0 is set
(Path_matrix (Y,(1. (n,K)))) . (G0 + 1) is set
the multF of n . ((I . G0),((Path_matrix (Y,(1. (n,K)))) . (G0 + 1))) is set
[(I . G0),((Path_matrix (Y,(1. (n,K)))) . (G0 + 1))] is set
{(I . G0),((Path_matrix (Y,(1. (n,K)))) . (G0 + 1))} is V40() set
{(I . G0)} is non empty trivial V40() 1 -element set
{{(I . G0),((Path_matrix (Y,(1. (n,K)))) . (G0 + 1))},{(I . G0)}} is V40() V44() set
the multF of n . [(I . G0),((Path_matrix (Y,(1. (n,K)))) . (G0 + 1))] is set
dom Y is V40() set
dom (idseq K) is V40() K -element Element of bool NAT
G0 is set
Y . G0 is set
(idseq K) . G0 is set
G1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Y . G1 is set
B3 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
B3 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(B3 + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
e is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len e is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . 1 is set
e is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len e is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . 1 is set
Seg (B3 + 1) is non empty V40() B3 + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= B3 + 1 ) } is set
s is set
e . s is set
x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom e is V40() Element of bool NAT
e . x is set
rng e is V40() set
px is Element of the carrier of n
x is set
px is set
[:NAT, the carrier of n:] is non empty non trivial V40() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
s is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
s is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
(Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1) is set
s . (B3 + 1) is Element of the carrier of n
[(s . (B3 + 1)),((Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1))] is set
{(s . (B3 + 1)),((Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1))} is V40() set
{(s . (B3 + 1))} is non empty trivial V40() 1 -element set
{{(s . (B3 + 1)),((Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1))},{(s . (B3 + 1))}} is V40() V44() set
the multF of n . ((s . (B3 + 1)),((Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1))) is set
the multF of n . [(s . (B3 + 1)),((Path_matrix (Y,(1. (n,K)))) . ((B3 + 1) + 1))] is set
x is Element of the carrier of n
<*x*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,x] is set
{1,x} is V40() set
{{1,x},{1}} is V40() V44() set
{[1,x]} is Function-like non empty trivial V40() 1 -element set
e ^ <*x*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
px is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len <*x*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len e) + (len <*x*>) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
px . (y + 1) is set
px . y is set
(Path_matrix (Y,(1. (n,K)))) . (y + 1) is set
the multF of n . ((px . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))) is set
[(px . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))] is set
{(px . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))} is V40() set
{(px . y)} is non empty trivial V40() 1 -element set
{{(px . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))},{(px . y)}} is V40() V44() set
the multF of n . [(px . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))] is set
Seg (len e) is V40() len e -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len e ) } is set
dom e is V40() Element of bool NAT
e . (y + 1) is set
e . y is set
the multF of n . ((e . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))) is set
[(e . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))] is set
{(e . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))} is V40() set
{(e . y)} is non empty trivial V40() 1 -element set
{{(e . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))},{(e . y)}} is V40() V44() set
the multF of n . [(e . y),((Path_matrix (Y,(1. (n,K)))) . (y + 1))] is set
dom e is V40() Element of bool NAT
px . (B3 + 1) is set
e . (B3 + 1) is set
(y + 1) - (B3 + 1) is V33() V34() ext-real set
<*x*> . ((y + 1) - (B3 + 1)) is set
Seg (len e) is V40() len e -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len e ) } is set
dom e is V40() Element of bool NAT
px . 1 is set
e is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len e is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . 1 is set
s is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
s . 1 is set
K + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(K + 1) - 1 is V33() V34() ext-real set
IFEQ ((idseq K),Y,(1_ n),(0. n)) is Element of the carrier of n
len I is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
I . 1 is set
B3 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len B3 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
B3 . 1 is set
X is non empty set
e is Element of X
B3 . e is set
dom B3 is V40() Element of bool NAT
rng B3 is V40() set
s is Element of the carrier of n
x is Element of the carrier of n
[:X, the carrier of n:] is non empty set
bool [:X, the carrier of n:] is non empty cup-closed diff-closed preBoolean set
[:NAT, the carrier of n:] is non empty non trivial V40() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
e is Relation-like X -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:X, the carrier of n:]
e is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
Indices (1. (n,K)) is set
dom (1. (n,K)) is V40() Element of bool NAT
width (1. (n,K)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (width (1. (n,K))) is V40() width (1. (n,K)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= width (1. (n,K)) ) } is set
[:(dom (1. (n,K))),(Seg (width (1. (n,K)))):] is V40() set
s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
[G1,s] is set
{G1,s} is V40() V44() set
{G1} is non empty trivial V40() V44() 1 -element set
{{G1,s},{G1}} is V40() V44() set
K -' G1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K - G1 is V33() V34() ext-real set
(Path_matrix (Y,(1. (n,K)))) . G1 is set
(1. (n,K)) * (G1,s) is Element of the carrier of n
x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
G1 + x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + x) is Element of the carrier of n
x + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
G1 + (x + 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
e . (G1 + (x + 1)) is Element of the carrier of n
1 + (G1 + x) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(G1 + x) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1) is set
e . ((G1 + x) + 1) is Element of the carrier of n
B3 . ((G1 + x) + 1) is set
B3 . (G1 + x) is set
the multF of n . ((B3 . (G1 + x)),((Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1))) is set
[(B3 . (G1 + x)),((Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1))] is set
{(B3 . (G1 + x)),((Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1))} is V40() set
{(B3 . (G1 + x))} is non empty trivial V40() 1 -element set
{{(B3 . (G1 + x)),((Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1))},{(B3 . (G1 + x))}} is V40() V44() set
the multF of n . [(B3 . (G1 + x)),((Path_matrix (Y,(1. (n,K)))) . ((G1 + x) + 1))] is set
px is Element of the carrier of n
(0. n) * px is Element of the carrier of n
the multF of n . ((0. n),px) is Element of the carrier of n
[(0. n),px] is set
{(0. n),px} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),px},{(0. n)}} is V40() V44() set
the multF of n . [(0. n),px] is set
(G1 + x) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(G1 + x) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(G1 + x) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
e . 1 is Element of the carrier of n
x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
x + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
e . (x + 1) is Element of the carrier of n
e . x is Element of the carrier of n
(Path_matrix (Y,(1. (n,K)))) . (x + 1) is set
the multF of n . ((e . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))) is set
[(e . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))] is set
{(e . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))} is V40() set
{(e . x)} is non empty trivial V40() 1 -element set
{{(e . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))},{(e . x)}} is V40() V44() set
the multF of n . [(e . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))] is set
B3 . (x + 1) is set
B3 . x is set
the multF of n . ((B3 . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))) is set
[(B3 . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))] is set
{(B3 . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))} is V40() set
{(B3 . x)} is non empty trivial V40() 1 -element set
{{(B3 . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))},{(B3 . x)}} is V40() V44() set
the multF of n . [(B3 . x),((Path_matrix (Y,(1. (n,K)))) . (x + 1))] is set
G1 + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + 0) is Element of the carrier of n
G1 -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 -' 1) is Element of the carrier of n
G1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(G1 + 1) - 1 is V33() V34() ext-real set
G1 - 1 is V33() V34() ext-real set
(G1 -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
1 - 1 is V33() V34() ext-real set
e . G1 is Element of the carrier of n
the multF of n . ((e . (G1 -' 1)),((Path_matrix (Y,(1. (n,K)))) . G1)) is set
[(e . (G1 -' 1)),((Path_matrix (Y,(1. (n,K)))) . G1)] is set
{(e . (G1 -' 1)),((Path_matrix (Y,(1. (n,K)))) . G1)} is V40() set
{(e . (G1 -' 1))} is non empty trivial V40() 1 -element set
{{(e . (G1 -' 1)),((Path_matrix (Y,(1. (n,K)))) . G1)},{(e . (G1 -' 1))}} is V40() V44() set
the multF of n . [(e . (G1 -' 1)),((Path_matrix (Y,(1. (n,K)))) . G1)] is set
x is Element of the carrier of n
x * (0. n) is Element of the carrier of n
the multF of n . (x,(0. n)) is Element of the carrier of n
[x,(0. n)] is set
{x,(0. n)} is V40() set
{x} is non empty trivial V40() 1 -element set
{{x,(0. n)},{x}} is V40() V44() set
the multF of n . [x,(0. n)] is set
G1 + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + 0) is Element of the carrier of n
G1 + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + 0) is Element of the carrier of n
G1 + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + 0) is Element of the carrier of n
G1 + (K -' G1) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e . (G1 + (K -' G1)) 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 K) is V40() Element of Fin (Permutations K)
Fin (Permutations K) is non empty cup-closed diff-closed preBoolean set
B is set
((idseq K),B,(1_ n),(0. n)) is set
[:(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
B 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:]
B 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:]
dom f2 is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations K) ) } is set
I is V40() Element of Fin (Permutations K)
(FinOmega (Permutations K)) \ I is V40() Element of Fin (Permutations K)
B . I is Element of the carrier of n
G0 is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{G0} is functional non empty trivial V40() V44() 1 -element set
I \/ {G0} is V40() set
B . (I \/ {G0}) is set
(Path_product (1. (n,K))) . G0 is Element of the carrier of n
the addF of n . ((B . I),((Path_product (1. (n,K))) . G0)) is Element of the carrier of n
[(B . I),((Path_product (1. (n,K))) . G0)] is set
{(B . I),((Path_product (1. (n,K))) . G0)} is V40() set
{(B . I)} is non empty trivial V40() 1 -element set
{{(B . I),((Path_product (1. (n,K))) . G0)},{(B . I)}} is V40() V44() set
the addF of n . [(B . I),((Path_product (1. (n,K))) . G0)] is set
{.G0.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
I \/ {.G0.} is V40() Element of Fin (Permutations K)
((idseq K),(I \/ {.G0.}),(1_ n),(0. n)) is set
((idseq K),I,(1_ n),(0. n)) is set
IFEQ ((idseq K),G0,(1_ n),(0. n)) is Element of the carrier of n
I is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{I} is functional non empty trivial V40() V44() 1 -element set
B . {I} is set
(Path_product (1. (n,K))) . I is Element of the carrier of n
((idseq K),{I},(1_ n),(0. n)) is set
f2 . I is Element of the carrier of n
IFEQ ((idseq K),I,(1_ n),(0. n)) is Element of the carrier of n
{.I.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B . {.I.} is Element of the carrier of n
((idseq K),{I},(1_ n),(0. n)) is set
f2 . I is Element of the carrier of n
IFEQ ((idseq K),I,(1_ n),(0. n)) is Element of the carrier of n
{.I.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B . {.I.} is Element of the carrier of n
{.I.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B . {.I.} is Element of the carrier of n
f2 . I is Element of the carrier of n
{.I.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B . {.I.} is Element of the carrier of n
f2 . I is Element of the carrier of n
B . {} is set
I is Element of the carrier of n
the addF of n . ((0. n),I) is Element of the carrier of n
[(0. n),I] is set
{(0. n),I} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),I},{(0. n)}} is V40() V44() set
the addF of n . [(0. n),I] is set
((idseq K),{},(1_ n),(0. n)) is set
B . (FinOmega (Permutations K)) is Element of the carrier of n
((idseq K),(FinOmega (Permutations K)),(1_ n),(0. n)) is set
Group_of_Perm K is non empty strict unital Group-like associative multMagma
the carrier of (Group_of_Perm K) is non empty set
the addF of n $$ ((FinOmega (Permutations K)),(Path_product (1. (n,K)))) is Element of the carrier of n
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
A is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
0. K is V59(K) Element of the carrier of K
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
[f,f2] is set
{f,f2} is V40() V44() set
{f} is non empty trivial V40() V44() 1 -element set
{{f,f2},{f}} is V40() V44() set
[:(Seg n),(Seg n):] is V40() set
Indices A is set
dom A is V40() Element of bool NAT
width A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (width A) is V40() width A -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= width A ) } is set
[:(dom A),(Seg (width A)):] is V40() set
A * (f,f2) is Element of the carrier of K
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
[f,f2] is set
{f,f2} is V40() V44() set
{f} is non empty trivial V40() V44() 1 -element set
{{f,f2},{f}} is V40() V44() set
A * (f,f2) is Element of the carrier of K
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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
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 having_a_unity 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
K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is Relation-like NAT -defined the carrier of n * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of n
Det A is Element of the carrier of n
diagonal_of_Matrix A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n "**" (diagonal_of_Matrix A) is Element of the carrier of n
Permutations K is non empty permutational set
Seg K is V40() K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= K ) } is set
[:(Seg K),(Seg K):] is V40() set
bool [:(Seg K),(Seg K):] is non empty cup-closed diff-closed preBoolean V40() V44() set
idseq K is Relation-like NAT -defined Function-like V40() K -element FinSequence-like FinSubsequence-like set
id (Seg K) is Relation-like Seg K -defined Seg K -valued Function-like one-to-one total quasi_total onto bijective V40() V112() V114() V115() V119() Element of bool [:(Seg K),(Seg K):]
len (diagonal_of_Matrix A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
0. n is V59(n) Element of the carrier of n
X is set
IFEQ ((idseq K),X,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of 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
X 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:]
X 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:]
Y is Relation-like Seg K -defined Seg K -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg K),(Seg K):]
Path_product A 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:]
dom (Path_product A) is set
B is set
(Path_product A) . B is set
X . B is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations K) ) } is set
I is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
X . I is Element of the carrier of n
Path_matrix (I,A) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n "**" (Path_matrix (I,A)) is Element of the carrier of n
- (( the multF of n "**" (Path_matrix (I,A))),I) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- (0. n) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
- ((0. n),I) is Element of the carrier of n
dom (diagonal_of_Matrix A) is V40() Element of bool NAT
G0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
I . G0 is set
(diagonal_of_Matrix A) . G0 is set
G1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
A * (G0,G1) is Element of the carrier of n
IFEQ ((idseq K),I,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of the carrier of n
(Path_matrix (I,A)) . 1 is set
rng (Path_matrix (I,A)) is V40() set
len (Path_matrix (I,A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Path_matrix (I,A))) is V40() len (Path_matrix (I,A)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Path_matrix (I,A)) ) } is set
dom (Path_matrix (I,A)) is V40() Element of bool NAT
G1 is Element of the carrier of n
<*G1*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,G1] is set
{1,G1} is V40() set
{{1,G1},{1}} is V40() V44() set
{[1,G1]} is Function-like non empty trivial V40() 1 -element set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
B3 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
e is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
B3 . (e + 1) is set
B3 . e is set
(Path_matrix (I,A)) . (e + 1) is set
the multF of n . ((B3 . e),((Path_matrix (I,A)) . (e + 1))) is set
[(B3 . e),((Path_matrix (I,A)) . (e + 1))] is set
{(B3 . e),((Path_matrix (I,A)) . (e + 1))} is V40() set
{(B3 . e)} is non empty trivial V40() 1 -element set
{{(B3 . e),((Path_matrix (I,A)) . (e + 1))},{(B3 . e)}} is V40() V44() set
the multF of n . [(B3 . e),((Path_matrix (I,A)) . (e + 1))] is set
e is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
e + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(e + 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
s is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
s . 1 is set
s is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
s . 1 is set
Seg (e + 1) is non empty V40() e + 1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= e + 1 ) } is set
x is set
s . x is set
px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom s is V40() Element of bool NAT
s . px is set
rng s is V40() set
y is Element of the carrier of n
px is set
y is set
[:NAT, the carrier of n:] is non empty non trivial V40() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
x is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
x is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
(Path_matrix (I,A)) . ((e + 1) + 1) is set
x . (e + 1) is Element of the carrier of n
[(x . (e + 1)),((Path_matrix (I,A)) . ((e + 1) + 1))] is set
{(x . (e + 1)),((Path_matrix (I,A)) . ((e + 1) + 1))} is V40() set
{(x . (e + 1))} is non empty trivial V40() 1 -element set
{{(x . (e + 1)),((Path_matrix (I,A)) . ((e + 1) + 1))},{(x . (e + 1))}} is V40() V44() set
the multF of n . ((x . (e + 1)),((Path_matrix (I,A)) . ((e + 1) + 1))) is set
the multF of n . [(x . (e + 1)),((Path_matrix (I,A)) . ((e + 1) + 1))] is set
px is Element of the carrier of n
<*px*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,px] is set
{1,px} is V40() set
{{1,px},{1}} is V40() V44() set
{[1,px]} is Function-like non empty trivial V40() 1 -element set
s ^ <*px*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
y is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len <*px*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len s) + (len <*px*>) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
pd + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . (pd + 1) is set
y . pd is set
(Path_matrix (I,A)) . (pd + 1) is set
the multF of n . ((y . pd),((Path_matrix (I,A)) . (pd + 1))) is set
[(y . pd),((Path_matrix (I,A)) . (pd + 1))] is set
{(y . pd),((Path_matrix (I,A)) . (pd + 1))} is V40() set
{(y . pd)} is non empty trivial V40() 1 -element set
{{(y . pd),((Path_matrix (I,A)) . (pd + 1))},{(y . pd)}} is V40() V44() set
the multF of n . [(y . pd),((Path_matrix (I,A)) . (pd + 1))] is set
Seg (len s) is V40() len s -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len s ) } is set
dom s is V40() Element of bool NAT
s . (pd + 1) is set
s . pd is set
the multF of n . ((s . pd),((Path_matrix (I,A)) . (pd + 1))) is set
[(s . pd),((Path_matrix (I,A)) . (pd + 1))] is set
{(s . pd),((Path_matrix (I,A)) . (pd + 1))} is V40() set
{(s . pd)} is non empty trivial V40() 1 -element set
{{(s . pd),((Path_matrix (I,A)) . (pd + 1))},{(s . pd)}} is V40() V44() set
the multF of n . [(s . pd),((Path_matrix (I,A)) . (pd + 1))] is set
dom s is V40() Element of bool NAT
y . (e + 1) is set
s . (e + 1) is set
(pd + 1) - (e + 1) is V33() V34() ext-real set
<*px*> . ((pd + 1) - (e + 1)) is set
Seg (len s) is V40() len s -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len s ) } is set
dom s is V40() Element of bool NAT
y . 1 is set
s is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
s . 1 is set
x is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
x . 1 is set
IFEQ ((idseq K),I,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of the carrier of n
K + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(K + 1) - 1 is V33() V34() ext-real set
K - 1 is V33() V34() ext-real set
dom I is V40() set
dom (idseq K) is V40() K -element Element of bool NAT
e is set
I . e is set
(idseq K) . e is set
s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
I . s is set
K -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len B3 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
B3 . 1 is set
(K -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
px is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
px . 1 is set
G0 is non empty set
y is Element of G0
px . y is set
dom px is V40() Element of bool NAT
rng px is V40() set
pd is Element of the carrier of n
z is Element of the carrier of n
[:G0, the carrier of n:] is non empty set
bool [:G0, the carrier of n:] is non empty cup-closed diff-closed preBoolean set
[:NAT, the carrier of n:] is non empty non trivial V40() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
y is Relation-like G0 -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:G0, the carrier of n:]
y is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:NAT, the carrier of n:]
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
pd + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . (pd + 1) is Element of the carrier of n
y . pd is Element of the carrier of n
(Path_matrix (I,A)) . (pd + 1) is set
the multF of n . ((y . pd),((Path_matrix (I,A)) . (pd + 1))) is set
[(y . pd),((Path_matrix (I,A)) . (pd + 1))] is set
{(y . pd),((Path_matrix (I,A)) . (pd + 1))} is V40() set
{(y . pd)} is non empty trivial V40() 1 -element set
{{(y . pd),((Path_matrix (I,A)) . (pd + 1))},{(y . pd)}} is V40() V44() set
the multF of n . [(y . pd),((Path_matrix (I,A)) . (pd + 1))] is set
px . (pd + 1) is set
px . pd is set
the multF of n . ((px . pd),((Path_matrix (I,A)) . (pd + 1))) is set
[(px . pd),((Path_matrix (I,A)) . (pd + 1))] is set
{(px . pd),((Path_matrix (I,A)) . (pd + 1))} is V40() set
{(px . pd)} is non empty trivial V40() 1 -element set
{{(px . pd),((Path_matrix (I,A)) . (pd + 1))},{(px . pd)}} is V40() V44() set
the multF of n . [(px . pd),((Path_matrix (I,A)) . (pd + 1))] is set
K -' s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K - s is V33() V34() ext-real set
(Path_matrix (I,A)) . s is set
x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A * (s,x) is Element of the carrier of n
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
s + pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + pd) is Element of the carrier of n
pd + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
s + (pd + 1) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . (s + (pd + 1)) is Element of the carrier of n
1 + (s + pd) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(s + pd) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(Path_matrix (I,A)) . ((s + pd) + 1) is set
y . ((s + pd) + 1) is Element of the carrier of n
px . ((s + pd) + 1) is set
px . (s + pd) is set
the multF of n . ((px . (s + pd)),((Path_matrix (I,A)) . ((s + pd) + 1))) is set
[(px . (s + pd)),((Path_matrix (I,A)) . ((s + pd) + 1))] is set
{(px . (s + pd)),((Path_matrix (I,A)) . ((s + pd) + 1))} is V40() set
{(px . (s + pd))} is non empty trivial V40() 1 -element set
{{(px . (s + pd)),((Path_matrix (I,A)) . ((s + pd) + 1))},{(px . (s + pd))}} is V40() V44() set
the multF of n . [(px . (s + pd)),((Path_matrix (I,A)) . ((s + pd) + 1))] is set
z is Element of the carrier of n
(0. n) * z is Element of the carrier of n
the multF of n . ((0. n),z) is Element of the carrier of n
[(0. n),z] is set
{(0. n),z} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),z},{(0. n)}} is V40() V44() set
the multF of n . [(0. n),z] is set
(s + pd) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(s + pd) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(s + pd) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
y . 1 is Element of the carrier of n
s + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + 0) is Element of the carrier of n
s -' 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s -' 1) is Element of the carrier of n
s + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(s + 1) - 1 is V33() V34() ext-real set
s - 1 is V33() V34() ext-real set
(s -' 1) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
1 - 1 is V33() V34() ext-real set
y . s is Element of the carrier of n
the multF of n . ((y . (s -' 1)),((Path_matrix (I,A)) . s)) is set
[(y . (s -' 1)),((Path_matrix (I,A)) . s)] is set
{(y . (s -' 1)),((Path_matrix (I,A)) . s)} is V40() set
{(y . (s -' 1))} is non empty trivial V40() 1 -element set
{{(y . (s -' 1)),((Path_matrix (I,A)) . s)},{(y . (s -' 1))}} is V40() V44() set
the multF of n . [(y . (s -' 1)),((Path_matrix (I,A)) . s)] is set
pd is Element of the carrier of n
pd * (0. n) is Element of the carrier of n
the multF of n . (pd,(0. n)) is Element of the carrier of n
[pd,(0. n)] is set
{pd,(0. n)} is V40() set
{pd} is non empty trivial V40() 1 -element set
{{pd,(0. n)},{pd}} is V40() V44() set
the multF of n . [pd,(0. n)] is set
s + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + 0) is Element of the carrier of n
s + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + 0) is Element of the carrier of n
s + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + 0) is Element of the carrier of n
s + (K -' s) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
y . (s + (K -' s)) 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 K) is V40() Element of Fin (Permutations K)
Fin (Permutations K) is non empty cup-closed diff-closed preBoolean set
G1 is set
((idseq K),G1,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
[:(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
G1 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:]
G1 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:]
dom X is set
len (Permutations K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations K)) is V40() len (Permutations K) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations K) ) } is set
B3 is V40() Element of Fin (Permutations K)
(FinOmega (Permutations K)) \ B3 is V40() Element of Fin (Permutations K)
G1 . B3 is Element of the carrier of n
e is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{e} is functional non empty trivial V40() V44() 1 -element set
B3 \/ {e} is V40() set
G1 . (B3 \/ {e}) is set
(Path_product A) . e is Element of the carrier of n
the addF of n . ((G1 . B3),((Path_product A) . e)) is Element of the carrier of n
[(G1 . B3),((Path_product A) . e)] is set
{(G1 . B3),((Path_product A) . e)} is V40() set
{(G1 . B3)} is non empty trivial V40() 1 -element set
{{(G1 . B3),((Path_product A) . e)},{(G1 . B3)}} is V40() V44() set
the addF of n . [(G1 . B3),((Path_product A) . e)] is set
{.e.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
B3 \/ {.e.} is V40() Element of Fin (Permutations K)
((idseq K),(B3 \/ {.e.}),( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
((idseq K),B3,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
IFEQ ((idseq K),e,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of the carrier of n
B3 is Relation-like Seg (len (Permutations K)) -defined Seg (len (Permutations K)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations K
{B3} is functional non empty trivial V40() V44() 1 -element set
G1 . {B3} is set
(Path_product A) . B3 is Element of the carrier of n
((idseq K),{B3},( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
X . B3 is Element of the carrier of n
IFEQ ((idseq K),B3,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of the carrier of n
{.B3.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
G1 . {.B3.} is Element of the carrier of n
((idseq K),{B3},( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
X . B3 is Element of the carrier of n
IFEQ ((idseq K),B3,( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is Element of the carrier of n
{.B3.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
G1 . {.B3.} is Element of the carrier of n
{.B3.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
G1 . {.B3.} is Element of the carrier of n
X . B3 is Element of the carrier of n
{.B3.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations K)
G1 . {.B3.} is Element of the carrier of n
X . B3 is Element of the carrier of n
G1 . {} is set
B3 is Element of the carrier of n
the addF of n . ((0. n),B3) is Element of the carrier of n
[(0. n),B3] is set
{(0. n),B3} is V40() set
{(0. n)} is non empty trivial V40() 1 -element set
{{(0. n),B3},{(0. n)}} is V40() V44() set
the addF of n . [(0. n),B3] is set
((idseq K),{},( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
G1 . (FinOmega (Permutations K)) is Element of the carrier of n
((idseq K),(FinOmega (Permutations K)),( the multF of n "**" (diagonal_of_Matrix A)),(0. n)) is set
Group_of_Perm K is non empty strict unital Group-like associative multMagma
the carrier of (Group_of_Perm K) is non empty set
the addF of n $$ ((FinOmega (Permutations K)),(Path_product A)) is Element of the carrier of n
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() 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 V40() Element of bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):]
[:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is V40() set
bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is non empty cup-closed diff-closed preBoolean V40() V44() 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
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
K " is Relation-like Function-like one-to-one set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
A is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
A @ is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K ^ A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (K ^ A) 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 having_a_unity V153( the carrier of n) 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
the multF of n "**" (K ^ A) is Element of the carrier of n
(Product (K ^ A)) " is Element of the carrier of n
Product A is Element of the carrier of n
the multF of n "**" A is Element of the carrier of n
(Product A) " is Element of the carrier of n
Product K is Element of the carrier of n
the multF of n "**" K is Element of the carrier of n
(Product K) " is Element of the carrier of n
((Product A) ") * ((Product K) ") is Element of the carrier of n
the multF of n . (((Product A) "),((Product K) ")) is Element of the carrier of n
[((Product A) "),((Product K) ")] is set
{((Product A) "),((Product K) ")} is V40() set
{((Product A) ")} is non empty trivial V40() 1 -element set
{{((Product A) "),((Product K) ")},{((Product A) ")}} is V40() V44() set
the multF of n . [((Product A) "),((Product K) ")] is set
(Product K) * (Product A) is Element of the carrier of n
the multF of n . ((Product K),(Product A)) is Element of the carrier of n
[(Product K),(Product A)] is set
{(Product K),(Product A)} is V40() set
{(Product K)} is non empty trivial V40() 1 -element set
{{(Product K),(Product A)},{(Product K)}} is V40() V44() set
the multF of n . [(Product K),(Product A)] is set
((Product K) * (Product A)) " is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom K is V40() Element of bool NAT
A is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom A is V40() Element of bool NAT
A is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom A is V40() Element of bool NAT
rng A is V40() set
f is set
f2 is set
A . f2 is set
F is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A . F is set
K /. F is Element of the carrier of n
(K /. F) " is Element of the carrier of n
f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f /. f2 is Element of the carrier of n
K /. f2 is Element of the carrier of n
(K /. f2) " is Element of the carrier of n
A . f2 is set
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom A is V40() Element of bool NAT
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
A . f2 is set
f . f2 is set
Seg (len f) is V40() len f -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
dom f is V40() Element of bool NAT
f /. f2 is Element of the carrier of n
Seg (len A) is V40() len A -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
A /. f2 is Element of the carrier of n
K /. f2 is Element of the carrier of n
(K /. f2) " is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
<*> the carrier of n is Relation-like NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial V40() set
(n,(<*> the carrier of n)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (<*> the carrier of n) is Function-like functional empty V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V44() cardinal {} -element FinSequence-membered Element of NAT
len (n,(<*> the carrier of n)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K ^ A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(K ^ A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,K) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,A) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,K) ^ (n,A) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (n,(K ^ A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (K ^ A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) + (len A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (n,K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len (n,K)) + (len A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (n,A) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len (n,K)) + (len (n,A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len ((n,K) ^ (n,A)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(n,(K ^ A)) . f is set
((n,K) ^ (n,A)) . f is set
dom (n,(K ^ A)) is V40() Element of bool NAT
dom (K ^ A) is V40() Element of bool NAT
Seg (len (n,(K ^ A))) is V40() len (n,(K ^ A)) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (n,(K ^ A)) ) } is set
(n,(K ^ A)) /. f is Element of the carrier of n
(K ^ A) /. f is Element of the carrier of n
((K ^ A) /. f) " is Element of the carrier of n
Seg (len K) is V40() len K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len K ) } is set
dom K is V40() Element of bool NAT
dom (n,K) is V40() Element of bool NAT
(K ^ A) . f is set
K . f is set
K /. f is Element of the carrier of n
(n,K) /. f is Element of the carrier of n
(n,K) . f is set
1 + (len K) is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(1 + (len K)) - (len K) is V33() V34() ext-real set
f - (len K) is V33() V34() ext-real set
f -' (len K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len A) + (len K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len A) + (len K)) - (len K) is V33() V34() ext-real set
Seg (len A) is V40() len A -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len A ) } is set
dom A is V40() Element of bool NAT
dom (n,A) is V40() Element of bool NAT
(K ^ A) . f is set
A . (f - (len K)) is set
A /. (f -' (len K)) is Element of the carrier of n
(n,A) /. (f -' (len K)) is Element of the carrier of n
f - (len (n,K)) is V33() V34() ext-real set
(n,A) . (f - (len (n,K))) is set
<*> the carrier of n is Relation-like NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial V40() set
n is non empty unital Group-like associative multMagma
the carrier of n is non empty 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 V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,K] is set
{1,K} is V40() set
{{1,K},{1}} is V40() V44() set
{[1,K]} is Function-like non empty trivial V40() 1 -element set
(n,<*K*>) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
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 V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,(K ")] is set
{1,(K ")} is V40() set
{{1,(K ")},{1}} is V40() V44() set
{[1,(K ")]} is Function-like non empty trivial V40() 1 -element set
len (n,<*K*>) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len <*K*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
len <*(K ")*> is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(n,<*K*>) . A is set
<*(K ")*> . A is set
Seg (len <*K*>) is non empty V40() len <*K*> -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len <*K*> ) } is set
dom <*K*> is non empty trivial V40() 1 -element Element of bool NAT
Seg (len (n,<*K*>)) is V40() len (n,<*K*>) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (n,<*K*>) ) } is set
dom (n,<*K*>) is V40() Element of bool NAT
(n,<*K*>) /. A is Element of the carrier of n
<*K*> /. A is Element of the carrier of n
(<*K*> /. A) " is Element of the carrier of n
<*K*> . A is set
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
1_ n is non being_of_order_0 Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Rev K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K ^ (n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (K ^ (n,(Rev K))) 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 having_a_unity V153( the carrier of n) 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
the multF of n "**" (K ^ (n,(Rev K))) is Element of the carrier of n
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev f)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f ^ (n,(Rev f)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (f ^ (n,(Rev f))) is Element of the carrier of n
the multF of n "**" (f ^ (n,(Rev f))) is Element of the carrier of n
f | A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Seg A is V40() A -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= A ) } is set
f | (Seg A) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
f2 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f /. (A + 1) is Element of the carrier of n
<*(f /. (A + 1))*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,(f /. (A + 1))] is set
{1,(f /. (A + 1))} is V40() set
{{1,(f /. (A + 1))},{1}} is V40() V44() set
{[1,(f /. (A + 1))]} is Function-like non empty trivial V40() 1 -element set
(n,<*(f /. (A + 1))*>) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) is Element of the carrier of n
the multF of n "**" (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) is Element of the carrier of n
Product <*(f /. (A + 1))*> is Element of the carrier of n
the multF of n "**" <*(f /. (A + 1))*> is Element of the carrier of n
Product (n,<*(f /. (A + 1))*>) is Element of the carrier of n
the multF of n "**" (n,<*(f /. (A + 1))*>) is Element of the carrier of n
(Product <*(f /. (A + 1))*>) * (Product (n,<*(f /. (A + 1))*>)) is Element of the carrier of n
the multF of n . ((Product <*(f /. (A + 1))*>),(Product (n,<*(f /. (A + 1))*>))) is Element of the carrier of n
[(Product <*(f /. (A + 1))*>),(Product (n,<*(f /. (A + 1))*>))] is set
{(Product <*(f /. (A + 1))*>),(Product (n,<*(f /. (A + 1))*>))} is V40() set
{(Product <*(f /. (A + 1))*>)} is non empty trivial V40() 1 -element set
{{(Product <*(f /. (A + 1))*>),(Product (n,<*(f /. (A + 1))*>))},{(Product <*(f /. (A + 1))*>)}} is V40() V44() set
the multF of n . [(Product <*(f /. (A + 1))*>),(Product (n,<*(f /. (A + 1))*>))] is set
(f /. (A + 1)) * (Product (n,<*(f /. (A + 1))*>)) is Element of the carrier of n
the multF of n . ((f /. (A + 1)),(Product (n,<*(f /. (A + 1))*>))) is Element of the carrier of n
[(f /. (A + 1)),(Product (n,<*(f /. (A + 1))*>))] is set
{(f /. (A + 1)),(Product (n,<*(f /. (A + 1))*>))} is V40() set
{(f /. (A + 1))} is non empty trivial V40() 1 -element set
{{(f /. (A + 1)),(Product (n,<*(f /. (A + 1))*>))},{(f /. (A + 1))}} is V40() V44() set
the multF of n . [(f /. (A + 1)),(Product (n,<*(f /. (A + 1))*>))] is set
(f /. (A + 1)) " is Element of the carrier of n
<*((f /. (A + 1)) ")*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
[1,((f /. (A + 1)) ")] is set
{1,((f /. (A + 1)) ")} is V40() set
{{1,((f /. (A + 1)) ")},{1}} is V40() V44() set
{[1,((f /. (A + 1)) ")]} is Function-like non empty trivial V40() 1 -element set
Product <*((f /. (A + 1)) ")*> is Element of the carrier of n
the multF of n "**" <*((f /. (A + 1)) ")*> is Element of the carrier of n
(f /. (A + 1)) * (Product <*((f /. (A + 1)) ")*>) is Element of the carrier of n
the multF of n . ((f /. (A + 1)),(Product <*((f /. (A + 1)) ")*>)) is Element of the carrier of n
[(f /. (A + 1)),(Product <*((f /. (A + 1)) ")*>)] is set
{(f /. (A + 1)),(Product <*((f /. (A + 1)) ")*>)} is V40() set
{{(f /. (A + 1)),(Product <*((f /. (A + 1)) ")*>)},{(f /. (A + 1))}} is V40() V44() set
the multF of n . [(f /. (A + 1)),(Product <*((f /. (A + 1)) ")*>)] is set
(f /. (A + 1)) * ((f /. (A + 1)) ") is Element of the carrier of n
the multF of n . ((f /. (A + 1)),((f /. (A + 1)) ")) is Element of the carrier of n
[(f /. (A + 1)),((f /. (A + 1)) ")] is set
{(f /. (A + 1)),((f /. (A + 1)) ")} is V40() set
{{(f /. (A + 1)),((f /. (A + 1)) ")},{(f /. (A + 1))}} is V40() V44() set
the multF of n . [(f /. (A + 1)),((f /. (A + 1)) ")] is set
f2 ^ <*(f /. (A + 1))*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Rev f2 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*(f /. (A + 1))*> ^ (Rev f2) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev f2)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,<*(f /. (A + 1))*>) ^ (n,(Rev f2)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
<*(f /. (A + 1))*> ^ ((n,<*(f /. (A + 1))*>) ^ (n,(Rev f2))) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f2 ^ (<*(f /. (A + 1))*> ^ ((n,<*(f /. (A + 1))*>) ^ (n,(Rev f2)))) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f2 ^ ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product f2 is Element of the carrier of n
the multF of n "**" f2 is Element of the carrier of n
Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))) is Element of the carrier of n
the multF of n "**" ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))) is Element of the carrier of n
(Product f2) * (Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2)))) is Element of the carrier of n
the multF of n . ((Product f2),(Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))))) is Element of the carrier of n
[(Product f2),(Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))))] is set
{(Product f2),(Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))))} is V40() set
{(Product f2)} is non empty trivial V40() 1 -element set
{{(Product f2),(Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))))},{(Product f2)}} is V40() V44() set
the multF of n . [(Product f2),(Product ((<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)) ^ (n,(Rev f2))))] is set
Product (n,(Rev f2)) is Element of the carrier of n
the multF of n "**" (n,(Rev f2)) is Element of the carrier of n
(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))) is Element of the carrier of n
the multF of n . ((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))),(Product (n,(Rev f2)))) is Element of the carrier of n
[(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))),(Product (n,(Rev f2)))] is set
{(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))),(Product (n,(Rev f2)))} is V40() set
{(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)))} is non empty trivial V40() 1 -element set
{{(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))),(Product (n,(Rev f2)))},{(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>)))}} is V40() V44() set
the multF of n . [(Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))),(Product (n,(Rev f2)))] is set
(Product f2) * ((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2)))) is Element of the carrier of n
the multF of n . ((Product f2),((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))))) is Element of the carrier of n
[(Product f2),((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))))] is set
{(Product f2),((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))))} is V40() set
{{(Product f2),((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))))},{(Product f2)}} is V40() V44() set
the multF of n . [(Product f2),((Product (<*(f /. (A + 1))*> ^ (n,<*(f /. (A + 1))*>))) * (Product (n,(Rev f2))))] is set
(Product f2) * (Product (n,(Rev f2))) is Element of the carrier of n
the multF of n . ((Product f2),(Product (n,(Rev f2)))) is Element of the carrier of n
[(Product f2),(Product (n,(Rev f2)))] is set
{(Product f2),(Product (n,(Rev f2)))} is V40() set
{{(Product f2),(Product (n,(Rev f2)))},{(Product f2)}} is V40() V44() set
the multF of n . [(Product f2),(Product (n,(Rev f2)))] is set
f2 ^ (n,(Rev f2)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (f2 ^ (n,(Rev f2))) is Element of the carrier of n
the multF of n "**" (f2 ^ (n,(Rev f2))) is Element of the carrier of n
f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev f)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f ^ (n,(Rev f)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (f ^ (n,(Rev f))) is Element of the carrier of n
the multF of n "**" (f ^ (n,(Rev f))) is Element of the carrier of n
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A ^ (n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (A ^ (n,(Rev A))) is Element of the carrier of n
the multF of n "**" (A ^ (n,(Rev A))) is Element of the carrier of n
<*> the carrier of n is Relation-like NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial V40() set
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A ^ (n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (A ^ (n,(Rev A))) is Element of the carrier of n
the multF of n "**" (A ^ (n,(Rev A))) is Element of the carrier of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A ^ (n,(Rev A)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (A ^ (n,(Rev A))) is Element of the carrier of n
the multF of n "**" (A ^ (n,(Rev A))) is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
1_ n is non being_of_order_0 Element of the carrier of n
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Rev K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev K)) ^ K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product ((n,(Rev K)) ^ K) 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 having_a_unity V153( the carrier of n) 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
the multF of n "**" ((n,(Rev K)) ^ K) is Element of the carrier of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (Rev K) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Rev (n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (Rev (n,(Rev K))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(n,(Rev (n,(Rev K)))) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (n,(Rev (n,(Rev K)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (Rev (n,(Rev K))) is V40() Element of bool NAT
dom (n,(Rev (n,(Rev K)))) is V40() Element of bool NAT
len (n,(Rev K)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom (Rev K) is V40() Element of bool NAT
dom (n,(Rev K)) is V40() Element of bool NAT
A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
K . A is set
(n,(Rev (n,(Rev K)))) . A is set
(len K) - A is V33() V34() ext-real set
((len K) - A) + 1 is V33() V34() ext-real set
(len K) -' A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len K) -' A) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
A + f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
Seg (len K) is V40() len K -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len K ) } is set
A - 1 is V33() V34() ext-real set
(len K) + 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len K) + (A - 1) is V33() V34() ext-real set
(len K) - (A - 1) is V33() V34() ext-real set
((len K) + (A - 1)) - (A - 1) is V33() V34() ext-real set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
f + A is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom K is V40() Element of bool NAT
K /. A is Element of the carrier of n
(Rev K) /. f is Element of the carrier of n
((Rev K) /. f) " is Element of the carrier of n
(((Rev K) /. f) ") " is Element of the carrier of n
(n,(Rev K)) /. f is Element of the carrier of n
((n,(Rev K)) /. f) " is Element of the carrier of n
(Rev (n,(Rev K))) /. A is Element of the carrier of n
((Rev (n,(Rev K))) /. A) " is Element of the carrier of n
(n,(Rev (n,(Rev K)))) /. A is Element of the carrier of n
n is non empty unital Group-like associative multMagma
the carrier of n is non empty set
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product K 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 having_a_unity V153( the carrier of n) 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
the multF of n "**" K is Element of the carrier of n
(Product K) " is Element of the carrier of n
Rev K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (n,(Rev K)) is Element of the carrier of n
the multF of n "**" (n,(Rev K)) is Element of the carrier of n
K ^ (n,(Rev K)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product (K ^ (n,(Rev K))) is Element of the carrier of n
the multF of n "**" (K ^ (n,(Rev K))) is Element of the carrier of n
1_ n is non being_of_order_0 Element of the carrier of n
(Product K) * (Product (n,(Rev K))) is Element of the carrier of n
the multF of n . ((Product K),(Product (n,(Rev K)))) is Element of the carrier of n
[(Product K),(Product (n,(Rev K)))] is set
{(Product K),(Product (n,(Rev K)))} is V40() set
{(Product K)} is non empty trivial V40() 1 -element set
{{(Product K),(Product (n,(Rev K)))},{(Product K)}} is V40() V44() set
the multF of n . [(Product K),(Product (n,(Rev K)))] is set
(n,(Rev K)) ^ K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Product ((n,(Rev K)) ^ K) is Element of the carrier of n
the multF of n "**" ((n,(Rev K)) ^ K) is Element of the carrier of n
(Product (n,(Rev K))) * (Product K) is Element of the carrier of n
the multF of n . ((Product (n,(Rev K))),(Product K)) is Element of the carrier of n
[(Product (n,(Rev K))),(Product K)] is set
{(Product (n,(Rev K))),(Product K)} is V40() set
{(Product (n,(Rev K)))} is non empty trivial V40() 1 -element set
{{(Product (n,(Rev K))),(Product K)},{(Product (n,(Rev K)))}} is V40() V44() set
the multF of n . [(Product (n,(Rev K))),(Product K)] is set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is 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
K is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
(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 V40() Element of Permutations n
A is Element of the carrier of (Group_of_Perm n)
A " is Element of the carrier of (Group_of_Perm n)
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
f is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
dom f is V40() set
(n,K) * K 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 V40() Element of bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):]
[:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is V40() set
bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):] is non empty cup-closed diff-closed preBoolean V40() V44() set
id (Seg n) is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() V112() V114() V115() V119() Element of bool [:(Seg n),(Seg n):]
rng f is V40() set
K * (n,K) 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 V40() Element of bool [:(Seg (len (Permutations n))),(Seg (len (Permutations n))):]
idseq n is Relation-like NAT -defined Function-like V40() n -element FinSequence-like FinSubsequence-like set
1_ (Group_of_Perm n) is non being_of_order_0 Element of the carrier of (Group_of_Perm n)
f2 is Element of the carrier of (Group_of_Perm n)
A * f2 is Element of the carrier of (Group_of_Perm n)
the multF of (Group_of_Perm n) is Relation-like [: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] -defined the carrier of (Group_of_Perm n) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm n)) associative Element of bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):]
[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] is non empty set
[:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty set
bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm n) . (A,f2) is Element of the carrier of (Group_of_Perm n)
[A,f2] is set
{A,f2} is V40() set
{A} is non empty trivial V40() 1 -element set
{{A,f2},{A}} is V40() V44() set
the multF of (Group_of_Perm n) . [A,f2] is set
f2 * A is Element of the carrier of (Group_of_Perm n)
the multF of (Group_of_Perm n) . (f2,A) is Element of the carrier of (Group_of_Perm n)
[f2,A] is set
{f2,A} is V40() set
{f2} is non empty trivial V40() 1 -element set
{{f2,A},{f2}} is V40() V44() set
the multF of (Group_of_Perm n) . [f2,A] is set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
(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 V40() Element of Permutations n
Group_of_Perm n is non empty strict unital Group-like associative multMagma
the carrier of (Group_of_Perm n) is non empty 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 V40() Element of Permutations n
f2 is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(len f2) mod 2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Product f2 is Element of the carrier of (Group_of_Perm n)
the multF of (Group_of_Perm n) is Relation-like [: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] -defined the carrier of (Group_of_Perm n) -valued Function-like non empty total quasi_total having_a_unity V153( the carrier of (Group_of_Perm n)) associative Element of bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):]
[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):] is non empty set
[:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty set
bool [:[: the carrier of (Group_of_Perm n), the carrier of (Group_of_Perm n):], the carrier of (Group_of_Perm n):] is non empty cup-closed diff-closed preBoolean set
the multF of (Group_of_Perm n) "**" f2 is Element of the carrier of (Group_of_Perm n)
dom f2 is V40() Element of bool NAT
Rev f2 is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
((Group_of_Perm n),(Rev f2)) is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len (Rev f2) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Y is Relation-like NAT -defined the carrier of (Group_of_Perm n) -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of (Group_of_Perm n)
len Y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom Y is V40() Element of bool NAT
X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Y . X is set
dom (Rev f2) is V40() Element of bool NAT
Seg (len Y) is V40() len Y -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len Y ) } is set
(len f2) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
(len f2) + X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len f2) + 1) - X is V33() V34() ext-real set
((len f2) + X) - X is V33() V34() ext-real set
(len f2) - X is V33() V34() ext-real set
((len f2) - X) + 1 is V33() V34() ext-real set
(len f2) -' X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((len f2) -' X) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
I is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len f2) is V40() len f2 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f2 ) } is set
f2 . I is set
G0 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
Y /. X is Element of the carrier of (Group_of_Perm n)
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
G1 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
X + I is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
dom G0 is V40() set
s is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
x is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
G0 . s is set
G0 . x is set
e is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
dom e is V40() set
B3 is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
dom B3 is V40() set
((Group_of_Perm n),(Rev f2)) /. X is Element of the carrier of (Group_of_Perm n)
B is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Rev f2) /. B is Element of the carrier of (Group_of_Perm n)
((Rev f2) /. B) " is Element of the carrier of (Group_of_Perm n)
f2 /. I is Element of the carrier of (Group_of_Perm n)
(f2 /. I) " is Element of the carrier of (Group_of_Perm n)
(n,G0) is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
dom G1 is V40() set
px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
G1 . px is set
G0 . px is set
px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
G1 . px is set
y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
G1 . y is set
pd is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
G1 . pd is set
px is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
G1 . px is set
G1 . y is set
f is Element of the carrier of (Group_of_Perm n)
f " is Element of the carrier of (Group_of_Perm n)
(n,A) is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
Product Y is Element of the carrier of (Group_of_Perm n)
the multF of (Group_of_Perm n) "**" Y is Element of the carrier of (Group_of_Perm n)
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
(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 V40() Element of Permutations n
(n,(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 V40() Element of Permutations n
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
the carrier of K is non empty non trivial 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 V40() Element of Permutations n
(n,A) is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
f is Element of the carrier of K
- (f,A) is Element of the carrier of K
- (f,(n,A)) is Element of the carrier of K
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
f2 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
f2 " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
- f is Element of the carrier of K
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K ^ A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence 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 having_a_unity 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
the multF of n "**" (K ^ A) is Element of the carrier of n
the multF of n "**" K is Element of the carrier of n
the multF of n "**" A is Element of the carrier of n
( the multF of n "**" K) * ( the multF of n "**" A) is Element of the carrier of n
the multF of n . (( the multF of n "**" K),( the multF of n "**" A)) is Element of the carrier of n
[( the multF of n "**" K),( the multF of n "**" A)] is set
{( the multF of n "**" K),( the multF of n "**" A)} is V40() set
{( the multF of n "**" K)} is non empty trivial V40() 1 -element set
{{( the multF of n "**" K),( the multF of n "**" A)},{( the multF of n "**" K)}} is V40() V44() set
the multF of n . [( the multF of n "**" K),( the multF of n "**" A)] is set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 having_a_unity 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
K is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
A is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n "**" K is Element of the carrier of n
the multF of n "**" A is Element of the carrier of n
len K is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
f + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
F is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Y is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len F is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
the multF of n "**" F is Element of the carrier of n
the multF of n "**" Y is Element of the carrier of n
rng F is V40() set
0 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
dom F is V40() Element of bool NAT
F . (f + 1) is set
rng Y is V40() set
X is Element of the carrier of n
dom Y is V40() Element of bool NAT
B is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
Y . B is set
Y | B is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Seg B is V40() B -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= B ) } is set
Y | (Seg B) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
Y /^ B is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(Y | B) ^ (Y /^ B) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B - 1 is V33() V34() ext-real set
max (0,(B - 1)) is V33() V34() ext-real set
(Y | B) . B is set
G1 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
G1 + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real positive non negative V40() cardinal Element of NAT
Seg G1 is V40() G1 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= G1 ) } is set
len Y is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
len (Y | B) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Y | B) | G1 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(Y | B) | (Seg G1) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
<*X*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like Element of 1 -tuples_on the carrier of n
1 -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b₁ where b₁ is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like Element of the carrier of n * : len b₁ = 1 } is set
[1,X] is set
{1,X} is V40() set
{{1,X},{1}} is V40() V44() set
{[1,X]} is Function-like non empty trivial V40() 1 -element set
((Y | B) | G1) ^ <*X*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
F | f2 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Seg f2 is V40() f2 -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= f2 ) } is set
F | (Seg f2) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
(F | f2) ^ <*X*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(Seg B) /\ (Seg G1) is V40() Element of bool NAT
Y | ((Seg B) /\ (Seg G1)) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSubsequence-like Element of bool [:NAT, the carrier of n:]
[:NAT, the carrier of n:] is non empty non trivial V40() set
bool [:NAT, the carrier of n:] is non empty non trivial cup-closed diff-closed preBoolean V40() set
Y | G1 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
Y | (Seg G1) is Relation-like NAT -defined Function-like V40() FinSubsequence-like set
e is set
Coim (F,e) is set
{e} is non empty trivial V40() 1 -element set
F " {e} is V40() set
card (Coim (F,e)) is V26() V27() V28() cardinal set
Coim (Y,e) is set
Y " {e} is V40() set
card (Coim (Y,e)) is V26() V27() V28() cardinal set
(F | f2) " {e} is V40() set
card ((F | f2) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
<*X*> " {e} is V40() set
card (<*X*> " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(card ((F | f2) " {e})) + (card (<*X*> " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Y | G1) ^ <*X*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
((Y | G1) ^ <*X*>) ^ (Y /^ B) is Relation-like NAT -defined the carrier of n -valued Function-like non empty V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(((Y | G1) ^ <*X*>) ^ (Y /^ B)) " {e} is V40() set
card ((((Y | G1) ^ <*X*>) ^ (Y /^ B)) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((Y | G1) ^ <*X*>) " {e} is V40() set
card (((Y | G1) ^ <*X*>) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Y /^ B) " {e} is V40() set
card ((Y /^ B) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(card (((Y | G1) ^ <*X*>) " {e})) + (card ((Y /^ B) " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Y | G1) " {e} is V40() set
card ((Y | G1) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(card ((Y | G1) " {e})) + (card (<*X*> " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((card ((Y | G1) " {e})) + (card (<*X*> " {e}))) + (card ((Y /^ B) " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(card ((Y | G1) " {e})) + (card ((Y /^ B) " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
((card ((Y | G1) " {e})) + (card ((Y /^ B) " {e}))) + (card (<*X*> " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Y | G1) ^ (Y /^ B) is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
((Y | G1) ^ (Y /^ B)) " {e} is V40() set
card (((Y | G1) ^ (Y /^ B)) " {e}) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(card (((Y | G1) ^ (Y /^ B)) " {e})) + (card (<*X*> " {e})) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Coim ((F | f2),e) is set
card (Coim ((F | f2),e)) is V26() V27() V28() cardinal set
Coim (((Y | G1) ^ (Y /^ B)),e) is set
card (Coim (((Y | G1) ^ (Y /^ B)),e)) is V26() V27() V28() cardinal set
len (F | f2) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
the multF of n "**" (F | f2) is Element of the carrier of n
the multF of n "**" ((Y | G1) ^ (Y /^ B)) is Element of the carrier of n
the multF of n "**" <*X*> is Element of the carrier of n
( the multF of n "**" ((Y | G1) ^ (Y /^ B))) * ( the multF of n "**" <*X*>) is Element of the carrier of n
the multF of n . (( the multF of n "**" ((Y | G1) ^ (Y /^ B))),( the multF of n "**" <*X*>)) is Element of the carrier of n
[( the multF of n "**" ((Y | G1) ^ (Y /^ B))),( the multF of n "**" <*X*>)] is set
{( the multF of n "**" ((Y | G1) ^ (Y /^ B))),( the multF of n "**" <*X*>)} is V40() set
{( the multF of n "**" ((Y | G1) ^ (Y /^ B)))} is non empty trivial V40() 1 -element set
{{( the multF of n "**" ((Y | G1) ^ (Y /^ B))),( the multF of n "**" <*X*>)},{( the multF of n "**" ((Y | G1) ^ (Y /^ B)))}} is V40() V44() set
the multF of n . [( the multF of n "**" ((Y | G1) ^ (Y /^ B))),( the multF of n "**" <*X*>)] is set
the multF of n "**" (Y | G1) is Element of the carrier of n
the multF of n "**" (Y /^ B) is Element of the carrier of n
( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B)) is Element of the carrier of n
the multF of n . (( the multF of n "**" (Y | G1)),( the multF of n "**" (Y /^ B))) is Element of the carrier of n
[( the multF of n "**" (Y | G1)),( the multF of n "**" (Y /^ B))] is set
{( the multF of n "**" (Y | G1)),( the multF of n "**" (Y /^ B))} is V40() set
{( the multF of n "**" (Y | G1))} is non empty trivial V40() 1 -element set
{{( the multF of n "**" (Y | G1)),( the multF of n "**" (Y /^ B))},{( the multF of n "**" (Y | G1))}} is V40() V44() set
the multF of n . [( the multF of n "**" (Y | G1)),( the multF of n "**" (Y /^ B))] is set
(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))) * ( the multF of n "**" <*X*>) is Element of the carrier of n
the multF of n . ((( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))),( the multF of n "**" <*X*>)) is Element of the carrier of n
[(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))),( the multF of n "**" <*X*>)] is set
{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))),( the multF of n "**" <*X*>)} is V40() set
{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B)))} is non empty trivial V40() 1 -element set
{{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))),( the multF of n "**" <*X*>)},{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B)))}} is V40() V44() set
the multF of n . [(( the multF of n "**" (Y | G1)) * ( the multF of n "**" (Y /^ B))),( the multF of n "**" <*X*>)] is set
( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>) is Element of the carrier of n
the multF of n . (( the multF of n "**" (Y | G1)),( the multF of n "**" <*X*>)) is Element of the carrier of n
[( the multF of n "**" (Y | G1)),( the multF of n "**" <*X*>)] is set
{( the multF of n "**" (Y | G1)),( the multF of n "**" <*X*>)} is V40() set
{{( the multF of n "**" (Y | G1)),( the multF of n "**" <*X*>)},{( the multF of n "**" (Y | G1))}} is V40() V44() set
the multF of n . [( the multF of n "**" (Y | G1)),( the multF of n "**" <*X*>)] is set
(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)) * ( the multF of n "**" (Y /^ B)) is Element of the carrier of n
the multF of n . ((( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)),( the multF of n "**" (Y /^ B))) is Element of the carrier of n
[(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)),( the multF of n "**" (Y /^ B))] is set
{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)),( the multF of n "**" (Y /^ B))} is V40() set
{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>))} is non empty trivial V40() 1 -element set
{{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)),( the multF of n "**" (Y /^ B))},{(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>))}} is V40() V44() set
the multF of n . [(( the multF of n "**" (Y | G1)) * ( the multF of n "**" <*X*>)),( the multF of n "**" (Y /^ B))] is set
the multF of n "**" (Y | B) is Element of the carrier of n
( the multF of n "**" (Y | B)) * ( the multF of n "**" (Y /^ B)) is Element of the carrier of n
the multF of n . (( the multF of n "**" (Y | B)),( the multF of n "**" (Y /^ B))) is Element of the carrier of n
[( the multF of n "**" (Y | B)),( the multF of n "**" (Y /^ B))] is set
{( the multF of n "**" (Y | B)),( the multF of n "**" (Y /^ B))} is V40() set
{( the multF of n "**" (Y | B))} is non empty trivial V40() 1 -element set
{{( the multF of n "**" (Y | B)),( the multF of n "**" (Y /^ B))},{( the multF of n "**" (Y | B))}} is V40() V44() set
the multF of n . [( the multF of n "**" (Y | B)),( the multF of n "**" (Y /^ B))] is set
f is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
f2 is Relation-like NAT -defined the carrier of n -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
the multF of n "**" f is Element of the carrier of n
the multF of n "**" f2 is Element of the carrier of n
len f2 is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
<*> the carrier of n is Relation-like NAT -defined the carrier of n -valued Function-like one-to-one constant functional empty proper V26() V27() V28() V30() V31() V32() V33() V34() ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered FinSequence of the carrier of n
[:NAT, the carrier of n:] is non empty non trivial V40() set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
the carrier of K is non empty non trivial 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 V40() Element of Permutations n
f is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f2 is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
f * A is Relation-like Seg (len (Permutations n)) -defined the carrier of K -valued Function-like V40() Element of bool [:(Seg (len (Permutations n))), the carrier of K:]
[:(Seg (len (Permutations n))), the carrier of K:] is set
bool [:(Seg (len (Permutations n))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
rng A is V40() set
F is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
rng F is V40() set
dom f is V40() Element of bool NAT
dom (f * A) is V40() set
dom F is V40() set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
f is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f2 is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence 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 V40() Element of Permutations n
f * A is Relation-like Seg (len (Permutations n)) -defined the carrier of K -valued Function-like V40() Element of bool [:(Seg (len (Permutations n))), the carrier of K:]
[:(Seg (len (Permutations n))), the carrier of K:] is set
bool [:(Seg (len (Permutations n))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total having_a_unity 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
the multF of K "**" f is Element of the carrier of K
the multF of K "**" f2 is Element of the carrier of K
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() left_unital doubleLoopStr
the carrier of K is non empty non trivial 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 V40() Element of Permutations n
f is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
f * A is Relation-like Seg (len (Permutations n)) -defined the carrier of K -valued Function-like V40() Element of bool [:(Seg (len (Permutations n))), the carrier of K:]
[:(Seg (len (Permutations n))), the carrier of K:] is set
bool [:(Seg (len (Permutations n))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
f2 is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
rng f2 is V40() set
rng A is V40() set
dom f is V40() Element of bool NAT
dom (f * A) is V40() set
dom f2 is V40() set
F is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like set
rng F is V40() set
rng f is V40() set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
(n,A) is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
f is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
f @ is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
Path_matrix ((n,A),(f @)) is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
Path_matrix (A,f) is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
(Path_matrix (A,f)) * (n,A) is Relation-like Seg (len (Permutations n)) -defined the carrier of K -valued Function-like V40() Element of bool [:(Seg (len (Permutations n))), the carrier of K:]
[:(Seg (len (Permutations n))), the carrier of K:] is set
bool [:(Seg (len (Permutations n))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
F is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
dom F is V40() set
len (Path_matrix (A,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
rng F is V40() set
rng (n,A) is V40() set
dom (Path_matrix (A,f)) is V40() Element of bool NAT
dom ((Path_matrix (A,f)) * (n,A)) is V40() set
X is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom X is V40() Element of bool NAT
B is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(n,A) . B is set
X . B is set
I is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal set
(f @) * (B,I) is Element of the carrier of K
Y is Relation-like Seg n -defined Seg n -valued Function-like total quasi_total V40() Element of bool [:(Seg n),(Seg n):]
rng Y is V40() set
A . I is set
(Path_matrix (A,f)) . I is set
f * (I,B) is Element of the carrier of K
dom f is V40() Element of bool NAT
len f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len f) is V40() len f -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len f ) } is set
width f is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (width f) is V40() width f -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= width f ) } is set
[I,B] is set
{I,B} is V40() V44() set
{I} is non empty trivial V40() V44() 1 -element set
{{I,B},{I}} is V40() V44() set
Indices f is set
[:(dom f),(Seg (width f)):] is V40() set
((Path_matrix (A,f)) * (n,A)) . B is set
(Path_matrix (A,f)) . ((n,A) . B) is set
len X is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Permutations n is non empty permutational set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
(n,A) is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
f is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
f @ is Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
Path_product (f @) 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 (f @)) . (n,A) is Element of the carrier of K
Path_product f 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:]
(Path_product f) . A is Element of the carrier of K
Path_matrix (A,f) is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
len (Path_matrix (A,f)) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
(Path_matrix (A,f)) * (n,A) is Relation-like Seg (len (Permutations n)) -defined the carrier of K -valued Function-like V40() Element of bool [:(Seg (len (Permutations n))), the carrier of K:]
[:(Seg (len (Permutations n))), the carrier of K:] is set
bool [:(Seg (len (Permutations n))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Path_matrix ((n,A),(f @)) is Relation-like NAT -defined the carrier of K -valued Function-like V40() 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 having_a_unity 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
the multF of K "**" (Path_matrix ((n,A),(f @))) is Element of the carrier of K
- (( the multF of K "**" (Path_matrix ((n,A),(f @)))),(n,A)) is Element of the carrier of K
f2 is Relation-like NAT -defined the carrier of K -valued Function-like V40() FinSequence-like FinSubsequence-like FinSequence of the carrier of K
the multF of K "**" f2 is Element of the carrier of K
- (( the multF of K "**" f2),(n,A)) is Element of the carrier of K
- (( the multF of K "**" f2),A) is Element of the carrier of K
the multF of K "**" (Path_matrix (A,f)) is Element of the carrier of K
- (( the multF of K "**" (Path_matrix (A,f))),A) is Element of the carrier of K
n is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
K is non empty non degenerated non trivial right_complementable almost_left_invertible V102() unital associative commutative V155() V156() V157() right-distributive left-distributive right_unital well-unital V169() 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 Relation-like NAT -defined the carrier of K * -valued Function-like V40() FinSequence-like FinSubsequence-like tabular Matrix of n,n, the carrier of K
Det A is Element of the carrier of K
A @ is Relation-like NAT -defined the carrier of K * -valued Function-like V40() 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
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:]
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 V40() 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
the addF of K $$ ((FinOmega (Permutations n)),(Path_product A)) is Element of the carrier of K
Seg n is V40() n -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= n ) } is set
[:(Seg n),(Seg n):] is V40() set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean V40() V44() set
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in FinOmega (Permutations n) } is set
G0 is set
G1 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
G1 " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
G0 is set
G1 is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
G1 " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
(G1 ") " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
[:(Fin (Permutations n)), the carrier of K:] is non empty set
bool [:(Fin (Permutations n)), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
len (Permutations n) is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT
Seg (len (Permutations n)) is V40() len (Permutations n) -element Element of bool NAT
{ b₁ where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V40() cardinal Element of NAT : ( 1 <= b₁ & b₁ <= len (Permutations n) ) } is set
G0 is Relation-like Fin (Permutations n) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (Permutations n)), the carrier of K:]
G0 . (FinOmega (Permutations n)) is Element of the carrier of K
G0 . {} is set
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in a₁ } is set
G0 . { (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in a₁ } is set
G1 is set
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in G1 } is set
G0 . { (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in G1 } is set
B3 is set
e is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
e " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
G1 is Relation-like Fin (Permutations n) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (Permutations n)), the carrier of K:]
B3 is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
{B3} is functional non empty trivial V40() V44() 1 -element set
G1 . {B3} is set
(Path_product A) . B3 is Element of the carrier of K
{.B3.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations n)
s is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
s " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
e is V40() Element of Fin (Permutations n)
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in e } is set
{(s ")} is functional non empty trivial V40() V44() 1 -element set
x is set
px is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
px " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
x is set
G1 . e is Element of the carrier of K
G0 . {(s ")} is set
(Path_product (A @)) . (s ") is set
(Path_product A) . s is set
B3 is V40() Element of Fin (Permutations n)
(FinOmega (Permutations n)) \ B3 is V40() Element of Fin (Permutations n)
G1 . B3 is Element of the carrier of K
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in B3 } is set
e is set
s is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
s " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
the Element of B3 is Element of B3
x is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
{x} is functional non empty trivial V40() V44() 1 -element set
B3 \/ {x} is V40() set
G1 . (B3 \/ {x}) is set
(Path_product A) . x is Element of the carrier of K
the addF of K . ((G1 . B3),((Path_product A) . x)) is Element of the carrier of K
[(G1 . B3),((Path_product A) . x)] is set
{(G1 . B3),((Path_product A) . x)} is V40() set
{(G1 . B3)} is non empty trivial V40() 1 -element set
{{(G1 . B3),((Path_product A) . x)},{(G1 . B3)}} is V40() V44() set
the addF of K . [(G1 . B3),((Path_product A) . x)] is set
px is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
px " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
e is V40() Element of Fin (Permutations n)
y is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective V40() Element of Permutations n
{y} is functional non empty trivial V40() V44() 1 -element set
e \/ {y} is V40() set
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in B3 \/ {x} } is set
pd is set
z is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
z " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
pd is set
z is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
z " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
pd is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
pd " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
(pd ") " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
(FinOmega (Permutations n)) \ e is V40() Element of Fin (Permutations n)
pd is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
pd " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
{.x.} is functional non empty trivial V40() V44() 1 -element Element of Fin (Permutations n)
B3 \/ {.x.} is V40() Element of Fin (Permutations n)
G1 . (B3 \/ {.x.}) is Element of the carrier of K
G0 . { (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in B3 \/ {x} } is set
G0 . e is Element of the carrier of K
z is set
p is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
p " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
(Path_product (A @)) . y is Element of the carrier of K
the addF of K . ((G0 . e),((Path_product (A @)) . y)) is Element of the carrier of K
[(G0 . e),((Path_product (A @)) . y)] is set
{(G0 . e),((Path_product (A @)) . y)} is V40() set
{(G0 . e)} is non empty trivial V40() 1 -element set
{{(G0 . e),((Path_product (A @)) . y)},{(G0 . e)}} is V40() V44() set
the addF of K . [(G0 . e),((Path_product (A @)) . y)] is set
G1 . {} is set
bool (Permutations n) is non empty cup-closed diff-closed preBoolean set
e is Element of the carrier of K
B3 is V40() Element of Fin (Permutations n)
{ (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in B3 } is set
s is set
x is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
x " is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):]
G0 . { (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in B3 } is set
G1 . (FinOmega (Permutations n)) is Element of the carrier of K
G0 . { (b₁ ") where b₁ is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective V40() Element of bool [:(Seg n),(Seg n):] : b₁ in FinOmega (Permutations n) } is set