:: MATRIX11 semantic presentation

REAL is set

INT is set

[:1,1:] is Relation-like non empty finite set

[:[:1,1:],1:] is Relation-like non empty finite set
bool [:[:1,1:],1:] is non empty cup-closed diff-closed preBoolean finite V52() set

Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V52() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V52() set
Permutations 1 is non empty permutational set

[:(Seg 1),(Seg 1):] is Relation-like non empty finite set
bool [:(Seg 1),(Seg 1):] is non empty cup-closed diff-closed preBoolean finite V52() set
{()} is functional non empty trivial finite V52() 1 -element set

n is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
TWOELEMENTSETS (Seg K) is set
A is set
B is set
{A,B} is non empty finite set

{A,B} is non empty finite V52() set

{A,B} is non empty finite V52() set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= {} ) } is set

TWOELEMENTSETS (Seg 1) is set
n is set

{K,A} is non empty finite V52() set
n is set

{K,A} is non empty finite V52() set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
TWOELEMENTSETS (Seg n) is set

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is set

Permutations n is non empty permutational set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len () ) } is set

K is set
A . K is set
dom A is finite set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V52() set
rng A is finite set
dom A is finite set
dom A is finite set

the carrier of n is non empty non trivial set
the multF of n is Relation-like [: the carrier of n, the carrier of n:] -defined the carrier of n -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of n, the carrier of n:], the carrier of n:]
[: the carrier of n, the carrier of n:] is 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 cup-closed diff-closed preBoolean set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

the carrier of K is non empty non trivial set
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set

1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K
P is set

{KK,mm} is non empty finite V52() set
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set

{aa,AB} is non empty finite V52() set

{aa,AB} is non empty finite V52() set

aa is set
AB is set
P is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]

{KK,mm} is non empty finite V52() set
P . {KK,mm} is set
P is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
KK is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
mm is set
P . mm is set
KK . mm is set

{aa,AB} is non empty finite V52() set
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set

P . {aa,AB} is set
P . {aa,AB} is set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
Fin (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean set

1_ K is Element of the carrier of K
the carrier of K is non empty non trivial set
K254(K) is V70(K) Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set

(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
B is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
the multF of K \$\$ (B,(n,K,A)) is Element of the carrier of K
[:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is Relation-like non empty set
bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
AB is Relation-like Fin (TWOELEMENTSETS (Seg (n + 2))) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:]
AB . B is Element of the carrier of K
AB . {} is set

F is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

AB . F is Element of the carrier of K
Ga is set
{Ga} is non empty trivial finite 1 -element set
Gs is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,A) . Gs is Element of the carrier of K
Ga is set
Gs is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,A) . Gs is Element of the carrier of K
{Gs} is non empty trivial finite 1 -element set
F \ {Gs} is finite Element of bool F

B9 is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
B \ B9 is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
{Gs} \/ B9 is non empty finite set

AB . B9 is Element of the carrier of K
(1_ K) * (1_ K) is Element of the carrier of K
the multF of K . ((1_ K),(1_ K)) is Element of the carrier of K
[(1_ K),(1_ K)] is set
{(1_ K),(1_ K)} is non empty finite set
{(1_ K)} is non empty trivial finite 1 -element set
{{(1_ K),(1_ K)},{(1_ K)}} is non empty finite V52() set
the multF of K . [(1_ K),(1_ K)] is set
SUM1 is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

AB . SUM1 is Element of the carrier of K

SUM1 is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

AB . SUM1 is Element of the carrier of K

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

the carrier of K is non empty non trivial set
1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K

(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
B is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,A) . B is Element of the carrier of K

{P,KK} is non empty finite V52() set
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set

(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
the carrier of K is non empty non trivial set
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set

(n,K,B) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]

