REAL is set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal V103() Element of bool REAL
bool REAL is non empty set
RAT is set
{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() complex ext-real non positive non negative V202() V203() V204() V205() set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal V103() set
bool NAT is non empty non trivial non finite V103() set
bool NAT is non empty non trivial non finite V103() set
Fin NAT is preBoolean set
INT is set
COMPLEX is set
1 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
2 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is Relation-like non empty non trivial non finite V103() set
[:[:NAT,NAT:],NAT:] is Relation-like non empty non trivial non finite V103() set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite V103() set
3 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() complex ext-real non positive non negative V202() V203() V204() V205() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V105() Function-yielding V147() complex ext-real non positive non negative V202() V203() V204() V205() set
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V37() 1 -element without_zero V103() set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V37() without_zero V103() set
[1,1] is set
{1,1} is non empty finite V37() without_zero V103() set
{{1,1},{1}} is non empty finite V37() without_zero V103() set
6 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
4 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
24 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
m is non empty set
m * is functional non empty FinSequence-membered FinSequenceSet of m
n is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
M is Relation-like NAT -defined m * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of n,K,m
len M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
width M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
K @ is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
[M,R] is set
{M,R} is non empty finite V37() set
{M} is non empty trivial finite V37() 1 -element set
{{M,R},{M}} is non empty finite V37() without_zero V103() set
Indices (K @) is set
dom (K @) is finite Element of bool NAT
width (K @) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width (K @)) is finite width (K @) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width (K @) ) } is set
[:(dom (K @)),(Seg (width (K @))):] is Relation-like finite set
[R,M] is set
{R,M} is non empty finite V37() set
{R} is non empty trivial finite V37() 1 -element set
{{R,M},{R}} is non empty finite V37() without_zero V103() set
Indices K is set
dom K is finite Element of bool NAT
width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width K) is finite width K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg (width K)):] is Relation-like finite set
K * (R,M) is Element of the carrier of n
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
(K @) * (M,R) is Element of the carrier of n
M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
[M,R] is set
{M,R} is non empty finite V37() set
{M} is non empty trivial finite V37() 1 -element set
{{M,R},{M}} is non empty finite V37() without_zero V103() set
Indices K is set
dom K is finite Element of bool NAT
width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width K) is finite width K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg (width K)):] is Relation-like finite set
[R,M] is set
{R,M} is non empty finite V37() set
{R} is non empty trivial finite V37() 1 -element set
{{R,M},{R}} is non empty finite V37() without_zero V103() set
Indices (K @) is set
dom (K @) is finite Element of bool NAT
width (K @) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width (K @)) is finite width (K @) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width (K @) ) } is set
[:(dom (K @)),(Seg (width (K @))):] is Relation-like finite set
(K @) * (R,M) is Element of the carrier of n
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
K * (M,R) is Element of the carrier of n
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
diagonal_of_Matrix K is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
K @ is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
diagonal_of_Matrix (K @) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (diagonal_of_Matrix K) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
P is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
(diagonal_of_Matrix (K @)) . P is set
(K @) * (P,P) is Element of the carrier of n
Indices K is set
dom K is finite Element of bool NAT
width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width K) is finite width K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg (width K)):] is Relation-like finite set
[:(Seg m),(Seg m):] is Relation-like finite set
[P,P] is set
{P,P} is non empty finite V37() set
{P} is non empty trivial finite V37() 1 -element set
{{P,P},{P}} is non empty finite V37() without_zero V103() set
(diagonal_of_Matrix K) . P is set
K * (P,P) is Element of the carrier of n
len (diagonal_of_Matrix (K @)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Permutations m is non empty permutational set
len (Permutations m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations m)) is finite len (Permutations m) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations m) ) } is set
idseq m is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg m),(Seg m):]
[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set
n is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
K is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg m),(Seg m):]
dom K is finite Element of bool (Seg m)
bool (Seg m) is non empty finite V37() set
M is set
n . M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
R - 1 is V105() complex ext-real set
Seg R is finite R -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= R ) } is set
K .: (Seg R) is finite set
Q is finite set
card (Seg R) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
card Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
n .: (Seg R) is finite set
P is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Seg P is finite P -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= P ) } is set
S is set
x1 is set
n . x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
P + 1 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
n . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
rng K is finite set
rng n is finite set
n . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
P + 1 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
rng K is finite set
rng n is finite set
card (Seg P) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
P + 1 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
P is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . P is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
nat_interval (R,m) is finite Element of bool NAT
K .: (nat_interval (R,m)) is finite set
Q is finite set
S is set
rng K is finite set
x1 is set
n . x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
i1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
card (nat_interval (R,m)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
card Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
S is set
n . S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n . R is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Permutations m is non empty permutational set
len (Permutations m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations m)) is finite len (Permutations m) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations m) ) } is set
idseq m is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg m),(Seg m):]
[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
Path_product K is Relation-like Permutations m -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations m), the carrier of n:]
[:(Permutations m), the carrier of n:] is Relation-like non empty set
bool [:(Permutations m), the carrier of n:] is non empty set
M is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
(Path_product K) . M is Element of the carrier of n
Path_matrix (M,K) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
R is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg m),(Seg m):]
rng R is finite set
Indices K is set
dom K is finite Element of bool NAT
width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width K) is finite width K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg (width K)):] is Relation-like finite set
S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
M . S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
dom R is finite Element of bool (Seg m)
bool (Seg m) is non empty finite V37() set
R . S is set
x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
[S,x1] is set
{S,x1} is non empty finite V37() set
{S} is non empty trivial finite V37() 1 -element set
{{S,x1},{S}} is non empty finite V37() without_zero V103() set
K * (S,x1) is Element of the carrier of n
len (Path_matrix (M,K)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
dom (Path_matrix (M,K)) is finite Element of bool NAT
(Path_matrix (M,K)) . S is set
R is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg m),(Seg m):]
rng R is finite set
Indices K is set
dom K is finite Element of bool NAT
width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (width K) is finite width K -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width K ) } is set
[:(dom K),(Seg (width K)):] is Relation-like finite set
S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
M . S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
dom R is finite Element of bool (Seg m)
bool (Seg m) is non empty finite V37() set
R . S is set
x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
[S,x1] is set
{S,x1} is non empty finite V37() set
{S} is non empty trivial finite V37() 1 -element set
{{S,x1},{S}} is non empty finite V37() without_zero V103() set
K * (S,x1) is Element of the carrier of n
len (Path_matrix (M,K)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
dom (Path_matrix (M,K)) is finite Element of bool NAT
(Path_matrix (M,K)) . S is set
dom (Path_matrix (M,K)) is finite Element of bool NAT
dom (Path_matrix (M,K)) is finite Element of bool NAT
Product (Path_matrix (M,K)) is Element of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total having_a_unity 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 Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
the multF of n $$ (Path_matrix (M,K)) is Element of the carrier of n
S is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
(Path_matrix (M,K)) . S is set
- ((0. n),M) is Element of the carrier of n
- (0. n) is Element of the carrier of n
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Permutations m is non empty permutational set
len (Permutations m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations m)) is finite len (Permutations m) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations m) ) } is set
idseq m is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg m),(Seg m):]
[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
diagonal_of_Matrix K is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
M is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
Path_matrix (M,K) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
len (Path_matrix (M,K)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
M . Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
dom (Path_matrix (M,K)) is finite Element of bool NAT
(Path_matrix (M,K)) . Q is set
K * (Q,Q) is Element of the carrier of n
(diagonal_of_Matrix K) . Q is set
len (diagonal_of_Matrix K) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular upper_triangular Matrix of m,m, the carrier of n
Det K is Element of the carrier of n
Permutations m is non empty permutational set
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
FinOmega (Permutations m) is Element of Fin (Permutations m)
Fin (Permutations m) is preBoolean set
Path_product K is Relation-like Permutations m -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations m), the carrier of n:]
[:(Permutations m), the carrier of n:] is Relation-like non empty set
bool [:(Permutations m), the carrier of n:] is non empty set
the addF of n $$ ((FinOmega (Permutations m)),(Path_product K)) is Element of the carrier of n
diagonal_of_Matrix K is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n $$ (diagonal_of_Matrix K) is Element of the carrier of n
idseq m is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg m),(Seg m):]
[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set
Group_of_Perm m is non empty strict Group-like associative multMagma
the carrier of (Group_of_Perm m) is non empty set
len (Permutations m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations m)) is finite len (Permutations m) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations m) ) } is set
x1 is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
{x1} is functional non empty trivial finite V37() 1 -element Element of bool (Permutations m)
bool (Permutations m) is non empty set
(Permutations m) \ {x1} is Element of bool (Permutations m)
i1 is Element of Fin (Permutations m)
x2 is Element of Fin (Permutations m)
the addF of n $$ (x2,(Path_product K)) is Element of the carrier of n
i1 is Element of Fin (Permutations m)
(Path_product K) .: i1 is Element of Fin the carrier of n
Fin the carrier of n is preBoolean set
0. n is zero Element of the carrier of n
the ZeroF of n is Element of the carrier of n
{(0. n)} is non empty trivial finite 1 -element Element of bool the carrier of n
bool the carrier of n is non empty set
i2 is set
dom (Path_product K) is non empty Element of bool (Permutations m)
y1 is set
(Path_product K) . y1 is set
y2 is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
(Path_product K) . y2 is Element of the carrier of n
the_unity_wrt the addF of n is Element of the carrier of n
dom (Path_product K) is non empty Element of bool (Permutations m)
the addF of n $$ (i1,(Path_product K)) is Element of the carrier of n
x2 is Element of Fin (Permutations m)
i1 \/ x2 is Element of Fin (Permutations m)
x2 \/ (Permutations m) is non empty set
the addF of n $$ (x2,(Path_product K)) is Element of the carrier of n
( the addF of n $$ (x2,(Path_product K))) + (0. n) is Element of the carrier of n
the addF of n . (( the addF of n $$ (x2,(Path_product K))),(0. n)) is Element of the carrier of n
i1 is Element of Fin (Permutations m)
x2 is Element of Fin (Permutations m)
the addF of n $$ (x2,(Path_product K)) is Element of the carrier of n
x2 is Element of Fin (Permutations m)
the addF of n $$ (x2,(Path_product K)) is Element of the carrier of n
(Path_product K) . x1 is Element of the carrier of n
Path_matrix (x1,K) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n $$ (Path_matrix (x1,K)) is Element of the carrier of n
- (( the multF of n $$ (Path_matrix (x1,K))),x1) is Element of the carrier of n
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital doubleLoopStr
the carrier of n is non empty non trivial V103() set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is Relation-like non empty set
[:[: the carrier of n, the carrier of n:], the carrier of n:] is Relation-like non empty set
bool [:[: the carrier of n, the carrier of n:], the carrier of n:] is non empty set
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular lower_triangular Matrix of m,m, the carrier of n
Det K is Element of the carrier of n
Permutations m is non empty permutational set
the addF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
FinOmega (Permutations m) is Element of Fin (Permutations m)
Fin (Permutations m) is preBoolean set
Path_product K is Relation-like Permutations m -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations m), the carrier of n:]
[:(Permutations m), the carrier of n:] is Relation-like non empty set
bool [:(Permutations m), the carrier of n:] is non empty set
the addF of n $$ ((FinOmega (Permutations m)),(Path_product K)) is Element of the carrier of n
diagonal_of_Matrix K is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n $$ (diagonal_of_Matrix K) is Element of the carrier of n
K @ is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding V147() tabular Matrix of m,m, the carrier of n
Det (K @) is Element of the carrier of n
Path_product (K @) is Relation-like Permutations m -defined the carrier of n -valued Function-like non empty total quasi_total Element of bool [:(Permutations m), the carrier of n:]
the addF of n $$ ((FinOmega (Permutations m)),(Path_product (K @))) is Element of the carrier of n
diagonal_of_Matrix (K @) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
the multF of n $$ (diagonal_of_Matrix (K @)) is Element of the carrier of n
m is finite set
bool m is non empty finite V37() set
card m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
n is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
{ b1 where b1 is finite Element of bool m : card b1 = n } is set
card { b1 where b1 is finite Element of bool m : card b1 = n } is V26() V27() V28() cardinal set
(card m) choose n is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Choose (m,K,1,0) is functional Element of bool (Funcs (m,{1,0}))
{1,0} is non empty finite V37() set
Funcs (m,{1,0}) is functional non empty FUNCTION_DOMAIN of m,{1,0}
bool (Funcs (m,{1,0})) is non empty set
m --> 0 is Relation-like m -defined NAT -valued RAT -valued Function-like constant total quasi_total finite Function-yielding V147() V202() V203() V204() V205() Element of bool [:m,NAT:]
[:m,NAT:] is Relation-like set
bool [:m,NAT:] is non empty set
{0} is functional non empty trivial finite V37() 1 -element set
[:m,{0}:] is Relation-like finite set
P is Relation-like Function-like set
dom P is set
rng P is set
Q is set
dom (m --> 0) is finite Element of bool m
{0,1} is non empty finite V37() Element of bool NAT
[:m,{0,1}:] is Relation-like finite set
bool [:m,{0,1}:] is non empty finite V37() set
{1} is non empty trivial finite V37() 1 -element without_zero V103() Element of bool NAT
S is Relation-like m -defined {0,1} -valued Function-like total quasi_total finite Element of bool [:m,{0,1}:]
S " {1} is finite set
card (S " {1}) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
dom S is finite Element of bool m
x1 is finite Element of bool m
x2 is set
S . x2 is set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
(x1 --> 1) . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
dom (x1 --> 1) is finite Element of bool x1
bool x1 is non empty finite V37() set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x1) . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
S . x2 is set
rng S is finite set
(m --> 0) . x2 is Relation-like Function-like V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
dom (x1 --> 1) is finite Element of bool x1
bool x1 is non empty finite V37() set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x1) . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
S . x2 is set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x1) . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
S . x2 is set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x1) . x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
dom (x1 --> 1) is finite Element of bool x1
bool x1 is non empty finite V37() set
dom H1(x1) is set
m \/ x1 is finite set
P . x1 is set
Q is set
S is set
P . Q is set
P . S is set
x1 is finite Element of bool m
card x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
x2 is finite Element of bool m
card x2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
x2 --> 1 is Relation-like non-empty x2 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x2,NAT:]
[:x2,NAT:] is Relation-like set
bool [:x2,NAT:] is non empty set
[:x2,{1}:] is Relation-like finite set
dom (x2 --> 1) is finite Element of bool x2
bool x2 is non empty finite V37() set
i1 is set
(x2 --> 1) . i1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
(m --> 0) +* (x2 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x2) . i1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
dom (x1 --> 1) is finite Element of bool x1
bool x1 is non empty finite V37() set
(m --> 0) . i1 is Relation-like Function-like V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
H1(x1) . i1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative V201() set
Q is set
S is set
P . S is set
x1 is finite Element of bool m
card x1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
x1 \/ m is finite set
x1 --> 1 is Relation-like non-empty x1 -defined NAT -valued RAT -valued Function-like constant total quasi_total finite V202() V203() V204() V205() Element of bool [:x1,NAT:]
[:x1,NAT:] is Relation-like set
bool [:x1,NAT:] is non empty set
[:x1,{1}:] is Relation-like finite set
(m --> 0) +* (x1 --> 1) is Relation-like RAT -valued Function-like finite V202() V203() V204() V205() set
card (Choose (m,K,1,0)) is V26() V27() V28() cardinal set
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
TWOELEMENTSETS (Seg m) is set
card (TWOELEMENTSETS (Seg m)) is V26() V27() V28() cardinal set
m choose 2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
bool (Seg m) is non empty finite V37() set
{ b1 where b1 is finite Element of bool (Seg m) : card b1 = 2 } is set
card (Seg m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
(card (Seg m)) choose 2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
m is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Permutations m is non empty permutational set
len (Permutations m) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations m)) is finite len (Permutations m) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations m) ) } is set
idseq m is Relation-like NAT -defined Function-like finite m -element FinSequence-like FinSubsequence-like set
Seg m is finite m -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= m ) } is set
id (Seg m) is Relation-like Seg m -defined Seg m -valued Function-like one-to-one total quasi_total finite Element of bool [:(Seg m),(Seg m):]
[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set
Rev (idseq m) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
m choose 2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
(m choose 2) mod 2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
n is Relation-like Seg (len (Permutations m)) -defined Seg (len (Permutations m)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations m
m - 1 is V105() complex ext-real set
m * (m - 1) is V105() complex ext-real set
(m * (m - 1)) / 2 is V105() complex ext-real set
m - 2 is V105() complex ext-real set
M is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
M + 2 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
Permutations (M + 2) is non empty permutational set
len (Permutations (M + 2)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Seg (len (Permutations (M + 2))) is finite len (Permutations (M + 2)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (M + 2)) ) } is set
the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
Seg (M + 2) is non empty finite M + 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= M + 2 ) } is set
TWOELEMENTSETS (Seg (M + 2)) is non empty finite set
FinOmega (TWOELEMENTSETS (Seg (M + 2))) is Element of Fin (TWOELEMENTSETS (Seg (M + 2)))
Fin (TWOELEMENTSETS (Seg (M + 2))) is preBoolean set
idseq (M + 2) is Relation-like NAT -defined Function-like finite M + 2 -element FinSequence-like FinSubsequence-like set
id (Seg (M + 2)) is Relation-like Seg (M + 2) -defined Seg (M + 2) -valued Function-like one-to-one non empty total quasi_total finite Element of bool [:(Seg (M + 2)),(Seg (M + 2)):]
[:(Seg (M + 2)),(Seg (M + 2)):] is Relation-like non empty finite set
bool [:(Seg (M + 2)),(Seg (M + 2)):] is non empty finite V37() set
Group_of_Perm (M + 2) is non empty strict Group-like associative multMagma
the carrier of (Group_of_Perm (M + 2)) is non empty set
the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is non empty non trivial V103() set
S is Relation-like Seg (len (Permutations (M + 2))) -defined Seg (len (Permutations (M + 2))) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations (M + 2)
Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Relation-like TWOELEMENTSETS (Seg (M + 2)) -defined the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (M + 2))), the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :]
[:(TWOELEMENTSETS (Seg (M + 2))), the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (M + 2))), the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is non empty set
R is Relation-like Seg (len (Permutations (M + 2))) -defined Seg (len (Permutations (M + 2))) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations (M + 2)
Part_sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Relation-like TWOELEMENTSETS (Seg (M + 2)) -defined the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (M + 2))), the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :]
{ b1 where b1 is Element of TWOELEMENTSETS (Seg (M + 2)) : ( b1 in TWOELEMENTSETS (Seg (M + 2)) & not (Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . b1 = (Part_sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . b1 ) } is set
x2 is set
i1 is Element of TWOELEMENTSETS (Seg (M + 2))
(Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . i1 is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
(Part_sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . i1 is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
x2 is finite set
i1 is set
i2 is Element of TWOELEMENTSETS (Seg (M + 2))
y1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
y2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
{y1,y2} is non empty finite V37() set
S . y2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
P1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Q1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
Q1 + 2 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
(Q1 + 2) - Q is V105() complex ext-real set
((Q1 + 2) - Q) + 1 is V105() complex ext-real set
(Q1 + 2) - P1 is V105() complex ext-real set
((Q1 + 2) - P1) + 1 is V105() complex ext-real set
P2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
S . P2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
len (idseq (M + 2)) is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
dom S is finite Element of bool (Seg (len (Permutations (M + 2))))
bool (Seg (len (Permutations (M + 2)))) is non empty finite V37() set
R . Q is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
R . P1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
Q2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT
S . Q2 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
S . y1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative set
(Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . i2 is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1_ the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1. the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is non zero Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the OneF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
(Q1 + 2) + 1 is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
((Q1 + 2) + 1) - Q is V105() complex ext-real set
((Q1 + 2) + 1) - P1 is V105() complex ext-real set
(Part_sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr )) . i2 is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
- (1_ the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
card (TWOELEMENTSETS (Seg (M + 2))) is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT
sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Relation-like [: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] -defined the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :]
[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is Relation-like non empty set
[:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is Relation-like non empty set
bool [:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is non empty set
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr $$ ((FinOmega (TWOELEMENTSETS (Seg (M + 2)))),(Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ))) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1_ the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1. the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is non zero Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the OneF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr $$ ((FinOmega (TWOELEMENTSETS (Seg (M + 2)))),(Part_sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ))) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Relation-like [: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] -defined the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :]
[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is Relation-like non empty set
[:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is Relation-like non empty set
bool [:[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :], the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr :] is non empty set
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr $$ ((FinOmega (TWOELEMENTSETS (Seg (M + 2)))),(Part_sgn (S, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ))) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1_ the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
1. the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is non zero Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the OneF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
sgn (R, the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr ) is Element of the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr
the multF of the non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V167() left_unital Fanoian doubleLoopStr $$ ((FinOmega (TWOELEMENTSETS (Seg (M + 2)))),(Part_