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
{ 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
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
{ 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
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
{ 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 {}) 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
{ 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
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
{ 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
{} + 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
{ 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) ) } is set
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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:]
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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
{ 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
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