:: MATRIX11 semantic presentation

REAL is set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

{} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

the Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

COMPLEX is set

NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial non finite cardinal limit_cardinal set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

Fin NAT is non empty cup-closed diff-closed preBoolean set

INT is set

1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

bool [:1,1:] is non empty cup-closed diff-closed preBoolean finite V52() 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

3 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of NAT

Seg 1 is non empty trivial finite 1 -element Element of bool NAT

{ b

{1} is non empty trivial finite V52() 1 -element set

Seg 2 is non empty finite 2 -element Element of bool NAT

{ b

{1,2} is non empty finite V52() set

Permutations 1 is non empty permutational set

idseq 1 is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set

id (Seg 1) is Relation-like Seg 1 -defined Seg 1 -valued V6() V8() V9() V13() Function-like one-to-one non empty total quasi_total onto bijective finite Element of bool [:(Seg 1),(Seg 1):]

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

{(idseq 1)} is functional non empty trivial finite V52() 1 -element set

dom {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

rng {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty trivial ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V120() set

id {} is Relation-like non-empty empty-yielding {} -defined {} -valued V6() V8() V9() V13() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty total ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

len {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered set

{{}} is functional non empty trivial finite V52() 1 -element set

n is set

K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

Seg K is finite K -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg K) is set

A is set

B is set

{A,B} is non empty finite set

P is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

Seg {} is Relation-like non-empty empty-yielding NAT -defined epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Function-like one-to-one constant functional empty proper ext-real non positive non negative V44() V45() finite finite-yielding V52() cardinal {} -element {} -element FinSequence-like FinSubsequence-like FinSequence-membered Element of bool NAT

{ b

TWOELEMENTSETS (Seg {}) is set

TWOELEMENTSETS (Seg 1) is set

n is set

K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

n is set

K is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

Seg n is finite n -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg n) is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is set

{} + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

Permutations n is non empty permutational set

len (Permutations n) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations n)) is finite len (Permutations n) -element Element of bool NAT

{ b

A is Relation-like Seg (len (Permutations n)) -defined Seg (len (Permutations n)) -valued Function-like one-to-one total quasi_total onto bijective finite Element of Permutations n

K is set

A . K is set

dom A is finite set

Seg n is finite n -element Element of bool NAT

{ b

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

n is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

A . AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

A . AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

A . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

{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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

A . aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . AB is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

P . {aa,AB} is set

P . {aa,AB} is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

Fin (TWOELEMENTSETS (Seg (n + 2))) is non empty cup-closed diff-closed preBoolean set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

(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

SUM1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

SUM1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

card F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

bool F is non empty cup-closed diff-closed preBoolean finite V52() set

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

card B9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card B9) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

card SUM1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

AB . SUM1 is Element of the carrier of K

card B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

card SUM1 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

AB . SUM1 is Element of the carrier of K

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

(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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

{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

A . P is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

A 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)

(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

B 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)

(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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

{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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

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

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

B 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)

(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

P 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)

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

{ b

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

card KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card KK) mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

A \ KK is finite Element of bool A

bool A is non empty cup-closed diff-closed preBoolean finite V52() set

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

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

b + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

card Bb is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card Bb) mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

bool Bb is non empty cup-closed diff-closed preBoolean finite V52() set

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

KK \ Pi is finite Element of bool KK

bool KK is non empty cup-closed diff-closed preBoolean finite V52() set

{i} \/ Pi is non empty finite set

card Pi is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card Pi) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

b mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

(b + 1) mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

{} + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

b mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

- ((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 mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

b mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

card b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card b) mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

{} mod 2 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

Seg n is finite n -element Element of bool NAT

{ b

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

K is Relation-like Seg n -defined Seg n -valued Function-like one-to-one total quasi_total onto bijective finite Element of bool [:(Seg n),(Seg n):]

dom K is finite set

A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

K . A is set

K . B is set

P is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

K . P is set

KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

K . KK is set

rng K is finite set

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

K . mm is set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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)

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

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

P . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

aa is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

Ga is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

P . Ga is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

KK . Ga is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . Ga is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

P . F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

KK . F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . F is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

(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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . P is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

(n,K,A) . {P,KK} is set

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

P 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 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)

A 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)

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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

aa is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

P . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

B . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

P . mm is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . KK is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

Gs is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal 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

B . Gs is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

P . Gs is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

A . (B . Gs) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

(n,aa,A) . {Gs,KK} is set

A . Gs is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

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

(n,aa,A) . {Gs,mm} is set

A . Gs is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

TWOELEMENTSETS (Seg (n + 2)) is non empty finite set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

(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

n is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal set

n + 2 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

Permutations (n + 2) is non empty permutational set

len (Permutations (n + 2)) is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT

{ b

K is non empty non degenerated non trivial right_complementable almost_left_invertible V113() unital associative commutative Abelian add-associative right_zeroed right-distributive left-distributive right_unital well-unital V171() left_unital doubleLoopStr

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

A 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)

(n,K,A) is Element of the carrier of K

Seg (n + 2) is non empty finite n + 2 -element Element of bool NAT

{ b

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

Path is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

Path + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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

card Ga is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

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

bool Ga is non empty cup-closed diff-closed preBoolean finite V52() set

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

{B9} \/ b is non empty finite set

card b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V44() V45() finite cardinal Element of NAT

(card b) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty ext-real positive non negative V44() V45() finite cardinal Element of NAT

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