:: MATRLIN semantic presentation

REAL is set

NAT is non empty non trivial V24() V25() V26() non finite V41() V42() Element of bool REAL

bool REAL is non empty set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support set

1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

{{},1} is non empty finite V40() set

COMPLEX is set

NAT is non empty non trivial V24() V25() V26() non finite V41() V42() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of NAT

2 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

K226(0,1,2) is non empty finite set

[:K226(0,1,2),K226(0,1,2):] is Relation-like non empty finite set

[:[:K226(0,1,2),K226(0,1,2):],K226(0,1,2):] is Relation-like non empty finite set

bool [:[:K226(0,1,2),K226(0,1,2):],K226(0,1,2):] is non empty finite V40() set

bool [:K226(0,1,2),K226(0,1,2):] is non empty finite V40() set

RAT is set

INT is set

3 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

Seg 1 is non empty trivial finite V43(1) Element of bool NAT

{1} is non empty trivial finite V40() V43(1) set

Seg 2 is non empty finite V43(2) Element of bool NAT

{1,2} is non empty finite V40() set

K is non empty set

K * is functional non empty FinSequence-membered FinSequenceSet of K

a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of K *

Del (V1,a) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

rng (Del (V1,a)) is finite set

rng V1 is finite set

V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

f is set

b1 is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K

len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

b2 is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K

len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

K + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Del (a,(K + 1)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len (Del (a,(K + 1))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Seg (len a) is finite V43( len a) Element of bool NAT

dom a is finite set

K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

K + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 is non empty set

V1 * is functional non empty FinSequence-membered FinSequenceSet of V1

V2 is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + 1,a,V1

width V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(V1,(K + 1),V2) is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V1 *

width (V1,(K + 1),V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

V2 . (K + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

<*(V2 . (K + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support set

f is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V1 *

width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Seg (len V2) is finite V43( len V2) Element of bool NAT

dom V2 is finite set

Line (V2,(K + 1)) is Relation-like NAT -defined V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width V2) -tuples_on V1

(width V2) -tuples_on V1 is FinSequenceSet of V1

len (V1,(K + 1),V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

rng (V1,(K + 1),V2) is finite set

b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

rng V2 is finite set

b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

j is Relation-like NAT -defined V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V1

len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

p2 is Relation-like NAT -defined V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V1

len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len (Line (V2,(K + 1))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

b1 is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len (Line (V2,(K + 1))),V1

width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

K + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 is non empty set

V1 * is functional non empty FinSequence-membered FinSequenceSet of V1

V2 is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + 1,a,V1

(V1,(K + 1),V2) is Relation-like NAT -defined V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V1 *

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len (V1,(K + 1),V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

width V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

width (V1,(K + 1),V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

len K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Del (K,(len K)) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

K . (len K) is set

<*(K . (len K))*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support set

(Del (K,(len K))) ^ <*(K . (len K))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

a is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

V1 is set

<*V1*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support set

a ^ <*V1*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like finite-support set

len a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len <*V1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

(len a) + (len <*V1*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

(len a) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

len (Del (K,(len K))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom a is finite set

Seg (len a) is finite V43( len a) Element of bool NAT

V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

(Del (K,(len K))) . V2 is set

K . V2 is set

a . V2 is set

K is non empty set

a is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K

<*a*> is Relation-like NAT -defined Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support set

K * is functional non empty FinSequence-membered FinSequenceSet of K

len a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of a is non empty set

bool the carrier of a is non empty set

V1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier V1 is finite Element of bool the carrier of a

Sum V1 is Element of the carrier of a

V2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier V2 is finite Element of bool the carrier of a

Sum V2 is Element of the carrier of a

f is Element of bool the carrier of a

(Sum V1) - (Sum V2) is Element of the carrier of a

- (Sum V2) is Element of the carrier of a

(Sum V1) + (- (Sum V2)) is Element of the carrier of a

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is Relation-like non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . ((Sum V1),(- (Sum V2))) is Element of the carrier of a

0. a is V56(a) Element of the carrier of a

V1 - V2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier (V1 - V2) is finite Element of bool the carrier of a

Sum (V1 - V2) is Element of the carrier of a

(Carrier V1) \/ (Carrier V2) is finite Element of bool the carrier of a

b1 is Element of the carrier of a

(V1 - V2) . b1 is Element of the carrier of K

0. K is V56(K) Element of the carrier of K

V1 . b1 is Element of the carrier of K

V2 . b1 is Element of the carrier of K

(V1 . b1) - (V2 . b1) is Element of the carrier of K

- (V2 . b1) is Element of the carrier of K

(V1 . b1) + (- (V2 . b1)) is Element of the carrier of K

the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

the addF of K . ((V1 . b1),(- (V2 . b1))) is Element of the carrier of K

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of a is non empty set

bool the carrier of a is non empty set

V1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier V1 is finite Element of bool the carrier of a

Sum V1 is Element of the carrier of a

V2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier V2 is finite Element of bool the carrier of a

Sum V2 is Element of the carrier of a

f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier f is finite Element of bool the carrier of a

Sum f is Element of the carrier of a

(Sum V2) + (Sum f) is Element of the carrier of a

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is Relation-like non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . ((Sum V2),(Sum f)) is Element of the carrier of a

V2 + f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

b1 is Element of bool the carrier of a

Carrier (V2 + f) is finite Element of bool the carrier of a

(Carrier V2) \/ (Carrier f) is finite Element of bool the carrier of a

Sum (V2 + f) is Element of the carrier of a

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

0. K is V56(K) Element of the carrier of K

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of a is non empty set

bool the carrier of a is non empty set

V1 is Element of the carrier of K

V2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier V2 is finite Element of bool the carrier of a

Sum V2 is Element of the carrier of a

f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

Carrier f is finite Element of bool the carrier of a

Sum f is Element of the carrier of a

V1 * (Sum f) is Element of the carrier of a

V1 * f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a

b1 is Element of bool the carrier of a

Carrier (V1 * f) is finite Element of bool the carrier of a

Sum (V1 * f) is Element of the carrier of a

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of a is non empty set

V1 is Element of the carrier of a

V2 is Basis of a

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is Relation-like non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the ZeroF of a is Element of the carrier of a

the lmult of a is Relation-like [: the carrier of K, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of a:], the carrier of a:]

[: the carrier of K, the carrier of a:] is Relation-like non empty set

[:[: the carrier of K, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of a:], the carrier of a:] is non empty set

VectSpStr(# the carrier of a, the addF of a, the ZeroF of a, the lmult of a #) is non empty strict VectSpStr over K

Lin V2 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of a

f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V2

Sum f is Element of the carrier of a

b1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V2

Sum b1 is Element of the carrier of a

Carrier b1 is finite Element of bool the carrier of a

bool the carrier of a is non empty set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

(0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is non empty set

bool the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is non empty set

{} the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered linearly-independent V144() FinSequence-yielding finite-support Element of bool the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K)

V1 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered linearly-independent V144() FinSequence-yielding finite-support Element of bool the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K)

Lin V1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of (0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

(0). ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of (0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the addF of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is Relation-like [: the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] -defined the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):]

[: the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is Relation-like non empty set

[:[: the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is Relation-like non empty set

bool [:[: the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is non empty set

the ZeroF of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is Element of the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K)

the lmult of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) is Relation-like [: the carrier of K, the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] -defined the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):]

the carrier of K is non empty non trivial set

[: the carrier of K, the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is Relation-like non empty set

[:[: the carrier of K, the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):], the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K):] is non empty set

VectSpStr(# the carrier of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the addF of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the ZeroF of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K), the lmult of ((0). the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K) #) is non empty strict VectSpStr over K

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

bool the carrier of a is non empty set

V1 is finite Element of bool the carrier of a

V2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set

rng V2 is finite set

f is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

rng b1 is finite set

K is non empty doubleLoopStr

a is non empty VectSpStr over K

the carrier of a is non empty set

V1 is non empty VectSpStr over K

the carrier of V1 is non empty set

[: the carrier of a, the carrier of V1:] is Relation-like non empty set

bool [: the carrier of a, the carrier of V1:] is non empty set

V2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

f is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b1 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

i is Element of the carrier of a

b2 . i is Element of the carrier of V1

V2 . i is Element of the carrier of V1

f . i is Element of the carrier of V1

(V2 . i) + (f . i) 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 non empty 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 Relation-like non empty set

[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like non empty set

bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is non empty set

the addF of V1 . ((V2 . i),(f . i)) is Element of the carrier of V1

b1 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

i is Element of the carrier of a

b1 . i is Element of the carrier of V1

V2 . i is Element of the carrier of V1

f . i is Element of the carrier of V1

(V2 . i) + (f . i) 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 non empty 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 Relation-like non empty set

[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like non empty set

bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is non empty set

the addF of V1 . ((V2 . i),(f . i)) is Element of the carrier of V1

b2 . i is Element of the carrier of V1

K is non empty doubleLoopStr

a is non empty VectSpStr over K

the carrier of a is non empty set

V1 is non empty VectSpStr over K

the carrier of V1 is non empty set

[: the carrier of a, the carrier of V1:] is Relation-like non empty set

bool [: the carrier of a, the carrier of V1:] is non empty set

the carrier of K is non empty set

f is Element of the carrier of K

V2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b1 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

i is Element of the carrier of a

b2 . i is Element of the carrier of V1

V2 . i is Element of the carrier of V1

f * (V2 . i) is Element of the carrier of V1

b1 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

b2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

i is Element of the carrier of a

b1 . i is Element of the carrier of V1

V2 . i is Element of the carrier of V1

f * (V2 . i) is Element of the carrier of V1

b2 . i is Element of the carrier of V1

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is Element of the carrier of a

V2 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V2 is finite set

Sum V2 is Element of the carrier of a

f is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Sum f is Element of the carrier of K

(Sum f) * V1 is Element of the carrier of a

b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

b1 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

b2 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom b2 is finite set

Sum b2 is Element of the carrier of a

i is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Sum i is Element of the carrier of K

(Sum i) * V1 is Element of the carrier of a

Seg b1 is finite V43(b1) Element of bool NAT

i | (Seg b1) is Relation-like NAT -defined Seg b1 -defined NAT -defined the carrier of K -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT, the carrier of K:]

[:NAT, the carrier of K:] is Relation-like non empty non trivial non finite set

bool [:NAT, the carrier of K:] is non empty non trivial non finite set

b2 | (Seg b1) is Relation-like NAT -defined Seg b1 -defined NAT -defined the carrier of a -valued Function-like finite FinSubsequence-like finite-support Element of bool [:NAT, the carrier of a:]

[:NAT, the carrier of a:] is Relation-like non empty non trivial non finite set

bool [:NAT, the carrier of a:] is non empty non trivial non finite set

p2 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom p2 is finite set

j is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom j is finite set

b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

p1 is Element of the carrier of K

j . b4 is set

i . b4 is set

b2 . b4 is set

p1 * V1 is Element of the carrier of a

p2 . b4 is set

b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

b4 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

Seg (b4 + 1) is non empty finite V43(b4 + 1) V43(b4 + 1) Element of bool NAT

b4 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

b2 . (b4 + 1) is set

dom i is finite set

i . (b4 + 1) is set

p1 is Element of the carrier of a

KL1 is Element of the carrier of K

KL1 * V1 is Element of the carrier of a

Sum p2 is Element of the carrier of a

(Sum p2) + p1 is Element of the carrier of a

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is Relation-like non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . ((Sum p2),p1) is Element of the carrier of a

Sum j is Element of the carrier of K

(Sum j) * V1 is Element of the carrier of a

((Sum j) * V1) + (KL1 * V1) is Element of the carrier of a

the addF of a . (((Sum j) * V1),(KL1 * V1)) is Element of the carrier of a

(Sum j) + KL1 is Element of the carrier of K

the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

the addF of K . ((Sum j),KL1) is Element of the carrier of K

((Sum j) + KL1) * V1 is Element of the carrier of a

b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom b1 is finite set

Sum b1 is Element of the carrier of a

b2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Sum b2 is Element of the carrier of K

(Sum b2) * V1 is Element of the carrier of a

<*> the carrier of a is Relation-like non-empty empty-yielding NAT -defined the carrier of a -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of a *

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

0. a is V56(a) Element of the carrier of a

<*> the carrier of K is Relation-like non-empty empty-yielding NAT -defined the carrier of K -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of K *

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

0. K is V56(K) Element of the carrier of K

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is Element of the carrier of a

V2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V2 is finite set

Sum V2 is Element of the carrier of K

(Sum V2) * V1 is Element of the carrier of a

f is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

Sum f is Element of the carrier of a

b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

dom f is finite set

b2 is Element of the carrier of K

V2 . b1 is set

V2 /. b1 is Element of the carrier of K

f . b1 is set

b2 * V1 is Element of the carrier of a

K is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of K is non empty set

0. K is V56(K) Element of the carrier of K

a is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

dom a is finite set

Sum a is Element of the carrier of K

V1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

dom V1 is finite set

Sum V1 is Element of the carrier of K

V2 is Element of the carrier of K

<*V2*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of K *

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

V1 ^ <*V2*> is Relation-like NAT -defined the carrier of K -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

dom (V1 ^ <*V2*>) is non empty finite set

Sum (V1 ^ <*V2*>) is Element of the carrier of K

len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(len V1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

Seg ((len V1) + 1) is non empty finite V43((len V1) + 1) V43((len V1) + 1) Element of bool NAT

(len V1) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 /. f is Element of the carrier of K

V1 . f is set

b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(V1 ^ <*V2*>) . b1 is set

(V1 ^ <*V2*>) /. f is Element of the carrier of K

len (V1 ^ <*V2*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

len <*V2*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

(len V1) + (len <*V2*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

(V1 ^ <*V2*>) . ((len V1) + 1) is set

Sum <*V2*> is Element of the carrier of K

(Sum V1) + (Sum <*V2*>) is Element of the carrier of K

the addF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is Relation-like non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

the addF of K . ((Sum V1),(Sum <*V2*>)) is Element of the carrier of K

(Sum V1) + V2 is Element of the carrier of K

the addF of K . ((Sum V1),V2) is Element of the carrier of K

(V1 ^ <*V2*>) /. ((len V1) + 1) is Element of the carrier of K

(Sum V1) + ((V1 ^ <*V2*>) /. ((len V1) + 1)) is Element of the carrier of K

the addF of K . ((Sum V1),((V1 ^ <*V2*>) /. ((len V1) + 1))) is Element of the carrier of K

(0. K) + (0. K) is Element of the carrier of K

the addF of K . ((0. K),(0. K)) is Element of the carrier of K

f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 /. f is Element of the carrier of K

<*> the carrier of K is Relation-like non-empty empty-yielding NAT -defined the carrier of K -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of K *

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

dom (<*> the carrier of K) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support set

Sum (<*> the carrier of K) is Element of the carrier of K

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

the lmult of a is Relation-like [: the carrier of K, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of a:], the carrier of a:]

[: the carrier of K, the carrier of a:] is Relation-like non empty set

[:[: the carrier of K, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of a:], the carrier of a:] is non empty set

V1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

V2 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

the lmult of a .: (V1,V2) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

<:V1,V2:> is Relation-like Function-like set

<:V1,V2:> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

dom V1 is finite set

V2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

dom V2 is finite set

(K,a,V2,V1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

the lmult of a is Relation-like [: the carrier of K, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of a:], the carrier of a:]

[: the carrier of K, the carrier of a:] is Relation-like non empty set

[:[: the carrier of K, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of a:], the carrier of a:] is non empty set

the lmult of a .: (V2,V1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

<:V2,V1:> is Relation-like Function-like set

<:V2,V1:> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set

dom (K,a,V2,V1) is finite set

rng V2 is finite set

rng V1 is finite set

[:(rng V2),(rng V1):] is Relation-like finite set

rng <:V2,V1:> is set

dom the lmult of a is Relation-like non empty set

dom <:V2,V1:> is set

(dom V2) /\ (dom V1) is finite set

K is non empty addLoopStr

the carrier of K is non empty set

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

a is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support FinSequence of the carrier of K *

len a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

V1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V1 is finite set

V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 /. V2 is Element of the carrier of K

V1 . V2 is set

a /. V2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of K *

Sum (a /. V2) is Element of the carrier of K

V1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V1 is finite set

V2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V2 is finite set

Seg (len V1) is finite V43( len V1) Element of bool NAT

f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

V1 . f is set

V1 /. f is Element of the carrier of K

a /. f is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of K *

Sum (a /. f) is Element of the carrier of K

V2 /. f is Element of the carrier of K

V2 . f is set

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

0. a is V56(a) Element of the carrier of a

V1 is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of a *

len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(a,V1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

Sum (a,V1) is Element of the carrier of a

len (a,V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

<*> the carrier of a is Relation-like non-empty empty-yielding NAT -defined the carrier of a -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of a *

K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

K + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

a is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

V1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (a) VectSpStr over a

the carrier of V1 is non empty set

the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1

0. V1 is V56(V1) Element of the carrier of V1

V2 is Relation-like NAT -defined the carrier of V1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + 1, 0 , the carrier of V1

(V1,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

Sum (V1,V2) is Element of the carrier of V1

dom (V1,V2) is finite set

f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

(V1,V2) /. f is Element of the carrier of V1

len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len (V1,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

dom V2 is finite set

b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

V2 /. b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of V1 *

rng V2 is finite set

V2 /. f is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of V1 *

len (V2 /. f) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

<*> the carrier of V1 is Relation-like non-empty empty-yielding NAT -defined the carrier of V1 -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of V1 *

Sum (V2 /. f) is Element of the carrier of V1

K is non empty set

a is Element of K

<*a*> is Relation-like NAT -defined K -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support Element of K *

K * is functional non empty FinSequence-membered FinSequenceSet of K

(K,<*a*>) is Relation-like NAT -defined K * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len <*a*>,K

len <*a*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

(K,<*a*>) @ is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of K *

len (K,<*a*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT

width (K,<*a*>) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len ((K,<*a*>) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

[f,b1] is set

{f,b1} is non empty finite V40() set

{f} is non empty trivial finite V40() V43(1) set

{{f,b1},{f}} is non empty finite V40() set

Indices (K,<*a*>) is set

dom (K,<*a*>) is non empty trivial finite V43(1) set

[:(dom (K,<*a*>)),(Seg 1):] is Relation-like non empty finite set

(K,<*a*>) * (f,b1) is Element of K

((K,<*a*>) @) * (f,b1) is Element of K

width ((K,<*a*>) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of a is non empty set

V1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V1 is non empty set

[: the carrier of a, the carrier of V1:] is Relation-like non empty set

bool [: the carrier of a, the carrier of V1:] is non empty set

V2 is Relation-like the carrier of a -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V1:]

f is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

Sum f is Element of the carrier of a

V2 . (Sum f) is Element of the carrier of V1

V2 * f is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

Sum (V2 * f) is Element of the carrier of V1

b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

Sum b1 is Element of the carrier of a

V2 . (Sum b1) is Element of the carrier of V1

V2 * b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

Sum (V2 * b1) is Element of the carrier of V1

b2 is Element of the carrier of a

<*b2*> is Relation-like NAT -defined the carrier of a -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of a *

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

b1 ^ <*b2*> is Relation-like NAT -defined the carrier of a -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

Sum (b1 ^ <*b2*>) is Element of the carrier of a

V2 . (Sum (b1 ^ <*b2*>)) is Element of the carrier of V1

V2 * (b1 ^ <*b2*>) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

Sum (V2 * (b1 ^ <*b2*>)) is Element of the carrier of V1

Sum <*b2*> is Element of the carrier of a

(Sum b1) + (Sum <*b2*>) is Element of the carrier of a

the addF of a is Relation-like [: the carrier of a, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of a, the carrier of a:], the carrier of a:]

[: the carrier of a, the carrier of a:] is Relation-like non empty set

[:[: the carrier of a, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of a, the carrier of a:], the carrier of a:] is non empty set

the addF of a . ((Sum b1),(Sum <*b2*>)) is Element of the carrier of a

V2 . ((Sum b1) + (Sum <*b2*>)) is Element of the carrier of V1

V2 . (Sum <*b2*>) is Element of the carrier of V1

(Sum (V2 * b1)) + (V2 . (Sum <*b2*>)) 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 non empty 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 Relation-like non empty set

[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like non empty set

bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is non empty set

the addF of V1 . ((Sum (V2 * b1)),(V2 . (Sum <*b2*>))) is Element of the carrier of V1

V2 . b2 is Element of the carrier of V1

(Sum (V2 * b1)) + (V2 . b2) is Element of the carrier of V1

the addF of V1 . ((Sum (V2 * b1)),(V2 . b2)) is Element of the carrier of V1

<*(V2 . b2)*> is Relation-like NAT -defined the carrier of V1 -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like finite-support Element of the carrier of V1 *

the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1

Sum <*(V2 . b2)*> is Element of the carrier of V1

(Sum (V2 * b1)) + (Sum <*(V2 . b2)*>) is Element of the carrier of V1

the addF of V1 . ((Sum (V2 * b1)),(Sum <*(V2 . b2)*>)) is Element of the carrier of V1

(V2 * b1) ^ <*(V2 . b2)*> is Relation-like NAT -defined the carrier of V1 -valued Function-like non empty finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

Sum ((V2 * b1) ^ <*(V2 . b2)*>) is Element of the carrier of V1

<*> the carrier of a is Relation-like non-empty empty-yielding NAT -defined the carrier of a -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of a *

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet of the carrier of a

Sum (<*> the carrier of a) is Element of the carrier of a

V2 . (Sum (<*> the carrier of a)) is Element of the carrier of V1

0. a is V56(a) Element of the carrier of a

V2 . (0. a) is Element of the carrier of V1

0. K is V56(K) Element of the carrier of K

the carrier of K is non empty non trivial set

(0. K) * (0. a) is Element of the carrier of a

V2 . ((0. K) * (0. a)) is Element of the carrier of V1

(0. K) * (V2 . (0. a)) is Element of the carrier of V1

0. V1 is V56(V1) Element of the carrier of V1

<*> the carrier of V1 is Relation-like non-empty empty-yielding NAT -defined the carrier of V1 -valued Function-like one-to-one constant functional empty V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support Element of the carrier of V1 *

the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1

Sum (<*> the carrier of V1) is Element of the carrier of V1

V2 * (<*> the carrier of a) is Relation-like non-empty empty-yielding NAT -defined the carrier of V1 -valued Function-like one-to-one constant functional empty proper V24() V25() V26() V28() V29() V30() V31() ext-real non positive non negative V35() finite finite-yielding V40() V41() V43( {} ) FinSequence-like FinSubsequence-like FinSequence-membered V144() FinSequence-yielding finite-support FinSequence of the carrier of V1

[:NAT, the carrier of V1:] is Relation-like non empty non trivial non finite set

Sum (V2 * (<*> the carrier of a)) is Element of the carrier of V1

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of V1 is non empty set

[: the carrier of V1, the carrier of a:] is Relation-like non empty set

bool [: the carrier of V1, the carrier of a:] is non empty set

V2 is Relation-like the carrier of V1 -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of V1, the carrier of a:]

f is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(K,V1,f,b1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

the lmult of V1 is Relation-like [: the carrier of K, the carrier of V1:] -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:]

[: the carrier of K, the carrier of V1:] is Relation-like non empty set

[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is non empty set

the lmult of V1 .: (f,b1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

<:f,b1:> is Relation-like Function-like set

<:f,b1:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set

V2 * (K,V1,f,b1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

V2 * b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

(K,a,f,(V2 * b1)) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

the lmult of a is Relation-like [: the carrier of K, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of a:], the carrier of a:]

[: the carrier of K, the carrier of a:] is Relation-like non empty set

[:[: the carrier of K, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of a:], the carrier of a:] is non empty set

the lmult of a .: (f,(V2 * b1)) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

<:f,(V2 * b1):> is Relation-like Function-like set

<:f,(V2 * b1):> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set

dom b1 is finite set

dom f is finite set

dom V2 is non empty set

rng b1 is finite set

dom (V2 * b1) is finite set

i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set

dom (V2 * (K,V1,f,b1)) is finite set

dom (K,V1,f,b1) is finite set

b1 /. i is Element of the carrier of V1

b1 . i is set

dom (K,a,f,(V2 * b1)) is finite set

f /. i is Element of the carrier of K

f . i is set

(V2 * b1) /. i is Element of the carrier of a

(V2 * b1) . i is set

(V2 * (K,V1,f,b1)) . i is set

(K,V1,f,b1) . i is set

V2 . ((K,V1,f,b1) . i) is set

the lmult of V1 . ((f . i),(b1 . i)) is set

V2 . ( the lmult of V1 . ((f . i),(b1 . i))) is set

(f /. i) * (b1 /. i) is Element of the carrier of V1

V2 . ((f /. i) * (b1 /. i)) is Element of the carrier of a

V2 . (b1 /. i) is Element of the carrier of a

(f /. i) * (V2 . (b1 /. i)) is Element of the carrier of a

(f /. i) * ((V2 * b1) /. i) is Element of the carrier of a

the lmult of a . ((f . i),((V2 * b1) . i)) is set

(K,a,f,(V2 * b1)) . i is set

len (K,V1,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len (K,a,f,(V2 * b1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

len (V2 * (K,V1,f,b1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of V1 is non empty set

[: the carrier of V1, the carrier of a:] is Relation-like non empty set

bool [: the carrier of V1, the carrier of a:] is non empty set

V2 is Relation-like the carrier of V1 -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [: the carrier of V1, the carrier of a:]

f is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)

len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

V2 * f is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

b1 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of K

len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT

(K,V1,b1,f) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

the lmult of V1 is Relation-like [: the carrier of K, the carrier of V1:] -defined the carrier of V1 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:]

[: the carrier of K, the carrier of V1:] is Relation-like non empty set

[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is non empty set

the lmult of V1 .: (b1,f) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V1

<:b1,f:> is Relation-like Function-like set

<:b1,f:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set

Sum (K,V1,b1,f) is Element of the carrier of V1

V2 . (Sum (K,V1,b1,f)) is Element of the carrier of a

(K,a,b1,(V2 * f)) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

the lmult of a is Relation-like [: the carrier of K, the carrier of a:] -defined the carrier of a -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of a:], the carrier of a:]

[: the carrier of K, the carrier of a:] is Relation-like non empty set

[:[: the carrier of K, the carrier of a:], the carrier of a:] is Relation-like non empty set

bool [:[: the carrier of K, the carrier of a:], the carrier of a:] is non empty set

the lmult of a .: (b1,(V2 * f)) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

<:b1,(V2 * f):> is Relation-like Function-like set

<:b1,(V2 * f):> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set

Sum (K,a,b1,(V2 * f)) is Element of the carrier of a

V2 * (K,V1,b1,f) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a

Sum (V2 * (K,V1,b1,f)) is Element of the carrier of a

K is non empty non degenerated non trivial right_complementable almost_left_invertible V99() V101() V103() right-distributive left-distributive right_unital well-unital V109() left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

a is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K

the carrier of a is non empty set

V1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support