:: MATRIX13 semantic presentation

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

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

INT 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

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is Relation-like non empty non trivial non finite V103() set
is Relation-like non empty non trivial non finite V103() set
bool 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

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

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

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

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

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

width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of 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 ()):] 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

width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of 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 ()):] 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

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

len 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

{ 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
() . P is set
(K @) * (P,P) is Element of the carrier of n
Indices K is set

width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of 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 ()):] 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
. P is set
K * (P,P) is Element of the carrier of n
len () 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 () is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{ 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

[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set

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

{ 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

{ 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 () is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{ 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

[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set

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

[:(), the carrier of n:] is Relation-like non empty set
bool [:(), the carrier of n:] is non empty set

() . M is Element of the carrier of n

rng R is finite set
Indices K is set

width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of 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 ()):] 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

rng R is finite set
Indices K is set

width K is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of 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 ()):] 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 () is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{ 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

[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set

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

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
. Q is set
len 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

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

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 () is Element of Fin ()

[:(), the carrier of n:] is Relation-like non empty set
bool [:(), the carrier of n:] is non empty set
the addF of n \$\$ ((),()) is Element of the carrier of n

the multF of n \$\$ is Element of the carrier of n

{ 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

[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() set

the carrier of () is non empty set
len () is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{x1} is functional non empty trivial finite V37() 1 -element Element of bool ()
bool () is non empty set
() \ {x1} is Element of bool ()
i1 is Element of Fin ()
x2 is Element of Fin ()
the addF of n \$\$ (x2,()) is Element of the carrier of n
i1 is Element of Fin ()
() .: 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 () is non empty Element of bool ()
y1 is set
() . y1 is set

() . y2 is Element of the carrier of n
the_unity_wrt the addF of n is Element of the carrier of n
dom () is non empty Element of bool ()
the addF of n \$\$ (i1,()) is Element of the carrier of n
x2 is Element of Fin ()
i1 \/ x2 is Element of Fin ()
x2 \/ () is non empty set
the addF of n \$\$ (x2,()) is Element of the carrier of n
( the addF of n \$\$ (x2,())) + (0. n) is Element of the carrier of n
the addF of n . (( the addF of n \$\$ (x2,())),(0. n)) is Element of the carrier of n
i1 is Element of Fin ()
x2 is Element of Fin ()
the addF of n \$\$ (x2,()) is Element of the carrier of n
x2 is Element of Fin ()
the addF of n \$\$ (x2,()) is Element of the carrier of n
() . x1 is Element 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

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

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 () is Element of Fin ()

[:(), the carrier of n:] is Relation-like non empty set
bool [:(), the carrier of n:] is non empty set
the addF of n \$\$ ((),()) is Element of the carrier of n

the multF of n \$\$ is Element of 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 [:(), the carrier of n:]
the addF of n \$\$ ((),(Path_product (K @))) is Element of the carrier of n

the multF of n \$\$ () 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

bool [:m,NAT:] is non empty 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

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 " {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

bool [:x1,NAT:] is non empty 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

bool [:x1,NAT:] is non empty 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

bool [:x1,NAT:] is non empty 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

bool [:x1,NAT:] is non empty 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

bool [:x2,NAT:] is non empty 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

bool [:x1,NAT:] is non empty 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

bool [:x1,NAT:] is non empty 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

{ 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 () 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 () is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT

{ b1 where b1 is V26() V27() V28() V32() finite cardinal V105() complex ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

{ 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

[:(Seg m),(Seg m):] is Relation-like finite set
bool [:(Seg m),(Seg m):] is non empty finite V37() 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

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

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

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

[::] is Relation-like non empty set
bool [::] is non empty set

{ b1 where b1 is Element of TWOELEMENTSETS (Seg (M + 2)) : ( b1 in TWOELEMENTSETS (Seg (M + 2)) & not () . b1 = () . b1 ) } is set
x2 is set
i1 is Element of TWOELEMENTSETS (Seg (M + 2))
() . 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
() . 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
() . 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

(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
() . 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

card (TWOELEMENTSETS (Seg (M + 2))) is non empty V26() V27() V28() V32() finite cardinal V105() complex ext-real positive non negative Element of NAT

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 [::] -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 :]
[::] 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 :] 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 :] 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 is Relation-like [::] -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 :]
[::] 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 :] 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 :] is non empty set