{KK,mm} is non empty finite V52() set
(n,K,A) . {KK,mm} is set
(n,K,B) . {KK,mm} is set
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set
aa is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
aa . KK is set
aa . mm is set
1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
Fin (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean set
Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set

the carrier of K is non empty non trivial set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
A is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

(n,K,B) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the multF of K \$\$ (A,(n,K,B)) is Element of the carrier of K

(n,K,P) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
{ b1 where b1 is Element of TWOELEMENTSETS (Seg (n + 2)) : ( b1 in A & not (n,K,B) . b1 = (n,K,P) . b1 ) } is set
the multF of K \$\$ (A,(n,K,P)) is Element of the carrier of K
- ( the multF of K \$\$ (A,(n,K,P))) is Element of the carrier of K
KK is finite set

A \ KK is finite Element of bool A

Path is set
F is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,B) . F is Element of the carrier of K
(n,K,P) . F is Element of the carrier of K
SUM1 is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
KK \/ SUM1 is finite set
[:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is Relation-like non empty set
bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
Path is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
the multF of K \$\$ (Path,(n,K,B)) is Element of the carrier of K
Gs is Relation-like Fin (TWOELEMENTSETS (Seg (n + 2))) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:]
Gs . KK is set
Gs . {} is set
the multF of K \$\$ (Path,(n,K,P)) is Element of the carrier of K
B9 is Relation-like Fin (TWOELEMENTSETS (Seg (n + 2))) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:]
B9 . KK is set
B9 . {} is set
b is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,B) . b is Element of the carrier of K
(n,K,P) . b is Element of the carrier of K
- ((n,K,P) . b) is Element of the carrier of K
1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K
((n,K,B) . b) + ((n,K,P) . b) is Element of the carrier of K
the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
the addF of K . (((n,K,B) . b),((n,K,P) . b)) is Element of the carrier of K
[((n,K,B) . b),((n,K,P) . b)] is set
{((n,K,B) . b),((n,K,P) . b)} is non empty finite set
{((n,K,B) . b)} is non empty trivial finite 1 -element set
{{((n,K,B) . b),((n,K,P) . b)},{((n,K,B) . b)}} is non empty finite V52() set
the addF of K . [((n,K,B) . b),((n,K,P) . b)] is set
0. K is V70(K) Element of the carrier of K
mA is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,B) . mA is Element of the carrier of K
(n,K,P) . mA is Element of the carrier of K

Bb is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

Gs . Bb is Element of the carrier of K
B9 . Bb is Element of the carrier of K
- (B9 . Bb) is Element of the carrier of K
PM is set
{PM} is non empty trivial finite 1 -element set
i is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,P) . i is Element of the carrier of K
(n,K,B) . i is Element of the carrier of K
PM is set
i is Element of TWOELEMENTSETS (Seg (n + 2))
{i} is non empty trivial finite 1 -element set
Bb \ {i} is finite Element of bool Bb

Pi is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
KK \ Pi is finite Element of bool KK

{i} \/ Pi is non empty finite set

B9 . Pi is Element of the carrier of K
(n,K,P) . i is Element of the carrier of K
the multF of K . ((B9 . Pi),((n,K,P) . i)) is Element of the carrier of K
[(B9 . Pi),((n,K,P) . i)] is set
{(B9 . Pi),((n,K,P) . i)} is non empty finite set
{(B9 . Pi)} is non empty trivial finite 1 -element set
{{(B9 . Pi),((n,K,P) . i)},{(B9 . Pi)}} is non empty finite V52() set
the multF of K . [(B9 . Pi),((n,K,P) . i)] is set
Gs . Pi is Element of the carrier of K
(n,K,B) . i is Element of the carrier of K
the multF of K . ((Gs . Pi),((n,K,B) . i)) is Element of the carrier of K
[(Gs . Pi),((n,K,B) . i)] is set
{(Gs . Pi),((n,K,B) . i)} is non empty finite set
{(Gs . Pi)} is non empty trivial finite 1 -element set
{{(Gs . Pi),((n,K,B) . i)},{(Gs . Pi)}} is non empty finite V52() set
the multF of K . [(Gs . Pi),((n,K,B) . i)] is set

2 - 1 is ext-real V44() V45() set

