REAL is set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is cup-closed diff-closed preBoolean set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() ext-real non positive non negative set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal set
bool NAT is non trivial cup-closed diff-closed preBoolean non finite set
bool NAT is non trivial cup-closed diff-closed preBoolean non finite set
Fin NAT is non empty cup-closed diff-closed preBoolean set
COMPLEX is set
1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
2 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
RAT is set
INT is set
[:COMPLEX,COMPLEX:] is Relation-like set
bool [:COMPLEX,COMPLEX:] is cup-closed diff-closed preBoolean set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is cup-closed diff-closed preBoolean set
[:REAL,REAL:] is Relation-like set
bool [:REAL,REAL:] is cup-closed diff-closed preBoolean set
[:[:REAL,REAL:],REAL:] is Relation-like set
bool [:[:REAL,REAL:],REAL:] is cup-closed diff-closed preBoolean set
[:RAT,RAT:] is Relation-like set
bool [:RAT,RAT:] is cup-closed diff-closed preBoolean set
[:[:RAT,RAT:],RAT:] is Relation-like set
bool [:[:RAT,RAT:],RAT:] is cup-closed diff-closed preBoolean set
[:INT,INT:] is Relation-like set
bool [:INT,INT:] is cup-closed diff-closed preBoolean set
[:[:INT,INT:],INT:] is Relation-like set
bool [:[:INT,INT:],INT:] is cup-closed diff-closed preBoolean set
[:NAT,NAT:] is Relation-like non trivial non finite set
[:[:NAT,NAT:],NAT:] is Relation-like non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non trivial cup-closed diff-closed preBoolean non finite set
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() ext-real non positive non negative Element of NAT
3 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Seg 1 is non empty trivial finite 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V37() 1 -element set
Seg 2 is non empty finite 2 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V37() set
idseq 2 is Relation-like NAT -defined Function-like finite 2 -element FinSequence-like FinSubsequence-like set
id (Seg 2) is Relation-like Seg 2 -defined Seg 2 -valued Function-like one-to-one non empty V14( Seg 2) quasi_total onto bijective finite V112() V114() V115() V119() Element of bool [:(Seg 2),(Seg 2):]
[:(Seg 2),(Seg 2):] is Relation-like finite set
bool [:(Seg 2),(Seg 2):] is cup-closed diff-closed preBoolean finite V37() set
<*1,2*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
<*1*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,1] is set
{1,1} is non empty finite V37() set
{{1,1},{1}} is non empty finite V37() set
{[1,1]} is Relation-like Function-like constant non empty trivial finite 1 -element set
<*2*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,2] is set
{{1,2},{1}} is non empty finite V37() set
{[1,2]} is Relation-like Function-like constant non empty trivial finite 1 -element set
K139(<*1*>,<*2*>) is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
1 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
union {} is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative 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 Function-like one-to-one non empty V14( Seg 1) quasi_total onto bijective finite V112() V114() V115() V119() Element of bool [:(Seg 1),(Seg 1):]
[:(Seg 1),(Seg 1):] is Relation-like finite set
bool [:(Seg 1),(Seg 1):] is cup-closed diff-closed preBoolean finite V37() set
{(idseq 1)} is functional non empty trivial finite V37() 1 -element set
id {} is Relation-like non-empty empty-yielding {} -defined {} -valued Function-like one-to-one constant functional empty V14( {} ) V26() V27() V28() V30() V31() V32() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V108() V109() V110() V112() V114() V115() V119() ext-real non positive non negative set
<*2,1*> is Relation-like NAT -defined Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like set
K139(<*2*>,<*1*>) is Relation-like NAT -defined Function-like non empty finite 1 + 1 -element FinSequence-like FinSubsequence-like set
K206(NAT,2,1) is Relation-like NAT -defined NAT -valued Function-like non empty finite 2 -element FinSequence-like FinSubsequence-like FinSequence of NAT
0 ! is V108() Element of REAL
n is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom n is finite Element of bool NAT
len n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(len n) -' 1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
DelLine (,n) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (DelLine (,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
A + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
x -' 1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
b is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of x,x, the carrier of n
dom b is finite Element of bool NAT
Deleting (b,K,A) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
DelLine (b,K) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
DelCol ((DelLine (b,K)),A) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len (Deleting (b,K,A)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len (DelLine (b,K)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
K is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital doubleLoopStr
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
A is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
width A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (width A) is finite width A -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width A ) } is set
DelCol (A,n) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
width (DelCol (A,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(width A) -' 1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len (DelCol (A,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
rng (DelCol (A,n)) is finite set
b is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom (DelCol (A,n)) is finite Element of bool NAT
X is set
(DelCol (A,n)) . X is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
Seg (len (DelCol (A,n))) is finite len (DelCol (A,n)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (DelCol (A,n)) ) } is set
B is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom A is finite Element of bool NAT
Line (A,B) is Relation-like NAT -defined the carrier of K -valued Function-like finite width A -element FinSequence-like FinSubsequence-like Element of (width A) -tuples_on the carrier of K
(width A) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
{ b1 where b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of K * : len b1 = width A } is set
DelLine (,(Line (A,B))) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len (Line (A,B)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom (Line (A,B)) is finite width A -element Element of bool NAT
n is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital doubleLoopStr
the carrier of n is non empty non trivial set
the carrier of n * is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
K is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
len K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
width K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
DelLine (K,A) is Relation-like NAT -defined the carrier of n * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of n *
width (DelLine (K,A)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom K is finite Element of bool NAT
DelLine (,K) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular set
len (DelLine (,K)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
x + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
dom (DelLine (,K)) is finite Element of bool NAT
(DelLine (K,A)) . x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (DelLine (,K)) is finite set
rng K is finite set
Line ((DelLine (K,A)),x) is Relation-like NAT -defined the carrier of n -valued Function-like finite width (DelLine (K,A)) -element FinSequence-like FinSubsequence-like Element of (width (DelLine (K,A))) -tuples_on the carrier of n
(width (DelLine (K,A))) -tuples_on the carrier of n is functional non empty FinSequence-membered FinSequenceSet of the carrier of n
{ b1 where b1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like Element of the carrier of n * : len b1 = width (DelLine (K,A)) } is set
len (Line ((DelLine (K,A)),x)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom K is finite Element of bool NAT
dom K is finite Element of bool NAT
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
K -' 1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
A is non empty non degenerated non trivial right_complementable almost_left_invertible V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital doubleLoopStr
the carrier of A is non empty non trivial set
the carrier of A * is functional non empty FinSequence-membered FinSequenceSet of the carrier of A
x is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of A
width x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (width x) is finite width x -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= width x ) } is set
b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
Deleting (x,b,n) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
DelLine (x,b) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
DelCol ((DelLine (x,b)),n) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
width (Deleting (x,b,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom x is finite Element of bool NAT
len (Deleting (x,b,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
len x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
width (DelLine (x,b)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom x is finite Element of bool NAT
len x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
dom x is finite Element of bool NAT
n is non empty multMagma
the carrier of n is non empty set
[: the carrier of n,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of n,NAT:], the carrier of n:] is Relation-like non trivial non finite set
bool [:[: the carrier of n,NAT:], the carrier of n:] is non trivial cup-closed diff-closed preBoolean non finite set
K is Relation-like [: the carrier of n,NAT:] -defined the carrier of n -valued Function-like V14([: the carrier of n,NAT:]) quasi_total Element of bool [:[: the carrier of n,NAT:], the carrier of n:]
A is Element of the carrier of n
x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
K . (A,x) is set
b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
K . (A,b) is Element of the carrier of n
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
Permutations n is non empty permutational set
len (Permutations n) is non empty V26() V27() V28() cardinal set
n ! is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
finSeg A is finite A -element Element of Fin NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= A ) } is set
[:(finSeg A),(finSeg A):] is Relation-like finite set
bool [:(finSeg A),(finSeg A):] is cup-closed diff-closed preBoolean finite V37() set
{ b1 where b1 is Relation-like finSeg A -defined finSeg A -valued Function-like V14( finSeg A) quasi_total finite Element of bool [:(finSeg A),(finSeg A):] : b1 is Relation-like finSeg A -defined finSeg A -valued Function-like one-to-one V14( finSeg A) quasi_total onto bijective finite Element of bool [:(finSeg A),(finSeg A):] } is set
X is set
X is set
B is Relation-like finSeg A -defined finSeg A -valued Function-like V14( finSeg A) quasi_total finite Element of bool [:(finSeg A),(finSeg A):]
card (finSeg A) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card (finSeg A)) ! is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
n + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Seg (n + 1) is non empty finite n + 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n + 1 ) } is set
Permutations (n + 1) is non empty permutational set
len (Permutations (n + 1)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (len (Permutations (n + 1))) is finite len (Permutations (n + 1)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (n + 1)) ) } is set
n ! is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{ b1 where b1 is Relation-like Seg (len (Permutations (n + 1))) -defined Seg (len (Permutations (n + 1))) -valued Function-like one-to-one V14( Seg (len (Permutations (n + 1)))) quasi_total onto bijective finite Element of Permutations (n + 1) : b1 . K = A } is set
len { b1 where b1 is Relation-like Seg (len (Permutations (n + 1))) -defined Seg (len (Permutations (n + 1))) -valued Function-like one-to-one V14( Seg (len (Permutations (n + 1)))) quasi_total onto bijective finite Element of Permutations (n + 1) : b1 . K = A } is V26() V27() V28() cardinal set
x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
x + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
finSeg (x + 1) is non empty finite x + 1 -element Element of Fin NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= x + 1 ) } is set
{A} is non empty trivial finite V37() 1 -element set
(finSeg (x + 1)) \ {A} is finite Element of bool (finSeg (x + 1))
bool (finSeg (x + 1)) is cup-closed diff-closed preBoolean finite V37() set
((finSeg (x + 1)) \ {A}) \/ {A} is non empty finite set
{K} is non empty trivial finite V37() 1 -element set
(finSeg (x + 1)) \ {K} is finite Element of bool (finSeg (x + 1))
Permutations (x + 1) is non empty permutational set
len (Permutations (x + 1)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (len (Permutations (x + 1))) is finite len (Permutations (x + 1)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= len (Permutations (x + 1)) ) } is set
{ b1 where b1 is Relation-like Seg (len (Permutations (x + 1))) -defined Seg (len (Permutations (x + 1))) -valued Function-like one-to-one V14( Seg (len (Permutations (x + 1)))) quasi_total onto bijective finite Element of Permutations (x + 1) : b1 . K = A } is set
((finSeg (x + 1)) \ {K}) \/ {K} is non empty finite set
[:(((finSeg (x + 1)) \ {K}) \/ {K}),(((finSeg (x + 1)) \ {A}) \/ {A}):] is Relation-like finite set
bool [:(((finSeg (x + 1)) \ {K}) \/ {K}),(((finSeg (x + 1)) \ {A}) \/ {A}):] is cup-closed diff-closed preBoolean finite V37() set
{ b1 where b1 is Relation-like ((finSeg (x + 1)) \ {K}) \/ {K} -defined ((finSeg (x + 1)) \ {A}) \/ {A} -valued Function-like non empty V14(((finSeg (x + 1)) \ {K}) \/ {K}) quasi_total finite Element of bool [:(((finSeg (x + 1)) \ {K}) \/ {K}),(((finSeg (x + 1)) \ {A}) \/ {A}):] : ( b1 is one-to-one & b1 . K = A ) } is set
j is set
[:(finSeg (x + 1)),(finSeg (x + 1)):] is Relation-like finite set
bool [:(finSeg (x + 1)),(finSeg (x + 1)):] is cup-closed diff-closed preBoolean finite V37() set
COL is Relation-like finSeg (x + 1) -defined finSeg (x + 1) -valued Function-like non empty V14( finSeg (x + 1)) quasi_total finite Element of bool [:(finSeg (x + 1)),(finSeg (x + 1)):]
COL . K is set
card (finSeg (x + 1)) is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
j is set
COL is Relation-like Seg (len (Permutations (x + 1))) -defined Seg (len (Permutations (x + 1))) -valued Function-like one-to-one V14( Seg (len (Permutations (x + 1)))) quasi_total onto bijective finite Element of Permutations (x + 1)
COL . K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
[:(finSeg (x + 1)),(finSeg (x + 1)):] is Relation-like finite set
bool [:(finSeg (x + 1)),(finSeg (x + 1)):] is cup-closed diff-closed preBoolean finite V37() set
L is Relation-like finSeg (x + 1) -defined finSeg (x + 1) -valued Function-like one-to-one non empty V14( finSeg (x + 1)) quasi_total onto bijective finite Element of bool [:(finSeg (x + 1)),(finSeg (x + 1)):]
L . K is set
card (finSeg (x + 1)) is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
card ((finSeg (x + 1)) \ {A}) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ((finSeg (x + 1)) \ {A})) + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
card ((finSeg (x + 1)) \ {K}) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ((finSeg (x + 1)) \ {K})) + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
[:((finSeg (x + 1)) \ {K}),((finSeg (x + 1)) \ {A}):] is Relation-like finite set
bool [:((finSeg (x + 1)) \ {K}),((finSeg (x + 1)) \ {A}):] is cup-closed diff-closed preBoolean finite V37() set
{ b1 where b1 is Relation-like (finSeg (x + 1)) \ {K} -defined (finSeg (x + 1)) \ {A} -valued Function-like quasi_total finite Element of bool [:((finSeg (x + 1)) \ {K}),((finSeg (x + 1)) \ {A}):] : b1 is one-to-one } is set
len { b1 where b1 is Relation-like (finSeg (x + 1)) \ {K} -defined (finSeg (x + 1)) \ {A} -valued Function-like quasi_total finite Element of bool [:((finSeg (x + 1)) \ {K}),((finSeg (x + 1)) \ {A}):] : b1 is one-to-one } is V26() V27() V28() cardinal set
(card ((finSeg (x + 1)) \ {A})) ! is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ((finSeg (x + 1)) \ {A})) -' (card ((finSeg (x + 1)) \ {K})) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((card ((finSeg (x + 1)) \ {A})) -' (card ((finSeg (x + 1)) \ {K}))) ! is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((card ((finSeg (x + 1)) \ {A})) !) / (((card ((finSeg (x + 1)) \ {A})) -' (card ((finSeg (x + 1)) \ {K}))) !) is V108() set
((card ((finSeg (x + 1)) \ {A})) !) / 1 is V108() set
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
n + 2 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Permutations (n + 2) is non empty permutational set
len (Permutations (n + 2)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative 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 V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
2Set (Seg (n + 2)) is non empty finite set
Fin (2Set (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 V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital Fanoian doubleLoopStr
the carrier of K is non empty non trivial set
1_ K is Element of the carrier of K
1. K is V52(K) Element of the carrier of K
- (1_ K) is 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 V14([: the carrier of K, the carrier of K:]) 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 set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is cup-closed diff-closed preBoolean set
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like V14([: the carrier of K,NAT:]) quasi_total Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial cup-closed diff-closed preBoolean non finite set
A is Relation-like Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -valued Function-like one-to-one V14( Seg (len (Permutations (n + 2)))) quasi_total onto bijective finite Element of Permutations (n + 2)
Part_sgn (A,K) is Relation-like 2Set (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty V14( 2Set (Seg (n + 2))) quasi_total finite Element of bool [:(2Set (Seg (n + 2))), the carrier of K:]
[:(2Set (Seg (n + 2))), the carrier of K:] is Relation-like set
bool [:(2Set (Seg (n + 2))), the carrier of K:] is cup-closed diff-closed preBoolean set
X is finite Element of Fin (2Set (Seg (n + 2)))
b is finite Element of Fin (2Set (Seg (n + 2)))
{ b1 where b1 is Element of 2Set (Seg (n + 2)) : ( b1 in b & (Part_sgn (A,K)) . b1 = - (1_ K) ) } is set
the multF of K $$ (b,(Part_sgn (A,K))) is Element of the carrier of K
card X is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),(card X)) is Element of the carrier of K
id (Seg (n + 2)) is Relation-like Seg (n + 2) -defined Seg (n + 2) -valued Function-like one-to-one non empty V14( Seg (n + 2)) quasi_total onto bijective finite V112() V114() V115() V119() Element of bool [:(Seg (n + 2)),(Seg (n + 2)):]
[:(Seg (n + 2)),(Seg (n + 2)):] is Relation-like finite set
bool [:(Seg (n + 2)),(Seg (n + 2)):] is cup-closed diff-closed preBoolean finite V37() set
B is Relation-like Seg (len (Permutations (n + 2))) -defined Seg (len (Permutations (n + 2))) -valued Function-like one-to-one V14( Seg (len (Permutations (n + 2)))) quasi_total onto bijective finite Element of Permutations (n + 2)
Part_sgn (B,K) is Relation-like 2Set (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty V14( 2Set (Seg (n + 2))) quasi_total finite Element of bool [:(2Set (Seg (n + 2))), the carrier of K:]
{ b1 where b1 is Element of 2Set (Seg (n + 2)) : ( b1 in b & not (Part_sgn (A,K)) . b1 = (Part_sgn (B,K)) . b1 ) } is set
j is set
(Part_sgn (B,K)) . j is set
N is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
i is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{N,i} is non empty finite V37() set
B . i is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
B . N is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
j is set
N is Element of 2Set (Seg (n + 2))
(Part_sgn (A,K)) . N is Element of the carrier of K
(Part_sgn (B,K)) . N is Element of the carrier of K
j is set
N is Element of 2Set (Seg (n + 2))
(Part_sgn (A,K)) . N is Element of the carrier of K
(Part_sgn (B,K)) . N is Element of the carrier of K
(card X) mod 2 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
2 * j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * j) + {} is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
the multF of K $$ (b,(Part_sgn (B,K))) is Element of the carrier of K
(card X) mod 2 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
2 * j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * j) + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
the multF of K $$ (b,(Part_sgn (B,K))) is Element of the carrier of K
- ( the multF of K $$ (b,(Part_sgn (B,K)))) is Element of the carrier of K
(card X) mod 2 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
n + 2 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Permutations (n + 2) is non empty permutational set
len (Permutations (n + 2)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg (len (Permutations (n + 2))) is finite len (Permutations (n + 2)) -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative 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 V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n + 2 ) } is set
2Set (Seg (n + 2)) is non empty finite set
Fin (2Set (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 V95() unital associative commutative V132() V133() V134() right-distributive left-distributive right_unital well-unital V146() left_unital Fanoian 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 V14([: the carrier of K, the carrier of K:]) 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 set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is cup-closed diff-closed preBoolean set
power K is Relation-like [: the carrier of K,NAT:] -defined the carrier of K -valued Function-like V14([: the carrier of K,NAT:]) quasi_total Element of bool [:[: the carrier of K,NAT:], the carrier of K:]
[: the carrier of K,NAT:] is Relation-like non trivial non finite set
[:[: the carrier of K,NAT:], the carrier of K:] is Relation-like non trivial non finite set
bool [:[: the carrier of K,NAT:], the carrier of K:] is non trivial cup-closed diff-closed preBoolean non finite set
1_ K is Element of the carrier of K
1. K is V52(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 V14( Seg (len (Permutations (n + 2)))) quasi_total onto bijective finite Element of Permutations (n + 2)
Part_sgn (A,K) is Relation-like 2Set (Seg (n + 2)) -defined the carrier of K -valued Function-like non empty V14( 2Set (Seg (n + 2))) quasi_total finite Element of bool [:(2Set (Seg (n + 2))), the carrier of K:]
[:(2Set (Seg (n + 2))), the carrier of K:] is Relation-like set
bool [:(2Set (Seg (n + 2))), the carrier of K:] is cup-closed diff-closed preBoolean set
x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
A . x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{ {b1,x} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,x} in 2Set (Seg (n + 2)) } is set
b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
x + b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
(K,(power K),(- (1_ K)),(x + b)) is Element of the carrier of K
X is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
X + 2 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
finSeg (X + 2) is non empty finite X + 2 -element Element of Fin NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= X + 2 ) } is set
[:(finSeg (X + 2)),(finSeg (X + 2)):] is Relation-like finite set
bool [:(finSeg (X + 2)),(finSeg (X + 2)):] is cup-closed diff-closed preBoolean finite V37() set
i is Relation-like finSeg (X + 2) -defined finSeg (X + 2) -valued Function-like one-to-one non empty V14( finSeg (X + 2)) quasi_total onto bijective finite Element of bool [:(finSeg (X + 2)),(finSeg (X + 2)):]
rng i is non empty finite set
Seg (X + 2) is non empty finite X + 2 -element Element of bool NAT
x - 1 is V108() V109() V110() set
Seg x is finite x -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= x ) } is set
(finSeg (X + 2)) \ (Seg x) is finite Element of bool (finSeg (X + 2))
bool (finSeg (X + 2)) is cup-closed diff-closed preBoolean finite V37() set
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
finSeg j is finite j -element Element of Fin NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= j ) } is set
L is set
2Set (Seg (X + 2)) is non empty finite set
i9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{i9,x} is non empty finite V37() set
L is finite Element of Fin (2Set (Seg (n + 2)))
{ b1 where b1 is Element of 2Set (Seg (n + 2)) : ( b1 in L & (Part_sgn (A,K)) . b1 = - (1_ K) ) } is set
j9 is set
Laa is Element of 2Set (Seg (n + 2))
(Part_sgn (A,K)) . Laa is Element of the carrier of K
dom i is non empty finite Element of bool (finSeg (X + 2))
rng A is finite set
b - 1 is V108() V109() V110() set
(finSeg j) \/ ((finSeg (X + 2)) \ (Seg x)) is finite set
x is Relation-like Function-like set
dom x is set
Laa is finite Element of Fin (2Set (Seg (n + 2)))
x " Laa is set
{x} is non empty trivial finite V37() 1 -element set
(Seg (X + 2)) \ {x} is finite Element of bool NAT
z is set
ProjD is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
z is set
ProjD is set
x . z is set
x . ProjD is set
{ProjD,x} is non empty finite set
{z,x} is non empty finite set
{x,ProjD} is non empty finite set
y is finite set
x .: y is finite set
card (x .: y) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card y is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(finSeg (X + 2)) \ {x} is finite Element of bool (finSeg (X + 2))
z is set
ProjD is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
rng x is set
z is set
ProjD is set
x . ProjD is set
Q1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
x . Q1 is set
{x,Q1} is non empty finite V37() set
(finSeg j) \ (x " Laa) is finite Element of bool (finSeg j)
bool (finSeg j) is cup-closed diff-closed preBoolean finite V37() set
((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa) is finite Element of bool (finSeg (X + 2))
((finSeg j) \ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa)) is finite set
i .: (((finSeg j) \ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa))) is finite set
j9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
Seg j9 is finite j9 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= j9 ) } is set
z is set
ProjD is set
i . ProjD is set
Q1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
x . Q1 is set
A . Q1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{Q1,x} is non empty finite V37() set
(Part_sgn (A,K)) . {Q1,x} is set
Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{Q,x} is non empty finite V37() set
j9 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
x . Q1 is set
Q is Element of 2Set (Seg (n + 2))
(Part_sgn (A,K)) . Q is Element of the carrier of K
{x,Q1} is non empty finite V37() set
i . x is set
A . Q1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
j9 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
the multF of K $$ (L,(Part_sgn (A,K))) is Element of the carrier of K
(finSeg j) /\ (x " Laa) is finite set
Q is set
Q19 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j9 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Pf is set
i . Pf is set
x . Pf is set
{Pf,x} is non empty finite set
2Set (Seg (X + 2)) is non empty finite set
domf is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{domf,x} is non empty finite V37() set
(Part_sgn (A,K)) . {domf,x} is set
k is Element of 2Set (Seg (n + 2))
(Part_sgn (A,K)) . k is Element of the carrier of K
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
(Part_sgn (A,K)) . {domf,x} is set
(x " Laa) /\ (finSeg j) is finite set
(finSeg j) \ ((x " Laa) /\ (finSeg j)) is finite Element of bool (finSeg j)
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Q is set
Q19 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{Q19,x} is non empty finite V37() set
x . Q19 is set
((finSeg j) /\ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa)) is finite set
(dom x) /\ (x " Laa) is set
finSeg j9 is finite j9 -element Element of Fin NAT
card (finSeg j9) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card (((finSeg j) \ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa))) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card ((finSeg j) \ ((x " Laa) /\ (finSeg j))) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ((finSeg j) \ ((x " Laa) /\ (finSeg j)))) + (card (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa))) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card (finSeg j) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card ((x " Laa) /\ (finSeg j)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card (finSeg j)) - (card ((x " Laa) /\ (finSeg j))) is V108() V109() V110() set
((card (finSeg j)) - (card ((x " Laa) /\ (finSeg j)))) + (card (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa))) is V108() V109() V110() set
b - x is V108() V109() V110() set
card Laa is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(finSeg j) /\ y is finite set
card ((finSeg j) /\ y) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ((finSeg j) /\ y)) + (card (finSeg j9)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((card ((finSeg j) /\ y)) + (card (finSeg j9))) - (card (finSeg j)) is V108() V109() V110() set
y /\ (finSeg j) is finite set
card (y /\ (finSeg j)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(((card ((finSeg j) /\ y)) + (card (finSeg j9))) - (card (finSeg j))) + (card (y /\ (finSeg j))) is V108() V109() V110() set
2 * (card ((finSeg j) /\ y)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * (card ((finSeg j) /\ y))) + (card (finSeg j9)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((2 * (card ((finSeg j) /\ y))) + (card (finSeg j9))) - (card (finSeg j)) is V108() V109() V110() set
(2 * (card ((finSeg j) /\ y))) + j9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((2 * (card ((finSeg j) /\ y))) + j9) - (card (finSeg j)) is V108() V109() V110() set
((2 * (card ((finSeg j) /\ y))) + j9) - j is V108() V109() V110() set
Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * (card ((finSeg j) /\ y))) + Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),((2 * (card ((finSeg j) /\ y))) + Q)) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * (card ((finSeg j) /\ y)))) is Element of the carrier of K
(K,(power K),(- (1_ K)),Q) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * (card ((finSeg j) /\ y)))) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(power K),(- (1_ K)),(2 * (card ((finSeg j) /\ y)))),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
(1_ K) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((1_ K),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
z is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
2 * z is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),(2 * z)) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * z)) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(power K),(- (1_ K)),(2 * z)),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
2 * x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * x) + Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),((2 * x) + Q)) is Element of the carrier of K
x - b is V108() V109() V110() set
card Laa is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((finSeg (X + 2)) \ (Seg x)) /\ y is finite Element of bool (finSeg (X + 2))
card (((finSeg (X + 2)) \ (Seg x)) /\ y) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card (finSeg j)) + (card (((finSeg (X + 2)) \ (Seg x)) /\ y)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((card (finSeg j)) + (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - (card (finSeg j9)) is V108() V109() V110() set
(((card (finSeg j)) + (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - (card (finSeg j9))) + (card (((finSeg (X + 2)) \ (Seg x)) /\ y)) is V108() V109() V110() set
2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - (card (finSeg j9)) is V108() V109() V110() set
((2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - (card (finSeg j9))) + (card (finSeg j)) is V108() V109() V110() set
(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - j9 is V108() V109() V110() set
((2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - j9) + (card (finSeg j)) is V108() V109() V110() set
((2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - j9) + j is V108() V109() V110() set
Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) + Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),((2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) + Q)) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))) is Element of the carrier of K
(K,(power K),(- (1_ K)),Q) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(power K),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
(1_ K) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((1_ K),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
ProjD is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
2 * ProjD is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),(2 * ProjD)) is Element of the carrier of K
(K,(power K),(- (1_ K)),(2 * ProjD)) * (K,(power K),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(power K),(- (1_ K)),(2 * ProjD)),(K,(power K),(- (1_ K)),Q)) is Element of the carrier of K
2 * b is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * b) + Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(power K),(- (1_ K)),((2 * b) + Q)) is Element of the carrier of K
n is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
n + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Seg (n + 1) is non empty finite n + 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n + 1 ) } is set
Seg n is finite n -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= n ) } is set
2Set (Seg n) is set
2Set (Seg (n + 1)) is set
[:(2Set (Seg n)),(2Set (Seg (n + 1))):] is Relation-like set
bool [:(2Set (Seg n)),(2Set (Seg (n + 1))):] is cup-closed diff-closed preBoolean set
K is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{ {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } is set
(2Set (Seg (n + 1))) \ { {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } is Element of bool (2Set (Seg (n + 1)))
bool (2Set (Seg (n + 1))) is cup-closed diff-closed preBoolean set
i is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{i,j} is non empty finite V37() set
N is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{N,K} is non empty finite V37() set
{K,N} is non empty finite V37() set
j is set
N is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
i is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{N,i} is non empty finite V37() set
i + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
i is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
i + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
Seg (i + 1) is non empty finite i + 1 -element Element of bool NAT
{ b1 where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : ( 1 <= b1 & b1 <= i + 1 ) } is set
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
COL is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
L is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{COL,L} is non empty finite V37() set
L + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{COL,(L + 1)} is non empty finite V37() set
COL + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{(COL + 1),(L + 1)} is non empty finite V37() set
{N,(i + 1)} is non empty finite V37() set
COL is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
L is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{COL,L} is non empty finite V37() set
L + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{COL,(L + 1)} is non empty finite V37() set
COL + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{(COL + 1),(L + 1)} is non empty finite V37() set
N + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{(N + 1),(i + 1)} is non empty finite V37() set
COL is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
L is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{COL,L} is non empty finite V37() set
L + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{COL,(L + 1)} is non empty finite V37() set
COL + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{(COL + 1),(L + 1)} is non empty finite V37() set
[:(2Set (Seg n)),((2Set (Seg (n + 1))) \ { {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } ):] is Relation-like set
bool [:(2Set (Seg n)),((2Set (Seg (n + 1))) \ { {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } ):] is cup-closed diff-closed preBoolean set
i is Relation-like 2Set (Seg n) -defined (2Set (Seg (n + 1))) \ { {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } -valued Function-like quasi_total Element of bool [:(2Set (Seg n)),((2Set (Seg (n + 1))) \ { {b1,K} where b1 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT : {b1,K} in 2Set (Seg (n + 1)) } ):]
N is set
j is non empty set
[:(2Set (Seg n)),j:] is Relation-like set
bool [:(2Set (Seg n)),j:] is cup-closed diff-closed preBoolean set
N is Relation-like 2Set (Seg n) -defined j -valued Function-like V14( 2Set (Seg n)) quasi_total Element of bool [:(2Set (Seg n)),j:]
rng N is set
i is set
j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
COL is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative set
{j,COL} is non empty finite V37() set
j - 1 is V108() V109() V110() set
COL - 1 is V108() V109() V110() set
dom N is Element of bool (2Set (Seg n))
bool (2Set (Seg n)) is cup-closed diff-closed preBoolean set
Laa is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
j9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{Laa,j9} is non empty finite V37() set
N . i is set
i9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
i9 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
dom N is Element of bool (2Set (Seg n))
bool (2Set (Seg n)) is cup-closed diff-closed preBoolean set
Laa is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
{Laa,i9} is non empty finite V37() set
N . {Laa,i9} is set
{Laa,(i9 + 1)} is non empty finite V37() set
L is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
L + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
dom N is Element of bool (2Set (Seg n))
bool (2Set (Seg n)) is cup-closed diff-closed preBoolean set
i9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
i9 + 1 is non empty V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real positive non negative Element of NAT
{L,i9} is non empty finite V37() set
N . {L,i9} is set
{(L + 1),(i9 + 1)} is non empty finite V37() set
dom N is Element of bool (2Set (Seg n))
bool (2Set (Seg n)) is cup-closed diff-closed preBoolean set
i is Relation-like 2Set (Seg n) -defined 2Set (Seg (n + 1)) -valued Function-like quasi_total Element of bool [:(2Set (Seg n)),(2Set (Seg (n + 1))):]