REAL is set
NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal Element of bool REAL
bool REAL is set
K704() is strict algebraic-closed doubleLoopStr
the carrier of K704() is set
NAT is non empty non trivial V25() V26() V27() non finite cardinal limit_cardinal set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set
K95(NAT) is V24() set
INT is set
COMPLEX is set
RAT is set
{} is Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element FinSequence-membered V46() ext-real non positive non negative V165() set
the Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element FinSequence-membered V46() ext-real non positive non negative V165() set is Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element FinSequence-membered V46() ext-real non positive non negative V165() set
2 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
0 is Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element FinSequence-membered V46() ext-real non positive non negative V165() Element of NAT
K516(0,1,2) is finite set
[:K516(0,1,2),K516(0,1,2):] is finite set
[:[:K516(0,1,2),K516(0,1,2):],K516(0,1,2):] is finite set
bool [:[:K516(0,1,2),K516(0,1,2):],K516(0,1,2):] is finite V36() set
bool [:K516(0,1,2),K516(0,1,2):] is finite V36() set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
K652() is non empty strict multMagma
the carrier of K652() is non empty set
<REAL,+> is non empty strict unital Group-like associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V232() multMagma
K658() is non empty strict associative commutative left-cancelable right-cancelable V232() SubStr of <REAL,+>
<NAT,+> is non empty strict unital associative commutative left-cancelable right-cancelable V232() uniquely-decomposable SubStr of K658()
<REAL,*> is non empty strict unital associative commutative multMagma
<NAT,*> is non empty strict unital associative commutative uniquely-decomposable SubStr of <REAL,*>
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is non trivial non finite set
[:[:NAT,NAT:],NAT:] is non trivial non finite set
bool [:[:NAT,NAT:],NAT:] is non trivial non finite set
3 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
card {} is Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element FinSequence-membered V46() ext-real non positive non negative V165() set
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
V1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V1 -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
V2 is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V2 is non empty non trivial set
the carrier of V2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V2
A is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of V2 *
Indices A is set
B is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of V2 *
A + B is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of V2 *
L is Relation-like NAT -defined NAT -valued Function-like finite K -element FinSequence-like FinSubsequence-like V177() Element of K -tuples_on NAT
rng L is finite set
F is Relation-like NAT -defined NAT -valued Function-like finite V1 -element FinSequence-like FinSubsequence-like V177() Element of V1 -tuples_on NAT
rng F is finite set
[:(rng L),(rng F):] is finite set
Segm ((A + B),L,F) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,V1, the carrier of V2
Segm (A,L,F) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,V1, the carrier of V2
Segm (B,L,F) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,V1, the carrier of V2
(Segm (A,L,F)) + (Segm (B,L,F)) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,V1, the carrier of V2
Indices (Segm (A,L,F)) is set
Indices (Segm (B,L,F)) is set
f is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
D is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[f,D] is set
{f,D} is non empty finite V36() set
{f} is non empty trivial finite V36() 1 -element set
{{f,D},{f}} is non empty finite V36() set
Indices (Segm ((A + B),L,F)) is set
L . f is set
F . D is set
[(L . f),(F . D)] is set
{(L . f),(F . D)} is non empty finite set
{(L . f)} is non empty trivial finite 1 -element set
{{(L . f),(F . D)},{(L . f)}} is non empty finite V36() set
(Segm ((A + B),L,F)) * (f,D) is Element of the carrier of V2
C is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
FA is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
(A + B) * (C,FA) is Element of the carrier of V2
A * (C,FA) is Element of the carrier of V2
B * (C,FA) is Element of the carrier of V2
(A * (C,FA)) + (B * (C,FA)) is Element of the carrier of V2
(Segm (A,L,F)) * (f,D) is Element of the carrier of V2
((Segm (A,L,F)) * (f,D)) + (B * (C,FA)) is Element of the carrier of V2
(Segm (B,L,F)) * (f,D) is Element of the carrier of V2
((Segm (A,L,F)) * (f,D)) + ((Segm (B,L,F)) * (f,D)) is Element of the carrier of V2
((Segm (A,L,F)) + (Segm (B,L,F))) * (f,D) is Element of the carrier of V2
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg K is finite K -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
V1 is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V1 is non empty non trivial set
1. (V1,K) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of V1
the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
V2 is finite without_zero Element of bool NAT
Segm ((1. (V1,K)),V2,V2) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card V2, card V2, the carrier of V1
card V2 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Sgm V2 is Relation-like NAT -defined NAT -valued Function-like finite card V2 -element FinSequence-like FinSubsequence-like V177() Element of (card V2) -tuples_on NAT
(card V2) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Segm ((1. (V1,K)),(Sgm V2),(Sgm V2)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card V2, card V2, the carrier of V1
1. (V1,(card V2)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card V2, card V2, the carrier of V1
L is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
F is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
[L,F] is set
{L,F} is non empty finite V36() set
{L} is non empty trivial finite V36() 1 -element set
{{L,F},{L}} is non empty finite V36() set
Indices (1. (V1,(card V2))) is set
rng (Sgm V2) is finite set
(Sgm V2) . L is set
(Sgm V2) . F is set
Indices (Segm ((1. (V1,K)),V2,V2)) is set
(Segm ((1. (V1,K)),V2,V2)) * (L,F) is Element of the carrier of V1
f is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
D is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
(1. (V1,K)) * (f,D) is Element of the carrier of V1
Indices (1. (V1,K)) is set
[:(Seg K),(Seg K):] is finite set
[:V2,V2:] is finite set
[((Sgm V2) . L),((Sgm V2) . F)] is set
{((Sgm V2) . L),((Sgm V2) . F)} is non empty finite set
{((Sgm V2) . L)} is non empty trivial finite 1 -element set
{{((Sgm V2) . L),((Sgm V2) . F)},{((Sgm V2) . L)}} is non empty finite V36() set
Seg (card V2) is finite card V2 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= card V2 ) } is set
[:(Seg (card V2)),(Seg (card V2)):] is finite set
dom (Sgm V2) is finite card V2 -element Element of bool NAT
1_ V1 is Element of the carrier of V1
1. V1 is V65(V1) Element of the carrier of V1
the OneF of V1 is Element of the carrier of V1
(1. (V1,(card V2))) * (L,F) is Element of the carrier of V1
0. V1 is V65(V1) Element of the carrier of V1
the ZeroF of V1 is Element of the carrier of V1
K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed 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
V1 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
Indices V1 is set
V2 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
V1 + V2 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of K *
A is finite without_zero Element of bool NAT
B is finite without_zero Element of bool NAT
[:A,B:] is finite set
Segm ((V1 + V2),A,B) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
card A is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
card B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Sgm A is Relation-like NAT -defined NAT -valued Function-like finite card A -element FinSequence-like FinSubsequence-like V177() Element of (card A) -tuples_on NAT
(card A) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Sgm B is Relation-like NAT -defined NAT -valued Function-like finite card B -element FinSequence-like FinSubsequence-like V177() Element of (card B) -tuples_on NAT
(card B) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Segm ((V1 + V2),(Sgm A),(Sgm B)) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
Segm (V1,A,B) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
Segm (V1,(Sgm A),(Sgm B)) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
Segm (V2,A,B) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
Segm (V2,(Sgm A),(Sgm B)) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
(Segm (V1,A,B)) + (Segm (V2,A,B)) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card A, card B, the carrier of K
rng (Sgm B) is finite set
L is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg L is finite L -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= L ) } is set
rng (Sgm A) is finite set
L is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg L is finite L -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= L ) } is set
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg K is finite K -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
K -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
V1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V2 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
A is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed 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
B 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
L 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
B + L 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
Delete ((B + L),V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
Delete (B,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
Delete (L,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
(Delete (B,V1,V2)) + (Delete (L,V1,V2)) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
{V1} is non empty trivial finite V36() 1 -element Element of bool NAT
(Seg K) \ {V1} is finite without_zero Element of bool NAT
{V2} is non empty trivial finite V36() 1 -element Element of bool NAT
(Seg K) \ {V2} is finite without_zero Element of bool NAT
[:((Seg K) \ {V1}),((Seg K) \ {V2}):] is finite set
[:(Seg K),(Seg K):] is finite set
Indices B is set
Deleting ((B + L),V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
Segm ((B + L),((Seg K) \ {V1}),((Seg K) \ {V2})) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
card ((Seg K) \ {V1}) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
card ((Seg K) \ {V2}) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Sgm ((Seg K) \ {V1}) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg K) \ {V1}) -element FinSequence-like FinSubsequence-like V177() Element of (card ((Seg K) \ {V1})) -tuples_on NAT
(card ((Seg K) \ {V1})) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Sgm ((Seg K) \ {V2}) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg K) \ {V2}) -element FinSequence-like FinSubsequence-like V177() Element of (card ((Seg K) \ {V2})) -tuples_on NAT
(card ((Seg K) \ {V2})) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Segm ((B + L),(Sgm ((Seg K) \ {V1})),(Sgm ((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (B,((Seg K) \ {V1}),((Seg K) \ {V2})) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (B,(Sgm ((Seg K) \ {V1})),(Sgm ((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (L,((Seg K) \ {V1}),((Seg K) \ {V2})) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (L,(Sgm ((Seg K) \ {V1})),(Sgm ((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
(Segm (B,((Seg K) \ {V1}),((Seg K) \ {V2}))) + (Segm (L,((Seg K) \ {V1}),((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Deleting (B,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
(Deleting (B,V1,V2)) + (Segm (L,((Seg K) \ {V1}),((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
Deleting (L,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
(Deleting (B,V1,V2)) + (Deleting (L,V1,V2)) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
(Delete (B,V1,V2)) + (Deleting (L,V1,V2)) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg K is finite K -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= K ) } is set
K -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
V1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V2 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
A is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed 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
B is Element of the carrier of A
L 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
B * L 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
Delete ((B * L),V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
Delete (L,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
B * (Delete (L,V1,V2)) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K -' 1,K -' 1, the carrier of A
{V1} is non empty trivial finite V36() 1 -element Element of bool NAT
(Seg K) \ {V1} is finite without_zero Element of bool NAT
{V2} is non empty trivial finite V36() 1 -element Element of bool NAT
(Seg K) \ {V2} is finite without_zero Element of bool NAT
[:((Seg K) \ {V1}),((Seg K) \ {V2}):] is finite set
[:(Seg K),(Seg K):] is finite set
Indices L is set
Deleting ((B * L),V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
Segm ((B * L),((Seg K) \ {V1}),((Seg K) \ {V2})) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
card ((Seg K) \ {V1}) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
card ((Seg K) \ {V2}) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Sgm ((Seg K) \ {V1}) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg K) \ {V1}) -element FinSequence-like FinSubsequence-like V177() Element of (card ((Seg K) \ {V1})) -tuples_on NAT
(card ((Seg K) \ {V1})) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Sgm ((Seg K) \ {V2}) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg K) \ {V2}) -element FinSequence-like FinSubsequence-like V177() Element of (card ((Seg K) \ {V2})) -tuples_on NAT
(card ((Seg K) \ {V2})) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Segm ((B * L),(Sgm ((Seg K) \ {V1})),(Sgm ((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (L,((Seg K) \ {V1}),((Seg K) \ {V2})) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Segm (L,(Sgm ((Seg K) \ {V1})),(Sgm ((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
B * (Segm (L,((Seg K) \ {V1}),((Seg K) \ {V2}))) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg K) \ {V1}), card ((Seg K) \ {V2}), the carrier of A
Deleting (L,V1,V2) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
B * (Deleting (L,V1,V2)) is Relation-like NAT -defined the carrier of A * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of A *
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
Seg V1 is finite V1 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= V1 ) } is set
V1 -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
V2 is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
1. (V2,V1) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V1,V1, the carrier of V2
the carrier of V2 is non empty non trivial set
the carrier of V2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V2
Delete ((1. (V2,V1)),K,K) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V1 -' 1,V1 -' 1, the carrier of V2
1. (V2,(V1 -' 1)) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V1 -' 1,V1 -' 1, the carrier of V2
V1 - 1 is V46() ext-real V165() set
card (Seg V1) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(V1 -' 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
{K} is non empty trivial finite V36() 1 -element Element of bool NAT
(Seg V1) \ {K} is finite without_zero Element of bool NAT
card ((Seg V1) \ {K}) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Deleting ((1. (V2,V1)),K,K) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular FinSequence of the carrier of V2 *
Segm ((1. (V2,V1)),((Seg V1) \ {K}),((Seg V1) \ {K})) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg V1) \ {K}), card ((Seg V1) \ {K}), the carrier of V2
Sgm ((Seg V1) \ {K}) is Relation-like NAT -defined NAT -valued Function-like finite card ((Seg V1) \ {K}) -element FinSequence-like FinSubsequence-like V177() Element of (card ((Seg V1) \ {K})) -tuples_on NAT
(card ((Seg V1) \ {K})) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
Segm ((1. (V2,V1)),(Sgm ((Seg V1) \ {K})),(Sgm ((Seg V1) \ {K}))) is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of card ((Seg V1) \ {K}), card ((Seg V1) \ {K}), the carrier of V2
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V1 is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V1 is non empty non trivial set
the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
[:NAT, the carrier of V1:] is non trivial non finite set
bool [:NAT, the carrier of V1:] is non trivial non finite set
V2 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V2 + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(V2 + 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
B is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
L is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
(V2 + 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
Seg (V2 + 1) is non empty finite V2 + 1 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= V2 + 1 ) } is set
F is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
F + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
D is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len D is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
D is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len D is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
[(V2 + 1),(F + 1)] is Element of [:NAT,NAT:]
{(V2 + 1),(F + 1)} is non empty finite V36() set
{(V2 + 1)} is non empty trivial finite V36() 1 -element set
{{(V2 + 1),(F + 1)},{(V2 + 1)}} is non empty finite V36() set
[:(Seg (V2 + 1)),(Seg (V2 + 1)):] is finite set
power V1 is Relation-like [: the carrier of V1,NAT:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1,NAT:], the carrier of V1:]
[: the carrier of V1,NAT:] is non trivial non finite set
[:[: the carrier of V1,NAT:], the carrier of V1:] is non trivial non finite set
bool [:[: the carrier of V1,NAT:], the carrier of V1:] is non trivial non finite set
1_ V1 is Element of the carrier of V1
1. V1 is V65(V1) Element of the carrier of V1
the OneF of V1 is Element of the carrier of V1
- (1_ V1) is Element of the carrier of V1
(F + 1) + (V2 + 1) is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))) is Element of the carrier of V1
Delete (L,(V2 + 1),(F + 1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
(V2 + 1) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Delete (B,(V2 + 1),(F + 1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
B * ((V2 + 1),(F + 1)) is Element of the carrier of V1
(B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
L * ((V2 + 1),(F + 1)) is Element of the carrier of V1
(L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
<%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%> is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
Indices L is set
F9 is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len F9 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%> is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
D + (F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>) is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
SA is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len SA is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
len <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%> is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(len F9) + (len <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(V2 + 1) + 2 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
((len F9) + (len <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>)) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
((V2 + 1) + 2) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
V2 + 2 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(V2 + 2) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
((V2 + 2) + 1) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
len (F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
SB is Element of the carrier of V1
eval (SA,SB) is Element of the carrier of V1
SB * L is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
B + (SB * L) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
LaplaceExpL ((B + (SB * L)),(V2 + 1)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(LaplaceExpL ((B + (SB * L)),(V2 + 1))) | (F + 1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Seg (F + 1) is non empty finite F + 1 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= F + 1 ) } is set
(LaplaceExpL ((B + (SB * L)),(V2 + 1))) | (Seg (F + 1)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Sum ((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | (F + 1)) is Element of the carrier of V1
the addF of V1 is Relation-like [: the carrier of V1, the carrier of V1:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
K132( the carrier of V1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | (F + 1)), the addF of V1) is Element of the carrier of V1
Indices B is set
((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) * SB is Element of the carrier of V1
((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) + (((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) * SB) is Element of the carrier of V1
(L * ((V2 + 1),(F + 1))) * SB is Element of the carrier of V1
((L * ((V2 + 1),(F + 1))) * SB) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) + (((L * ((V2 + 1),(F + 1))) * SB) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) is Element of the carrier of V1
(B * ((V2 + 1),(F + 1))) + ((L * ((V2 + 1),(F + 1))) * SB) is Element of the carrier of V1
((B * ((V2 + 1),(F + 1))) + ((L * ((V2 + 1),(F + 1))) * SB)) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
(SB * L) * ((V2 + 1),(F + 1)) is Element of the carrier of V1
(B * ((V2 + 1),(F + 1))) + ((SB * L) * ((V2 + 1),(F + 1))) is Element of the carrier of V1
((B * ((V2 + 1),(F + 1))) + ((SB * L) * ((V2 + 1),(F + 1)))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
(B + (SB * L)) * ((V2 + 1),(F + 1)) is Element of the carrier of V1
((B + (SB * L)) * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))) is Element of the carrier of V1
len (LaplaceExpL ((B + (SB * L)),(V2 + 1))) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
dom (LaplaceExpL ((B + (SB * L)),(V2 + 1))) is finite Element of bool NAT
(LaplaceExpL ((B + (SB * L)),(V2 + 1))) | F is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Seg F is finite F -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= F ) } is set
(LaplaceExpL ((B + (SB * L)),(V2 + 1))) | (Seg F) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
(LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1) is set
<*((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like set
[1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))] is set
{1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))} is non empty finite set
{1} is non empty trivial finite V36() 1 -element set
{{1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))},{1}} is non empty finite V36() set
{[1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))]} is Function-like non empty trivial finite 1 -element set
((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | F) ^ <*((LaplaceExpL ((B + (SB * L)),(V2 + 1))) . (F + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
SB * (Delete (L,(V2 + 1),(F + 1))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
(Delete (B,(V2 + 1),(F + 1))) + (SB * (Delete (L,(V2 + 1),(F + 1)))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
Delete ((SB * L),(V2 + 1),(F + 1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
(Delete (B,(V2 + 1),(F + 1))) + (Delete ((SB * L),(V2 + 1),(F + 1))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
Delete ((B + (SB * L)),(V2 + 1),(F + 1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
eval ((F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>),SB) is Element of the carrier of V1
eval (F9,SB) is Element of the carrier of V1
eval (<%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>,SB) is Element of the carrier of V1
(eval (F9,SB)) * (eval (<%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>,SB)) is Element of the carrier of V1
Det ((Delete (B,(V2 + 1),(F + 1))) + (SB * (Delete (L,(V2 + 1),(F + 1))))) is Element of the carrier of V1
(Det ((Delete (B,(V2 + 1),(F + 1))) + (SB * (Delete (L,(V2 + 1),(F + 1)))))) * (eval (<%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>,SB)) is Element of the carrier of V1
Minor ((B + (SB * L)),(V2 + 1),(F + 1)) is Element of the carrier of V1
Det (Delete ((B + (SB * L)),(V2 + 1),(F + 1))) is Element of the carrier of V1
(Minor ((B + (SB * L)),(V2 + 1),(F + 1))) * (((B + (SB * L)) * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))) is Element of the carrier of V1
Cofactor ((B + (SB * L)),(V2 + 1),(F + 1)) is Element of the carrier of V1
(V2 + 1) + (F + 1) is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() set
(power V1) . ((- (1_ V1)),((V2 + 1) + (F + 1))) is Element of the carrier of V1
((power V1) . ((- (1_ V1)),((V2 + 1) + (F + 1)))) * (Minor ((B + (SB * L)),(V2 + 1),(F + 1))) is Element of the carrier of V1
((B + (SB * L)) * ((V2 + 1),(F + 1))) * (Cofactor ((B + (SB * L)),(V2 + 1),(F + 1))) is Element of the carrier of V1
Sum ((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | F) is Element of the carrier of V1
K132( the carrier of V1,((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | F), the addF of V1) is Element of the carrier of V1
(Sum ((LaplaceExpL ((B + (SB * L)),(V2 + 1))) | F)) + (eval ((F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>),SB)) is Element of the carrier of V1
eval (D,SB) is Element of the carrier of V1
(eval (D,SB)) + (eval ((F9 *' <%((B * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1))))),((L * ((V2 + 1),(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + (V2 + 1)))))%>),SB)) is Element of the carrier of V1
0_. V1 is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) with_roots Element of bool [:NAT, the carrier of V1:]
F is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) with_roots Element of bool [:NAT, the carrier of V1:]
len F is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
f is Element of the carrier of V1
eval (F,f) is Element of the carrier of V1
f * L is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
B + (f * L) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
LaplaceExpL ((B + (f * L)),(V2 + 1)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(LaplaceExpL ((B + (f * L)),(V2 + 1))) | {} is Relation-like NAT -defined the carrier of V1 -valued Function-like one-to-one constant functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() ext-real non positive non negative V165() FinSequence of the carrier of V1
Seg {} is Function-like functional empty V25() V26() V27() V29() V30() V31() finite V36() cardinal {} -element {} -element FinSequence-membered without_zero V46() ext-real non positive non negative V165() Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= {} ) } is set
(LaplaceExpL ((B + (f * L)),(V2 + 1))) | (Seg {}) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Sum ((LaplaceExpL ((B + (f * L)),(V2 + 1))) | {}) is Element of the carrier of V1
the addF of V1 is Relation-like [: the carrier of V1, the carrier of V1:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
K132( the carrier of V1,((LaplaceExpL ((B + (f * L)),(V2 + 1))) | {}), the addF of V1) is Element of the carrier of V1
<*> the carrier of V1 is Relation-like NAT -defined the carrier of V1 -valued Function-like one-to-one constant functional empty V25() V26() V27() V29() V30() V31() finite finite-yielding V36() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V46() ext-real non positive non negative V165() FinSequence of the carrier of V1
0. V1 is V65(V1) Element of the carrier of V1
the ZeroF of V1 is Element of the carrier of V1
F is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len F is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
f is Element of the carrier of V1
eval (F,f) is Element of the carrier of V1
f * L is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
B + (f * L) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
Det (B + (f * L)) is Element of the carrier of V1
LaplaceExpL ((B + (f * L)),(V2 + 1)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
len (LaplaceExpL ((B + (f * L)),(V2 + 1))) is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
(LaplaceExpL ((B + (f * L)),(V2 + 1))) | (V2 + 1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(LaplaceExpL ((B + (f * L)),(V2 + 1))) | (Seg (V2 + 1)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Sum ((LaplaceExpL ((B + (f * L)),(V2 + 1))) | (V2 + 1)) is Element of the carrier of V1
the addF of V1 is Relation-like [: the carrier of V1, the carrier of V1:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
K132( the carrier of V1,((LaplaceExpL ((B + (f * L)),(V2 + 1))) | (V2 + 1)), the addF of V1) is Element of the carrier of V1
Sum (LaplaceExpL ((B + (f * L)),(V2 + 1))) is Element of the carrier of V1
K132( the carrier of V1,(LaplaceExpL ((B + (f * L)),(V2 + 1))), the addF of V1) is Element of the carrier of V1
{} + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V2 is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of {} , {} , the carrier of V1
A is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of {} , {} , the carrier of V1
1_. V1 is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
B is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len B is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
L is Element of the carrier of V1
eval (B,L) is Element of the carrier of V1
L * A is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of {} , {} , the carrier of V1
V2 + (L * A) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of {} , {} , the carrier of V1
Det (V2 + (L * A)) is Element of the carrier of V1
1_ V1 is Element of the carrier of V1
1. V1 is V65(V1) Element of the carrier of V1
the OneF of V1 is Element of the carrier of V1
V2 is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of V1
A is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of V1
K is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
K + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
V1 is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of V1 is non empty non trivial set
the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
[:NAT, the carrier of V1:] is non trivial non finite set
bool [:NAT, the carrier of V1:] is non trivial non finite set
1. (V1,K) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of K,K, the carrier of V1
V2 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
V2 + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
1. (V1,V2) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2,V2, the carrier of V1
(V2 + 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
1. (V1,(V2 + 1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
B is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
Indices (1. (V1,(V2 + 1))) is set
Indices B is set
(V2 + 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(V2 + 1) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Seg (V2 + 1) is non empty finite V2 + 1 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= V2 + 1 ) } is set
[:(Seg (V2 + 1)),(Seg (V2 + 1)):] is finite set
F is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() set
F + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
power V1 is Relation-like [: the carrier of V1,NAT:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1,NAT:], the carrier of V1:]
[: the carrier of V1,NAT:] is non trivial non finite set
[:[: the carrier of V1,NAT:], the carrier of V1:] is non trivial non finite set
bool [:[: the carrier of V1,NAT:], the carrier of V1:] is non trivial non finite set
1_ V1 is Element of the carrier of V1
1. V1 is V65(V1) Element of the carrier of V1
the OneF of V1 is Element of the carrier of V1
- (1_ V1) is Element of the carrier of V1
(F + 1) + 1 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
(power V1) . ((- (1_ V1)),((F + 1) + 1)) is Element of the carrier of V1
B * (1,(F + 1)) is Element of the carrier of V1
(B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))) is Element of the carrier of V1
(1. (V1,(V2 + 1))) * (1,(F + 1)) is Element of the carrier of V1
((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))) is Element of the carrier of V1
<%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
[1,(F + 1)] is Element of [:NAT,NAT:]
{1,(F + 1)} is non empty finite V36() set
{1} is non empty trivial finite V36() 1 -element set
{{1,(F + 1)},{1}} is non empty finite V36() set
(- (1_ V1)) * (- (1_ V1)) is Element of the carrier of V1
(1_ V1) * (1_ V1) is Element of the carrier of V1
2 -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
2 - 1 is V46() ext-real V165() set
<%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> . 1 is Element of the carrier of V1
0. V1 is V65(V1) Element of the carrier of V1
the ZeroF of V1 is Element of the carrier of V1
len <%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
Delete (B,1,1) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
FA is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len FA is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
<%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> *' FA is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
FB is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty total quasi_total V234(V1) Element of bool [:NAT, the carrier of V1:]
len FB is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
FA . V2 is set
(len <%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%>) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
<%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> . ((len <%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%>) -' 1) is Element of the carrier of V1
(len FA) -' 1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT
FA . ((len FA) -' 1) is Element of the carrier of V1
(<%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%> . ((len <%((B * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1)))),(((1. (V1,(V2 + 1))) * (1,(F + 1))) * ((power V1) . ((- (1_ V1)),((F + 1) + 1))))%>) -' 1)) * (FA . ((len FA) -' 1)) is Element of the carrier of V1
(V2 + 1) + 2 is non empty V25() V26() V27() V31() finite cardinal V46() ext-real positive non negative V165() Element of NAT
((V2 + 1) + 2) - 1 is V46() ext-real V165() set
SS is Element of the carrier of V1
eval (FB,SS) is Element of the carrier of V1
SS * (1. (V1,(V2 + 1))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
B + (SS * (1. (V1,(V2 + 1)))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2 + 1,V2 + 1, the carrier of V1
LaplaceExpL ((B + (SS * (1. (V1,(V2 + 1))))),1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(LaplaceExpL ((B + (SS * (1. (V1,(V2 + 1))))),1)) | (F + 1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Seg (F + 1) is non empty finite F + 1 -element without_zero Element of bool NAT
{ b1 where b1 is V25() V26() V27() V31() finite cardinal V46() ext-real non negative V165() Element of NAT : ( 1 <= b1 & b1 <= F + 1 ) } is set
(LaplaceExpL ((B + (SS * (1. (V1,(V2 + 1))))),1)) | (Seg (F + 1)) is Relation-like NAT -defined Function-like finite FinSubsequence-like set
Sum ((LaplaceExpL ((B + (SS * (1. (V1,(V2 + 1))))),1)) | (F + 1)) is Element of the carrier of V1
the addF of V1 is Relation-like [: the carrier of V1, the carrier of V1:] -defined the carrier of V1 -valued Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
K132( the carrier of V1,((LaplaceExpL ((B + (SS * (1. (V1,(V2 + 1))))),1)) | (F + 1)), the addF of V1) is Element of the carrier of V1
SS * (1. (V1,V2)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of V2,V2, the carrier of V1
(Delete (B,1,1)) + (SS * (1. (V1,V2))) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
Delete ((1. (V1,(V2 + 1))),1,1) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
SS * (Delete ((1. (V1,(V2 + 1))),1,1)) is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like tabular Matrix of (V2 + 1) -' 1,(V2 + 1) -' 1, the carrier of V1
(Delete (B,1,1)) + (SS