- ((n,K,P) . i) is Element of the carrier of K
(Gs . Pi) * (- ((n,K,P) . i)) is Element of the carrier of K
the multF of K . ((Gs . Pi),(- ((n,K,P) . i))) is Element of the carrier of K
[(Gs . Pi),(- ((n,K,P) . i))] is set
{(Gs . Pi),(- ((n,K,P) . i))} is non empty finite set
{{(Gs . Pi),(- ((n,K,P) . i))},{(Gs . Pi)}} is non empty finite V52() set
the multF of K . [(Gs . Pi),(- ((n,K,P) . i))] is set
(Gs . Pi) * ((n,K,P) . i) is Element of the carrier of K
the multF of K . ((Gs . Pi),((n,K,P) . i)) is Element of the carrier of K
[(Gs . Pi),((n,K,P) . i)] is set
{(Gs . Pi),((n,K,P) . i)} is non empty finite set
{{(Gs . Pi),((n,K,P) . i)},{(Gs . Pi)}} is non empty finite V52() set
the multF of K . [(Gs . Pi),((n,K,P) . i)] is set

- ((n,K,P) . i) is Element of the carrier of K
- (B9 . Pi) is Element of the carrier of K
(- (B9 . Pi)) * (- ((n,K,P) . i)) is Element of the carrier of K
the multF of K . ((- (B9 . Pi)),(- ((n,K,P) . i))) is Element of the carrier of K
[(- (B9 . Pi)),(- ((n,K,P) . i))] is set
{(- (B9 . Pi)),(- ((n,K,P) . i))} is non empty finite set
{(- (B9 . Pi))} is non empty trivial finite 1 -element set
{{(- (B9 . Pi)),(- ((n,K,P) . i))},{(- (B9 . Pi))}} is non empty finite V52() set
the multF of K . [(- (B9 . Pi)),(- ((n,K,P) . i))] is set
2 - 1 is ext-real V44() V45() set
(B9 . Pi) * ((n,K,P) . i) is Element of the carrier of K

b is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

Gs . b is Element of the carrier of K
B9 . b is Element of the carrier of K
- (B9 . b) is Element of the carrier of K

