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