:: VECTSP11 semantic presentation

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

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

{ b

(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

{ b

(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

{ b

(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

{ b

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

{ b

(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