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

{1} is non empty trivial V40() V44() 1 -element set

Seg 2 is non empty V40() 2 -element Element of bool NAT

{ b

{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

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

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

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

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

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

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

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

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

(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

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

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

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

[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

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

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

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

{ b

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

(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

(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

Seg K is V40() K -element Element of bool NAT

{ b

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 (