:: LAPLACE semantic presentation

REAL is set
NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal Element of bool REAL

NAT is non empty non trivial V26() V27() V28() non finite cardinal limit_cardinal 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

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

[:(Seg 2),(Seg 2):] is Relation-like finite set

[1,1] is set
{1,1} is non empty finite V37() set
{{1,1},{1}} is non empty finite V37() set

[1,2] is set
{{1,2},{1}} is non empty finite V37() 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

[:(Seg 1),(Seg 1):] is Relation-like finite set

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

0 ! is V108() Element of REAL

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

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

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

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

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

width A is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of 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

width (DelCol (A,n)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
() -' 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

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

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

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

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

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

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

width (DelLine (K,A)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT

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

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

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

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

width x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of 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

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

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

len x is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of 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 () 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

{ 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
[:(),():] is Relation-like finite set

{ } is set
X is set
X is set

card () is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ()) ! 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))

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

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

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

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

j is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of 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 (X + 2)) \ (Seg x)) is finite 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
() \ (x " Laa) is finite Element of bool ()

((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa) is finite Element of bool (finSeg (X + 2))
(() \ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa)) is finite set
i .: ((() \ (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
() /\ (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) /\ () is finite set
() \ ((x " Laa) /\ ()) is finite Element of bool ()
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
(() /\ (x " Laa)) \/ (((finSeg (X + 2)) \ (Seg x)) /\ (x " Laa)) is finite set
(dom x) /\ (x " Laa) is set

card (finSeg j9) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card ((() \ (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 (() \ ((x " Laa) /\ ())) 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 (() \ ((x " Laa) /\ ()))) + (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 () is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
card ((x " Laa) /\ ()) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card ()) - (card ((x " Laa) /\ ())) is V108() V109() V110() set
((card ()) - (card ((x " Laa) /\ ()))) + (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
() /\ y is finite set
card (() /\ y) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(card (() /\ y)) + (card (finSeg j9)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((card (() /\ y)) + (card (finSeg j9))) - (card ()) is V108() V109() V110() set
y /\ () is finite set
card (y /\ ()) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(((card (() /\ y)) + (card (finSeg j9))) - (card ())) + (card (y /\ ())) is V108() V109() V110() set
2 * (card (() /\ y)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(2 * (card (() /\ y))) + (card (finSeg j9)) is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((2 * (card (() /\ y))) + (card (finSeg j9))) - (card ()) is V108() V109() V110() set
(2 * (card (() /\ y))) + j9 is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
((2 * (card (() /\ y))) + j9) - (card ()) is V108() V109() V110() set
((2 * (card (() /\ 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 (() /\ y))) + Q is V26() V27() V28() V32() finite cardinal V108() V109() V110() ext-real non negative Element of NAT
(K,(),(- (1_ K)),((2 * (card (() /\ y))) + Q)) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * (card (() /\ y)))) is Element of the carrier of K
(K,(),(- (1_ K)),Q) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * (card (() /\ y)))) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(),(- (1_ K)),(2 * (card (() /\ y)))),(K,(),(- (1_ K)),Q)) is Element of the carrier of K
(1_ K) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((1_ K),(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,(),(- (1_ K)),(2 * z)) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * z)) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(),(- (1_ K)),(2 * z)),(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,(),(- (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 ()) + (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 ()) + (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) - (card (finSeg j9)) is V108() V109() V110() set
(((card ()) + (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 ()) 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 ()) 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,(),(- (1_ K)),((2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y))) + Q)) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))) is Element of the carrier of K
(K,(),(- (1_ K)),Q) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(),(- (1_ K)),(2 * (card (((finSeg (X + 2)) \ (Seg x)) /\ y)))),(K,(),(- (1_ K)),Q)) is Element of the carrier of K
(1_ K) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((1_ K),(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,(),(- (1_ K)),(2 * ProjD)) is Element of the carrier of K
(K,(),(- (1_ K)),(2 * ProjD)) * (K,(),(- (1_ K)),Q) is Element of the carrier of K
the multF of K . ((K,(),(- (1_ K)),(2 * ProjD)),(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,(),(- (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

{ 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

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

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

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

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

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