1_ K is Element of the carrier of K
K254(K) is V70(K) Element of the carrier of K
the multF of K \$\$ (SUM1,(n,K,B)) is Element of the carrier of K
the multF of K . (( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,B)))) is Element of the carrier of K
[( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,B)))] is set
{( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,B)))} is non empty finite set
{( the multF of K \$\$ (SUM1,(n,K,B)))} is non empty trivial finite 1 -element set
{{( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,B)))},{( the multF of K \$\$ (SUM1,(n,K,B)))}} is non empty finite V52() set
the multF of K . [( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,B)))] is set
the multF of K \$\$ (SUM1,(n,K,P)) is Element of the carrier of K
the multF of K . (( the multF of K \$\$ (SUM1,(n,K,P))),( the multF of K \$\$ (Path,(n,K,P)))) is Element of the carrier of K
[( the multF of K \$\$ (SUM1,(n,K,P))),( the multF of K \$\$ (Path,(n,K,P)))] is set
{( the multF of K \$\$ (SUM1,(n,K,P))),( the multF of K \$\$ (Path,(n,K,P)))} is non empty finite set
{( the multF of K \$\$ (SUM1,(n,K,P)))} is non empty trivial finite 1 -element set
{{( the multF of K \$\$ (SUM1,(n,K,P))),( the multF of K \$\$ (Path,(n,K,P)))},{( the multF of K \$\$ (SUM1,(n,K,P)))}} is non empty finite V52() set
the multF of K . [( the multF of K \$\$ (SUM1,(n,K,P))),( the multF of K \$\$ (Path,(n,K,P)))] is set
dom (n,K,B) is non empty finite set
(n,K,B) | SUM1 is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined SUM1 -defined TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
dom ((n,K,B) | SUM1) is finite set
dom (n,K,P) is non empty finite set
(n,K,P) | SUM1 is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined SUM1 -defined TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
dom ((n,K,P) | SUM1) is finite set
b is set
((n,K,B) | SUM1) . b is set
((n,K,P) | SUM1) . b is set
mA is Element of TWOELEMENTSETS (Seg (n + 2))
((n,K,B) | SUM1) . mA is set
(n,K,B) . mA is Element of the carrier of K
((n,K,P) | SUM1) . mA is set
(n,K,P) . mA is Element of the carrier of K
( the multF of K \$\$ (SUM1,(n,K,B))) * ( the multF of K \$\$ (Path,(n,K,P))) is Element of the carrier of K
the multF of K . (( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,P)))) is Element of the carrier of K
[( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,P)))] is set
{( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,P)))} is non empty finite set
{{( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,P)))},{( the multF of K \$\$ (SUM1,(n,K,B)))}} is non empty finite V52() set
the multF of K . [( the multF of K \$\$ (SUM1,(n,K,B))),( the multF of K \$\$ (Path,(n,K,P)))] is set
- ( the multF of K \$\$ (Path,(n,K,P))) is Element of the carrier of K
( the multF of K \$\$ (SUM1,(n,K,B))) * (- ( the multF of K \$\$ (Path,(n,K,P)))) is Element of the carrier of K
the multF of K . (( the multF of K \$\$ (SUM1,(n,K,B))),(- ( the multF of K \$\$ (Path,(n,K,P))))) is Element of the carrier of K
[( the multF of K \$\$ (SUM1,(n,K,B))),(- ( the multF of K \$\$ (Path,(n,K,P))))] is set
{( the multF of K \$\$ (SUM1,(n,K,B))),(- ( the multF of K \$\$ (Path,(n,K,P))))} is non empty finite set
{{( the multF of K \$\$ (SUM1,(n,K,B))),(- ( the multF of K \$\$ (Path,(n,K,P))))},{( the multF of K \$\$ (SUM1,(n,K,B)))}} is non empty finite V52() set
the multF of K . [( the multF of K \$\$ (SUM1,(n,K,B))),(- ( the multF of K \$\$ (Path,(n,K,P))))] is set

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
[:(Seg n),(Seg n):] is Relation-like finite set
bool [:(Seg n),(Seg n):] is non empty cup-closed diff-closed preBoolean finite V52() set

dom K is finite set

K . A is set
K . B is set

K . P is set

K . KK is set
rng K is finite set

K . mm is set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

the carrier of K is non empty non trivial set
KK is Relation-like Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations (n + 2)

B * P is Relation-like Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -valued Seg (len (Permutations (n + 2))) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):]
[:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):] is Relation-like finite set
bool [:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):] is non empty cup-closed diff-closed preBoolean finite V52() set
(n,K,B) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
(n,K,KK) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]

[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set
Path is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,B) . Path is Element of the carrier of K
(n,K,KK) . Path is Element of the carrier of K
AB is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
dom AB is non empty finite set
SUM1 is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
dom SUM1 is non empty finite set

{F,Ga} is non empty finite V52() set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set

1_ K is Element of the carrier of K
the carrier of K is non empty non trivial set
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K

(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set

{P,KK} is non empty finite V52() set
(n,K,A) . {P,KK} is set

[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set
mm is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
mm . P is set
mm . KK is set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set

A * B is Relation-like Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -valued Seg (len (Permutations (n + 2))) -valued Function-like one-to-one total quasi_total onto bijective bijective finite Element of bool [:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):]
[:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):] is Relation-like finite set
bool [:(Seg (len (Permutations (n + 2)))),(Seg (len (Permutations (n + 2)))):] is non empty cup-closed diff-closed preBoolean finite V52() set

{KK,mm} is non empty finite V52() set

1_ aa is Element of the carrier of aa
the carrier of aa is non empty non trivial set
K254(aa) is V70(aa) Element of the carrier of aa
- (1_ aa) is Element of the carrier of aa
(n,aa,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of aa -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of aa:]
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of aa:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of aa:] is non empty cup-closed diff-closed preBoolean set
(n,aa,A) . {KK,mm} is set
(n,aa,P) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of aa -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of aa:]
(n,aa,P) . {KK,mm} is set
dom B is finite set
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like non empty finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is non empty cup-closed diff-closed preBoolean finite V52() set
F is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
dom F is non empty finite set
Ga is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
dom Ga is non empty finite set

