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