Path is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
dom Path is non empty finite set
Path . KK is set
Path . mm is set

{KK,Gs} is non empty finite V52() set
(n,aa,A) . {KK,Gs} is set
(n,aa,P) . {KK,Gs} is set
{mm,Gs} is non empty finite V52() set
(n,aa,A) . {mm,Gs} is set
(n,aa,P) . {mm,Gs} is set

{Gs,KK} is non empty finite V52() set
(n,aa,A) . {Gs,KK} is set

{Gs,mm} is non empty finite V52() set
(n,aa,A) . {Gs,mm} is set

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

the carrier of K is non empty non trivial set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
FinOmega (TWOELEMENTSETS (Seg (n + 2))) is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
Fin (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean set

(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the multF of K \$\$ ((FinOmega (TWOELEMENTSETS (Seg (n + 2)))),(n,K,A)) is Element of the carrier of K

Permutations (n + 2) is non empty permutational set

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 2)) ) } is set

1_ K is Element of the carrier of K
the carrier of K is non empty non trivial set
K254(K) is V70(K) Element of the carrier of K
- (1_ K) is Element of the carrier of K

(n,K,A) is Element of the carrier of K
Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
TWOELEMENTSETS (Seg (n + 2)) is non empty finite set
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total having_a_unity commutative associative Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]
[: the carrier of K, the carrier of K:] is Relation-like non empty set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty cup-closed diff-closed preBoolean set
FinOmega (TWOELEMENTSETS (Seg (n + 2))) is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
Fin (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean set
(n,K,A) is Relation-like TWOELEMENTSETS (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty total quasi_total finite Element of bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:]
[:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is Relation-like non empty set
bool [:(TWOELEMENTSETS (Seg (n + 2))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
the multF of K \$\$ ((FinOmega (TWOELEMENTSETS (Seg (n + 2)))),(n,K,A)) is Element of the carrier of K
[:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is Relation-like non empty set
bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:] is non empty cup-closed diff-closed preBoolean set
AB is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
the multF of K \$\$ (AB,(n,K,A)) is Element of the carrier of K
SUM1 is Relation-like Fin (TWOELEMENTSETS (Seg (n + 2))) -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:(Fin (TWOELEMENTSETS (Seg (n + 2)))), the carrier of K:]
SUM1 . AB is Element of the carrier of K
SUM1 . {} is set

Ga is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))

SUM1 . Ga is Element of the carrier of K
Gs is set
{Gs} is non empty trivial finite 1 -element set
B9 is Element of TWOELEMENTSETS (Seg (n + 2))
(n,K,A) . B9 is Element of the carrier of K
Gs is set
B9 is Element of TWOELEMENTSETS (Seg (n + 2))
{B9} is non empty trivial finite 1 -element set
Ga \ {B9} is finite Element of bool Ga

b is finite Element of Fin (TWOELEMENTSETS (Seg (n + 2)))
{B9} \/ b is non empty finite set

SUM1 . b is Element of the carrier of K
(TWOELEMENTSETS (Seg (n + 2))) \ b is finite Element of bool (TWOELEMENTSETS (Seg (n + 2)))
bool (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean finite V52() set
(n,K,A) . B9 is Element of the carrier of K
the multF of K . ((SUM1 . b),((n,K,A) . B9)) is Element of the carrier of K
[(SUM1 . b),((n,K,A) . B9)] is set
{(SUM1 . b),((n,K,A) . B9)} is non empty finite set
{(SUM1 . b)} is non empty trivial finite 1 -element set
{{(SUM1 . b),((n,K,A) . B9)},{(SUM1 . b)}} is non empty finite V52() set
the multF of K . [(SUM1 . b),((n,K,A) . B9)] is set
(1_ K) * (1_ K) is Element of the carrier of K
the multF of K . ((1_ K),(1_ K)) is Element of the carrier of K
[(1_ K),(1_ K)] is set
{(1_ K),(1_ K)} is non empty fini