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 FinSequence of the carrier of a
dom V1 is finite set
[:(dom V1),(dom V1):] is Relation-like finite set
bool [:(dom V1),(dom V1):] is non empty finite V40() set
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
f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
f (#) 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
f (#) 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
b1 is Relation-like dom V1 -defined dom V1 -valued Function-like one-to-one total quasi_total onto bijective finite finite-support Element of bool [:(dom V1),(dom V1):]
V1 * b1 is Relation-like dom V1 -defined the carrier of a -valued Function-like finite finite-support Element of bool [:(dom V1), the carrier of a:]
[:(dom V1), the carrier of a:] is Relation-like set
bool [:(dom V1), the carrier of a:] is non empty set
(f (#) V1) * b1 is Relation-like dom V1 -defined the carrier of a -valued Function-like finite finite-support Element of bool [:(dom V1), the carrier of a:]
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len V1) is finite V43( len V1) Element of bool NAT
len (f (#) V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (f (#) V1)) is finite V43( len (f (#) V1)) Element of bool NAT
dom (f (#) V1) is finite set
len (f (#) V2) 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
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 (f (#) V2) is finite set
dom ((f (#) V1) * b1) is finite set
dom V2 is finite set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom b1 is finite set
b1 . i is set
rng b1 is finite set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b1 . j is set
V2 /. i is Element of the carrier of a
V2 . i is set
V1 . (b1 . i) is set
V1 /. (b1 . i) is Element of the carrier of a
(f (#) V2) . i is set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
V1 /. p2 is Element of the carrier of a
f . (V1 /. p2) is Element of the carrier of K
(f . (V1 /. p2)) * (V1 /. p2) is Element of the carrier of a
(f (#) V1) . p2 is set
b2 . i 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
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
rng V1 is finite set
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
bool the carrier of a is non empty set
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
Sum (V2 (#) V1) is Element of the carrier of a
Sum V2 is Element of the carrier of a
bool (rng V1) is non empty finite V40() set
dom V1 is finite set
[:(dom V1),(dom V1):] is Relation-like finite set
bool [:(dom V1),(dom V1):] is non empty finite V40() set
f is finite Element of bool (rng V1)
f ` is finite Element of bool (rng V1)
V1 - (f `) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
V1 - f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(V1 - (f `)) ^ (V1 - f) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b1 is Relation-like dom V1 -defined dom V1 -valued Function-like one-to-one total quasi_total onto bijective finite finite-support Element of bool [:(dom V1),(dom V1):]
V1 * b1 is Relation-like dom V1 -defined the carrier of a -valued Function-like finite finite-support Element of bool [:(dom V1), the carrier of a:]
[:(dom V1), the carrier of a:] is Relation-like set
bool [:(dom V1), the carrier of a:] is non empty set
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 (V2 (#) V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (V2 (#) V1) is finite set
[:(dom (V2 (#) V1)),(dom (V2 (#) V1)):] is Relation-like finite set
bool [:(dom (V2 (#) V1)),(dom (V2 (#) V1)):] is non empty finite V40() set
rng b2 is finite set
(rng V1) \ (f `) is finite Element of bool (rng V1)
(rng V1) \ (Carrier V2) is finite Element of bool (rng V1)
(rng V1) \ ((rng V1) \ (Carrier V2)) is finite Element of bool (rng V1)
(rng V1) /\ (Carrier V2) is finite Element of bool the carrier of a
i 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 (#) i 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 (V2 (#) i) is finite set
0. a is V56(a) Element of the carrier of a
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(V2 (#) i) /. p2 is Element of the carrier of a
len (V2 (#) i) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom i is finite set
i . p2 is set
rng i is finite set
i /. p2 is Element of the carrier of a
(V2 (#) i) . p2 is set
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i /. b4 is Element of the carrier of a
V2 . (i /. b4) is Element of the carrier of K
(V2 . (i /. b4)) * (i /. b4) is Element of the carrier of a
0. K is V56(K) Element of the carrier of K
(0. K) * (i /. p2) is Element of the carrier of a
Sum (V2 (#) i) is Element of the carrier of a
b2 ^ i 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 (#) (b2 ^ i) 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
j is Relation-like dom (V2 (#) V1) -defined dom (V2 (#) V1) -valued Function-like one-to-one total quasi_total onto bijective finite finite-support Element of bool [:(dom (V2 (#) V1)),(dom (V2 (#) V1)):]
(V2 (#) V1) * j is Relation-like dom (V2 (#) V1) -defined the carrier of a -valued Function-like finite finite-support Element of bool [:(dom (V2 (#) V1)), the carrier of a:]
[:(dom (V2 (#) V1)), the carrier of a:] is Relation-like set
bool [:(dom (V2 (#) V1)), the carrier of a:] is non empty set
Sum (V2 (#) (b2 ^ i)) is Element of the carrier of a
V2 (#) 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
(V2 (#) b2) ^ (V2 (#) i) 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 (#) b2) ^ (V2 (#) i)) is Element of the carrier of a
Sum (V2 (#) b2) is Element of the carrier of a
(Sum (V2 (#) b2)) + (Sum (V2 (#) i)) 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 (#) b2)),(Sum (V2 (#) i))) is Element of the carrier of a
(Sum V2) + (0. a) is Element of the carrier of a
the addF of a . ((Sum V2),(0. a)) 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
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 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:]
b1 is set
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
rng b2 is finite set
Sum b2 is Element of the carrier of V1
V2 . (Sum b2) is Element of the carrier of a
f . (Sum b2) is Element of the carrier of a
i 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
rng i is finite set
Sum i is Element of the carrier of V1
V2 . (Sum i) is Element of the carrier of a
f . (Sum i) is Element of the carrier of a
j is Element of the carrier of V1
<*j*> 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
i ^ <*j*> 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
rng (i ^ <*j*>) is non empty finite set
Sum (i ^ <*j*>) is Element of the carrier of V1
V2 . (Sum (i ^ <*j*>)) is Element of the carrier of a
f . (Sum (i ^ <*j*>)) is Element of the carrier of a
rng <*j*> is non empty trivial finite V43(1) set
(rng i) \/ (rng <*j*>) is non empty finite set
{j} is non empty trivial finite V43(1) set
Sum <*j*> is Element of the carrier of V1
(Sum i) + (Sum <*j*>) 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 i),(Sum <*j*>)) is Element of the carrier of V1
V2 . ((Sum i) + (Sum <*j*>)) is Element of the carrier of a
V2 . (Sum <*j*>) is Element of the carrier of a
(f . (Sum i)) + (V2 . (Sum <*j*>)) 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 . ((f . (Sum i)),(V2 . (Sum <*j*>))) is Element of the carrier of a
V2 . j is Element of the carrier of a
(f . (Sum i)) + (V2 . j) is Element of the carrier of a
the addF of a . ((f . (Sum i)),(V2 . j)) is Element of the carrier of a
f . j is Element of the carrier of a
(f . (Sum i)) + (f . j) is Element of the carrier of a
the addF of a . ((f . (Sum i)),(f . j)) is Element of the carrier of a
f . (Sum <*j*>) is Element of the carrier of a
(f . (Sum i)) + (f . (Sum <*j*>)) is Element of the carrier of a
the addF of a . ((f . (Sum i)),(f . (Sum <*j*>))) is Element of the carrier of a
f . ((Sum i) + (Sum <*j*>)) is Element of the carrier of a
<*> 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
rng (<*> the carrier of V1) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty trivial 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() V147() FinSequence-yielding finite-support set
Sum (<*> the carrier of V1) is Element of the carrier of V1
V2 . (Sum (<*> the carrier of V1)) is Element of the carrier of a
f . (Sum (<*> the carrier of V1)) is Element of the carrier of a
0. V1 is V56(V1) Element of the carrier of V1
V2 . (0. V1) is Element of the carrier of a
0. K is V56(K) Element of the carrier of K
the carrier of K is non empty non trivial set
(0. K) * (0. V1) is Element of the carrier of V1
V2 . ((0. K) * (0. V1)) is Element of the carrier of a
(0. K) * (V2 . (0. V1)) is Element of the carrier of a
0. a is V56(a) Element of the carrier of a
f . (0. V1) is Element of the carrier of a
(0. K) * (f . (0. V1)) is Element of the carrier of a
f . ((0. K) * (0. V1)) 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
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 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:]
b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
len 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 a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of a
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
rng b1 is finite set
Seg (len b1) is finite V43( len b1) Element of bool NAT
dom b1 is finite set
b2 is Basis of V1
Lin b2 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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 ZeroF of V1 is Element 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 is non empty non trivial set
[: 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
VectSpStr(# the carrier of V1, the addF of V1, the ZeroF of V1, the lmult of V1 #) is non empty strict VectSpStr over K
j is Element of the carrier of V1
p2 is Relation-like the carrier of V1 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of b2
Sum p2 is Element of the carrier of V1
p2 (#) 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
i is non empty set
{ ((p2 . (b1 /. b1)) * (b1 /. b1)) where b1 is Element of i : verum } is set
rng (p2 (#) b1) is finite set
KL1 is set
dom (p2 (#) b1) is finite set
KL2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(p2 (#) b1) . KL2 is set
len (p2 (#) b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (p2 (#) b1)) is finite V43( len (p2 (#) b1)) Element of bool NAT
b1 /. KL2 is Element of the carrier of V1
p2 . (b1 /. KL2) is Element of the carrier of K
(p2 . (b1 /. KL2)) * (b1 /. KL2) is Element of the carrier of V1
KL1 is Element of the carrier of V1
V2 . KL1 is Element of the carrier of a
f . KL1 is Element of the carrier of a
KL2 is Element of i
b1 /. KL2 is Element of the carrier of V1
p2 . (b1 /. KL2) is Element of the carrier of K
(p2 . (b1 /. KL2)) * (b1 /. KL2) is Element of the carrier of V1
V2 . (b1 /. KL2) is Element of the carrier of a
b1 . KL2 is set
V2 . (b1 . KL2) is set
(f * b1) . KL2 is set
f . (b1 . KL2) is set
f . (b1 /. KL2) is Element of the carrier of a
V2 . ((p2 . (b1 /. KL2)) * (b1 /. KL2)) is Element of the carrier of a
(p2 . (b1 /. KL2)) * (f . (b1 /. KL2)) is Element of the carrier of a
f . ((p2 . (b1 /. KL2)) * (b1 /. KL2)) is Element of the carrier of a
Carrier p2 is finite Element of bool the carrier of V1
bool the carrier of V1 is non empty set
V2 . j is Element of the carrier of a
Sum (p2 (#) b1) is Element of the carrier of V1
V2 . (Sum (p2 (#) b1)) is Element of the carrier of a
f . (Sum (p2 (#) b1)) is Element of the carrier of a
f . j is Element of the carrier of a
K is non empty set
K * is functional non empty FinSequence-membered FinSequenceSet of 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 *
K is non empty set
K * is functional non empty FinSequence-membered FinSequenceSet of 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 *
V1 is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of K *
a ^^ V1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support set
V2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
rng V2 is finite set
width a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width a) + (width V1) 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() Element of NAT
b1 is set
rng a is finite set
rng V1 is finite set
dom V2 is finite set
b2 is set
V2 . b2 is set
dom a is finite set
dom V1 is finite set
(dom a) /\ (dom V1) is finite set
V1 . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
a . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 . p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (V1,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width V1) -tuples_on K
(width V1) -tuples_on K is FinSequenceSet of K
i is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K
j is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K
i ^ j is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K
b4 is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K
len b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
a . p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (a,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width a) -tuples_on K
(width a) -tuples_on K is FinSequenceSet of K
len (Line (a,p2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (Line (V1,p2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (Line (a,p2))) + (len (Line (V1,p2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width a) + (len (Line (V1,p2))) 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
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
V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
f is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of a,V2,K
b1 is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,V2,K
f ^ b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support set
a + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
f ^ b1 is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support FinSequence of K *
rng (f ^ b1) is finite set
b2 is set
i is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of K
len i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
rng f is finite set
rng b1 is finite set
(rng f) \/ (rng b1) is finite set
dom f is finite set
j is set
f . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line (f,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width f) -tuples_on K
(width f) -tuples_on K is FinSequenceSet of K
dom b1 is finite set
j is set
b1 . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line (b1,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width b1) -tuples_on K
(width b1) -tuples_on K is FinSequenceSet of K
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b2 is Relation-like NAT -defined K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of K *
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
rng b2 is finite set
width b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
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
rng f is finite set
rng b1 is finite set
(rng f) \/ (rng b1) is finite set
dom f is finite set
j is set
f . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line (f,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width f) -tuples_on K
(width f) -tuples_on K is FinSequenceSet of K
dom b1 is finite set
j is set
b1 . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line (b1,p2) is Relation-like NAT -defined K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width b1) -tuples_on K
(width b1) -tuples_on K is FinSequenceSet of K
K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
f is non empty set
f * is functional non empty FinSequence-membered FinSequenceSet of f
b1 is Relation-like NAT -defined f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a,f
dom b1 is finite set
Line (b1,V2) is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width b1) -tuples_on f
width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width b1) -tuples_on f is FinSequenceSet of f
b2 is Relation-like NAT -defined f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a,f
(f,K,V1,a,b1,b2) is Relation-like NAT -defined f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a,f
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line ((f,K,V1,a,b1,b2),V2) is Relation-like NAT -defined f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (f,K,V1,a,b1,b2)) -tuples_on f
width (f,K,V1,a,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width (f,K,V1,a,b1,b2)) -tuples_on f is FinSequenceSet of f
dom (f,K,V1,a,b1,b2) is finite set
(f,K,V1,a,b1,b2) . V2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b1 . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 is non empty set
V2 * is functional non empty FinSequence-membered FinSequenceSet of V2
f is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a,V2
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b1 is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a,V2
width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(V2,K,V1,a,f,b1) is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a,V2
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
width (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
rng (V2,K,V1,a,f,b1) is finite set
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
len (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) + (len b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) + (len b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
0 + 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
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
rng f is finite set
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p2 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b4 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
len b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
rng b1 is finite set
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p2 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b4 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
len b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (V2,K,V1,a,f,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
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b1 is non empty set
b1 * is functional non empty FinSequence-membered FinSequenceSet of b1
b2 is Relation-like NAT -defined b1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a,b1
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len b2) + V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i is Relation-like NAT -defined b1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a,b1
dom i is finite set
(b1,K,V1,a,b2,i) is Relation-like NAT -defined b1 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a,b1
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Line ((b1,K,V1,a,b2,i),f) is Relation-like NAT -defined b1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (b1,K,V1,a,b2,i)) -tuples_on b1
width (b1,K,V1,a,b2,i) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width (b1,K,V1,a,b2,i)) -tuples_on b1 is FinSequenceSet of b1
Line (i,V2) is Relation-like NAT -defined b1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width i) -tuples_on b1
width i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width i) -tuples_on b1 is FinSequenceSet of b1
dom (b1,K,V1,a,b2,i) is finite set
(b1,K,V1,a,b2,i) . f is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 is non empty set
V2 * is functional non empty FinSequence-membered FinSequenceSet of V2
f is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a,V2
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (width f) is finite V43( width f) Element of bool NAT
b1 is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a,V2
width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(V2,K,V1,a,f,b1) is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a,V2
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Col ((V2,K,V1,a,f,b1),b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len (V2,K,V1,a,f,b1)) -tuples_on V2
len (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (V2,K,V1,a,f,b1)) -tuples_on V2 is FinSequenceSet of V2
Col (f,b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on V2
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) -tuples_on V2 is FinSequenceSet of V2
Col (b1,b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len b1) -tuples_on V2
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len b1) -tuples_on V2 is FinSequenceSet of V2
(Col (f,b2)) ^ (Col (b1,b2)) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
dom (Col ((V2,K,V1,a,f,b1),b2)) is finite set
len (Col ((V2,K,V1,a,f,b1),b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (Col ((V2,K,V1,a,f,b1),b2))) is finite V43( len (Col ((V2,K,V1,a,f,b1),b2))) Element of bool NAT
(len f) + (len b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (Col (b1,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) + (len (Col (b1,b2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (Col (f,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (Col (f,b2))) + (len (Col (b1,b2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len ((Col (f,b2)) ^ (Col (b1,b2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Seg (len (V2,K,V1,a,f,b1)) is finite V43( len (V2,K,V1,a,f,b1)) Element of bool NAT
dom (V2,K,V1,a,f,b1) is finite set
width (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (width (V2,K,V1,a,f,b1)) is finite V43( width (V2,K,V1,a,f,b1)) Element of bool NAT
[i,b2] is set
{i,b2} is non empty finite V40() set
{i} is non empty trivial finite V40() V43(1) set
{{i,b2},{i}} is non empty finite V40() set
[:(dom (V2,K,V1,a,f,b1)),(Seg (width (V2,K,V1,a,f,b1))):] is Relation-like finite set
Indices (V2,K,V1,a,f,b1) is set
(V2,K,V1,a,f,b1) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(V2,K,V1,a,f,b1) * (i,b2) is Element of V2
j is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
j . b2 is set
dom ((Col (f,b2)) ^ (Col (b1,b2))) is finite set
dom (Col (f,b2)) is finite set
Seg (len (Col (f,b2))) is finite V43( len (Col (f,b2))) Element of bool NAT
Seg (len f) is finite V43( len f) Element of bool NAT
dom f is finite set
[:(dom f),(Seg (width f)):] is Relation-like finite set
Indices f is set
f . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
f * (i,b2) is Element of V2
p2 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
p2 . b2 is set
(Col ((V2,K,V1,a,f,b1),b2)) . i is set
(Col (f,b2)) . i is set
((Col (f,b2)) ^ (Col (b1,b2))) . i is set
dom (Col (b1,b2)) is finite set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(len (Col (f,b2))) + p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(len (Col (f,b2))) + p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (Col (b1,b2))) is finite V43( len (Col (b1,b2))) Element of bool NAT
Seg (len b1) is finite V43( len b1) Element of bool NAT
dom b1 is finite set
[p2,b2] is set
{p2,b2} is non empty finite V40() set
{p2} is non empty trivial finite V40() V43(1) set
{{p2,b2},{p2}} is non empty finite V40() set
Seg (width b1) is finite V43( width b1) Element of bool NAT
[:(dom b1),(Seg (width b1)):] is Relation-like finite set
Indices b1 is set
b1 . p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b1 * (p2,b2) is Element of V2
b4 is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
b4 . b2 is set
(Col ((V2,K,V1,a,f,b1),b2)) . i is set
(Col (b1,b2)) . p2 is set
((Col (f,b2)) ^ (Col (b1,b2))) . i is set
dom (Col (f,b2)) is finite set
dom (Col (b1,b2)) is finite set
(Col ((V2,K,V1,a,f,b1),b2)) . i is set
((Col (f,b2)) ^ (Col (b1,b2))) . i is set
(Col ((V2,K,V1,a,f,b1),b2)) . i is set
((Col (f,b2)) ^ (Col (b1,b2))) . i is set
K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 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
f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V2
the carrier of f is non empty set
the carrier of f * is functional non empty FinSequence-membered FinSequenceSet of the carrier of f
b1 is Relation-like NAT -defined the carrier of f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a, the carrier of f
(f,b1) is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of f
b2 is Relation-like NAT -defined the carrier of f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a, the carrier of f
( the carrier of f,K,V1,a,b1,b2) is Relation-like NAT -defined the carrier of f * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a, the carrier of f
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(f,( the carrier of f,K,V1,a,b1,b2)) is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of f
(f,b2) is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of f
(f,b1) ^ (f,b2) is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of f
dom (f,( the carrier of f,K,V1,a,b1,b2)) is finite set
len (f,( the carrier of f,K,V1,a,b1,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (f,( the carrier of f,K,V1,a,b1,b2))) is finite V43( len (f,( the carrier of f,K,V1,a,b1,b2))) Element of bool NAT
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
len ( the carrier of f,K,V1,a,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len ( the carrier of f,K,V1,a,b1,b2)) is finite V43( len ( the carrier of f,K,V1,a,b1,b2)) Element of bool NAT
dom ( the carrier of f,K,V1,a,b1,b2) is finite set
dom b1 is finite set
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (f,b1) is finite set
(f,( the carrier of f,K,V1,a,b1,b2)) . i is set
(f,( the carrier of f,K,V1,a,b1,b2)) /. i is Element of the carrier of f
( the carrier of f,K,V1,a,b1,b2) /. i is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of f *
Sum (( the carrier of f,K,V1,a,b1,b2) /. i) is Element of the carrier of f
b1 /. i is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of f *
Sum (b1 /. i) is Element of the carrier of f
(f,b1) /. i is Element of the carrier of f
(f,b1) . i is set
((f,b1) ^ (f,b2)) . i is set
dom b2 is finite set
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (f,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (f,b2) is finite set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(len b1) + j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(len b1) + j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(f,( the carrier of f,K,V1,a,b1,b2)) . i is set
(f,( the carrier of f,K,V1,a,b1,b2)) /. i is Element of the carrier of f
( the carrier of f,K,V1,a,b1,b2) /. i is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of f *
Sum (( the carrier of f,K,V1,a,b1,b2) /. i) is Element of the carrier of f
b2 /. j is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of f *
Sum (b2 /. j) is Element of the carrier of f
(f,b2) /. j is Element of the carrier of f
(f,b2) . j is set
((f,b1) ^ (f,b2)) . i is set
dom b1 is finite set
dom b2 is finite set
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(f,( the carrier of f,K,V1,a,b1,b2)) . i is set
((f,b1) ^ (f,b2)) . i is set
(f,( the carrier of f,K,V1,a,b1,b2)) . i is set
((f,b1) ^ (f,b2)) . i is set
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len b1) + (len b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (f,b1)) + (len b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (f,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (f,b1)) + (len (f,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len ((f,b1) ^ (f,b2)) 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
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 is non empty set
V2 * is functional non empty FinSequence-membered FinSequenceSet of V2
f is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K,a,V2
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
f @ is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V2 *
b1 is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V1,a,V2
width b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(V2,K,V1,a,f,b1) is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of K + V1,a,V2
K + V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(V2,K,V1,a,f,b1) @ is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V2 *
b1 @ is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V2 *
(V2,(f @),(b1 @)) is Relation-like NAT -defined V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of V2 *
len (V2,(f @),(b1 @)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (V2,(f @),(b1 @))) is finite V43( len (V2,(f @),(b1 @))) Element of bool NAT
dom (V2,(f @),(b1 @)) is finite set
dom (f @) is finite set
dom (b1 @) is finite set
(dom (f @)) /\ (dom (b1 @)) is finite set
len (b1 @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (b1 @)) is finite V43( len (b1 @)) Element of bool NAT
(dom (f @)) /\ (Seg (len (b1 @))) is finite Element of bool NAT
len (f @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (f @)) is finite V43( len (f @)) Element of bool NAT
(Seg (len (f @))) /\ (Seg (len (b1 @))) is finite Element of bool NAT
Seg (width f) is finite V43( width f) Element of bool NAT
(Seg (width f)) /\ (Seg (len (b1 @))) is finite Element of bool NAT
Seg (width b1) is finite V43( width b1) Element of bool NAT
(Seg (width f)) /\ (Seg (width b1)) is finite Element of bool NAT
dom ((V2,K,V1,a,f,b1) @) is finite set
len ((V2,K,V1,a,f,b1) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len ((V2,K,V1,a,f,b1) @)) is finite V43( len ((V2,K,V1,a,f,b1) @)) Element of bool NAT
width (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Seg (width (V2,K,V1,a,f,b1)) is finite V43( width (V2,K,V1,a,f,b1)) Element of bool NAT
(f @) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(b1 @) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(Seg (len (f @))) /\ (dom (b1 @)) is finite Element of bool NAT
((V2,K,V1,a,f,b1) @) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (((V2,K,V1,a,f,b1) @),b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width ((V2,K,V1,a,f,b1) @)) -tuples_on V2
width ((V2,K,V1,a,f,b1) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width ((V2,K,V1,a,f,b1) @)) -tuples_on V2 is FinSequenceSet of V2
Col ((V2,K,V1,a,f,b1),b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len (V2,K,V1,a,f,b1)) -tuples_on V2
len (V2,K,V1,a,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (V2,K,V1,a,f,b1)) -tuples_on V2 is FinSequenceSet of V2
Col (f,b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on V2
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) -tuples_on V2 is FinSequenceSet of V2
Col (b1,b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len b1) -tuples_on V2
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len b1) -tuples_on V2 is FinSequenceSet of V2
(Col (f,b2)) ^ (Col (b1,b2)) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
Line ((f @),b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (f @)) -tuples_on V2
width (f @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width (f @)) -tuples_on V2 is FinSequenceSet of V2
(Line ((f @),b2)) ^ (Col (b1,b2)) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
Line ((b1 @),b2) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (b1 @)) -tuples_on V2
width (b1 @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width (b1 @)) -tuples_on V2 is FinSequenceSet of V2
(Line ((f @),b2)) ^ (Line ((b1 @),b2)) is Relation-like NAT -defined V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of V2
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(Line ((f @),b2)) ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(V2,(f @),(b1 @)) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support 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
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 *
(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
V2 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 *
(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
(a,V1) + (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
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 .: ((a,V1),(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
<:(a,V1),(a,V2):> is Relation-like Function-like set
<:(a,V1),(a,V2):> (#) the addF of a is Relation-like the carrier of a -valued Function-like set
( the carrier of a,V1,V2) 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 *
(a,( the carrier 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
len V1 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
min ((len V1),(len V2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg f is finite V43(f) Element of bool NAT
Seg (len V1) is finite V43( len V1) Element of bool NAT
Seg (len V2) is finite V43( len V2) Element of bool NAT
(Seg (len V1)) /\ (Seg (len V2)) is finite Element of bool NAT
dom V2 is finite set
(Seg (len V1)) /\ (dom V2) is finite Element of bool NAT
dom V1 is finite set
(dom V1) /\ (dom V2) is finite set
dom ( the carrier of a,V1,V2) is finite set
len ( the carrier of a,V1,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len ( the carrier of a,V1,V2)) is finite V43( len ( the carrier of a,V1,V2)) Element of bool NAT
len ((a,V1) + (a,V2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (a,V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (a,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
min ((len (a,V1)),(len (a,V2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
min ((len V1),(len (a,V2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
len (a,( the carrier of a,V1,V2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom ((a,V1) + (a,V2)) is finite set
Seg (len ((a,V1) + (a,V2))) is finite V43( len ((a,V1) + (a,V2))) Element of bool NAT
b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom (a,( the carrier of a,V1,V2)) is finite set
V1 . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
V2 . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
V1 /. b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element 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 Element of the carrier of a *
(V1 /. b1) ^ (V2 /. b1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of a *
b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b2 ^ (V2 /. b1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b2 ^ i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
( the carrier of a,V1,V2) . b1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
( the carrier of a,V1,V2) /. b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of a *
Seg (len (a,V2)) is finite V43( len (a,V2)) Element of bool NAT
dom (a,V2) is finite set
(a,V2) /. b1 is Element of the carrier of a
(a,V2) . b1 is set
Seg (len (a,V1)) is finite V43( len (a,V1)) Element of bool NAT
dom (a,V1) is finite set
(a,V1) /. b1 is Element of the carrier of a
(a,V1) . b1 is set
((a,V1) + (a,V2)) . b1 is set
((a,V1) /. b1) + ((a,V2) /. b1) is Element of the carrier of a
the addF of a . (((a,V1) /. b1),((a,V2) /. b1)) is Element of the carrier of a
Sum (V1 /. b1) is Element of the carrier of a
(Sum (V1 /. b1)) + ((a,V2) /. b1) is Element of the carrier of a
the addF of a . ((Sum (V1 /. b1)),((a,V2) /. b1)) is Element of the carrier of a
Sum (V2 /. b1) is Element of the carrier of a
(Sum (V1 /. b1)) + (Sum (V2 /. b1)) is Element of the carrier of a
the addF of a . ((Sum (V1 /. b1)),(Sum (V2 /. b1))) is Element of the carrier of a
Sum (( the carrier of a,V1,V2) /. b1) is Element of the carrier of a
(a,( the carrier of a,V1,V2)) /. b1 is Element of the carrier of a
(a,( the carrier of a,V1,V2)) . b1 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
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
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
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
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
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 .: (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 addF of a is Relation-like the carrier of a -valued Function-like set
Sum (V1 + V2) is Element of the carrier of a
Sum V1 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 . ((Sum V1),(Sum V2)) is Element of the carrier of a
(len V1) -tuples_on the carrier of a is FinSequenceSet 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 Element of (len V1) -tuples_on the carrier of a
b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len V1) -tuples_on the carrier of a
f + b1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len V1) -tuples_on the carrier of a
the addF of a .: (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
<:f,b1:> is Relation-like Function-like set
<:f,b1:> (#) the addF of a is Relation-like the carrier of a -valued Function-like set
Sum (f + b1) 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
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
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
V2 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 V2 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
(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
Sum (a,V2) is Element of the carrier of a
(Sum (a,V1)) + (Sum (a,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 (a,V1)),(Sum (a,V2))) is Element of the carrier of a
( the carrier of a,V1,V2) 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 *
(a,( the carrier 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
Sum (a,( the carrier of a,V1,V2)) 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
len (a,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(a,V1) + (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
the addF of a .: ((a,V1),(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
<:(a,V1),(a,V2):> is Relation-like Function-like set
<:(a,V1),(a,V2):> (#) the addF of a is Relation-like the carrier of a -valued Function-like set
Sum ((a,V1) + (a,V2)) 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
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
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 *
(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
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 *
(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
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 carrier of a,V2) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len V2, the carrier of a
len V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(a,( 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
Sum (a,( the carrier of a,V2)) is Element of the carrier of a
( the carrier of a,V2) @ 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 *
(a,(( 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
Sum (a,(( the carrier of a,V2) @)) 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,(<*> the carrier of a)) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len (<*> the carrier of a), the carrier of a
len (<*> the carrier of a) 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
len ( the carrier of a,(<*> the carrier of a)) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
width ( the carrier of a,(<*> the carrier of a)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
( the carrier of a,(<*> the carrier of a)) @ 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 (( the carrier of a,(<*> the carrier of a)) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
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 carrier of a,f) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len f, the carrier of a
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(a,( 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
Sum (a,( the carrier of a,f)) is Element of the carrier of a
( the carrier of a,f) @ 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 *
(a,(( 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
Sum (a,(( the carrier of a,f) @)) is Element of the carrier of a
b1 is Element of the carrier of a
<*b1*> 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 *
f ^ <*b1*> 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
( the carrier of a,(f ^ <*b1*>)) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len (f ^ <*b1*>), the carrier of a
len (f ^ <*b1*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(a,( the carrier of a,(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
Sum (a,( the carrier of a,(f ^ <*b1*>))) is Element of the carrier of a
( the carrier of a,(f ^ <*b1*>)) @ 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 *
(a,(( the carrier of a,(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
Sum (a,(( the carrier of a,(f ^ <*b1*>)) @)) is Element of the carrier of a
( the carrier of a,<*b1*>) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len <*b1*>, the carrier of a
len <*b1*> is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>)) 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 ( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len ( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>))) is finite V43( len ( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>))) Element of bool NAT
dom ( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>)) is finite set
dom ( the carrier of a,f) is non empty trivial finite V43(1) set
dom ( the carrier of a,<*b1*>) is non empty trivial finite V43(1) set
(dom ( the carrier of a,f)) /\ (dom ( the carrier of a,<*b1*>)) is finite set
(Seg 1) /\ (dom ( the carrier of a,<*b1*>)) is finite Element of bool NAT
(Seg 1) /\ (Seg 1) is finite Element of bool NAT
len ( the carrier of a,(f ^ <*b1*>)) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
Seg (len ( the carrier of a,(f ^ <*b1*>))) is non empty finite V43( len ( the carrier of a,(f ^ <*b1*>))) Element of bool NAT
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
( the carrier of a,f) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
( the carrier of a,<*b1*>) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>)) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
f ^ j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
( the carrier of a,(f ^ <*b1*>)) . b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(a,( 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
Sum (a,( the carrier of a,<*b1*>)) is Element of the carrier of a
( the carrier of a,<*b1*>) @ 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 *
(a,(( 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
Sum (a,(( the carrier of a,<*b1*>) @)) is Element of the carrier of a
len ( the carrier of a,<*b1*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
width ( the carrier of a,<*b1*>) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
( the carrier of a,<*b1*>) @ 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 (( the carrier of a,<*b1*>) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len ( the carrier of a,f) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
width ( the carrier of a,f) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (( the carrier of a,f) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (( the carrier of a,f) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width ( the carrier of a,(f ^ <*b1*>)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len f) + (len <*b1*>) is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(len f) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(( the carrier of a,<*b1*>) @) @ 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 *
width (( the carrier of a,<*b1*>) @) is V24() V25() V26() V30() V31() ext-real 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 V144() tabular FinSequence-yielding finite-support Matrix of len f,1, the carrier of a
i is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1,1, the carrier of a
( the carrier of a,(len f),1,1,b2,i) is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of (len f) + 1,1, the carrier of a
(len f) + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() set
( the carrier of a,(len f),1,1,b2,i) @ 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 *
(( the carrier of a,f) @) @ 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 *
( the carrier of a,((( the carrier of a,f) @) @),((( the carrier of a,<*b1*>) @) @)) 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 *
(( the carrier of a,(f ^ <*b1*>)) @) @ 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 *
(( the carrier of a,f) @) ^ (( the carrier of a,<*b1*>) @) is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() FinSequence-yielding finite-support FinSequence of the carrier of a *
len ((( the carrier of a,f) @) ^ (( the carrier of a,<*b1*>) @)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len (( the carrier of a,f) @)) + (len (( the carrier of a,<*b1*>) @)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width ( the carrier of a,f)) + (len (( the carrier of a,<*b1*>) @)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width ( the carrier of a,f)) + (width ( the carrier of a,<*b1*>)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (( the carrier of a,(f ^ <*b1*>)) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(a,( the carrier of a,( the carrier of a,f),( 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
Sum (a,( the carrier of a,( the carrier of a,f),( the carrier of a,<*b1*>))) is Element of the carrier of a
(a,( 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
Sum (a,( the carrier of a,<*b1*>)) is Element of the carrier of a
(Sum (a,(( the carrier of a,f) @))) + (Sum (a,( the carrier of a,<*b1*>))) 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 (a,(( the carrier of a,f) @))),(Sum (a,( the carrier of a,<*b1*>)))) is Element of the carrier of a
(a,(( 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
Sum (a,(( the carrier of a,<*b1*>) @)) is Element of the carrier of a
(Sum (a,(( the carrier of a,f) @))) + (Sum (a,(( the carrier of a,<*b1*>) @))) is Element of the carrier of a
the addF of a . ((Sum (a,(( the carrier of a,f) @))),(Sum (a,(( the carrier of a,<*b1*>) @)))) is Element of the carrier of a
(a,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
(a,i) 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
(a,b2) ^ (a,i) 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,b2) ^ (a,i)) is Element of the carrier of a
(a,( the carrier of a,(len f),1,1,b2,i)) 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,( the carrier of a,(len f),1,1,b2,i)) is Element of the carrier of a
0 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
(a,( the carrier of a,(<*> the carrier of a))) 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,( the carrier of a,(<*> the carrier of a))) is Element of the carrier of a
0. a is V56(a) Element of the carrier of a
(a,(( the carrier of a,(<*> the carrier of a)) @)) 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,(( the carrier of a,(<*> the carrier of a)) @)) is Element of the carrier of a
V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() Element of NAT
f 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 f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(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
Sum (a,f) 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 V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of a *
(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
Sum (a,(f @)) is Element of the carrier of a
dom f is finite set
Seg (len f) is finite V43( len f) Element of bool NAT
f . 1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (f,1) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width f) -tuples_on the carrier of a
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width f) -tuples_on the carrier of a is FinSequenceSet 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
( the carrier of a,b1) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len b1, the carrier of a
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
f . (V2 + 1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (f,(V2 + 1)) is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width f) -tuples_on the carrier of a
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width f) -tuples_on the carrier of a is FinSequenceSet 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
( the carrier of a,b1) is Relation-like NAT -defined the carrier of a * -valued Function-like constant non empty trivial finite V43(1) FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of 1, len b1, the carrier of a
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V2 + 1, width f, the carrier of a
( the carrier of a,(V2 + 1),i) 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 *
j is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V2, width f, the carrier of a
width j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width i is V24() V25() V26() V30() V31() ext-real 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 V144() tabular FinSequence-yielding finite-support Matrix of 1, width f, the carrier of a
width b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j @ 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 (j @) is V24() V25() V26() V30() V31() ext-real 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 V144() tabular FinSequence-yielding 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
( the carrier of a,(V2 + 1),f) 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 ( the carrier of a,(V2 + 1),f) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
( the carrier of a,V2,1,(width f),j,b2) is Relation-like NAT -defined the carrier of a * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of V2 + 1, width f, the carrier of a
V2 + 1 is non empty V24() V25() V26() V30() V31() ext-real positive non negative V35() finite V41() set
(a,( the carrier of a,V2,1,(width f),j,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
Sum (a,( the carrier of a,V2,1,(width f),j,b2)) is Element of the carrier of a
(a,j) 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
(a,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
(a,j) ^ (a,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
Sum ((a,j) ^ (a,b2)) is Element of the carrier of a
(a,( the carrier of a,(V2 + 1),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 (a,( the carrier of a,(V2 + 1),f)) is Element of the carrier of a
Sum (a,b2) is Element of the carrier of a
(Sum (a,( the carrier of a,(V2 + 1),f))) + (Sum (a,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 (a,( the carrier of a,(V2 + 1),f))),(Sum (a,b2))) is Element of the carrier of a
( the carrier of a,(V2 + 1),f) @ 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 *
(a,(( the carrier of a,(V2 + 1),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 (a,(( the carrier of a,(V2 + 1),f) @)) is Element of the carrier of a
(Sum (a,(( the carrier of a,(V2 + 1),f) @))) + (Sum (a,b2)) is Element of the carrier of a
the addF of a . ((Sum (a,(( the carrier of a,(V2 + 1),f) @))),(Sum (a,b2))) is Element of the carrier of a
(a,(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
Sum (a,(b2 @)) is Element of the carrier of a
(Sum (a,(( the carrier of a,(V2 + 1),f) @))) + (Sum (a,(b2 @))) is Element of the carrier of a
the addF of a . ((Sum (a,(( the carrier of a,(V2 + 1),f) @))),(Sum (a,(b2 @)))) is Element of the carrier of a
( the carrier of a,(j @),(b2 @)) 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 *
(a,( the carrier of a,(j @),(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
Sum (a,( the carrier of a,(j @),(b2 @))) is Element of the carrier of a
( the carrier of a,V2,1,(width f),j,b2) @ 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 *
(a,(( the carrier of a,V2,1,(width f),j,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
Sum (a,(( the carrier of a,V2,1,(width f),j,b2) @)) 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 V144() tabular FinSequence-yielding 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
(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
Sum (a,V2) 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 V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of a *
(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
Sum (a,(V2 @)) is Element of the carrier of a
width V2 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
0. a is V56(a) Element of the carrier of a
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
V2 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 V2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(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
Sum (a,V2) 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 V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of a *
(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
Sum (a,(V2 @)) is Element of the carrier of a
K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 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 V1 is non empty non trivial set
the carrier of V1 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
V2 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (V1) VectSpStr over V1
the carrier of V2 is non empty set
f 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,a, the carrier of V1
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i 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 i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j 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 j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom j is finite set
p2 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b4 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom b4 is finite set
(V1,V2,i,b4) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
the lmult of V2 is Relation-like [: the carrier of V1, the carrier of V2:] -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of V1, the carrier of V2:], the carrier of V2:]
[: the carrier of V1, the carrier of V2:] is Relation-like non empty set
[:[: the carrier of V1, the carrier of V2:], the carrier of V2:] is Relation-like non empty set
bool [:[: the carrier of V1, the carrier of V2:], the carrier of V2:] is non empty set
the lmult of V2 .: (i,b4) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
<:i,b4:> is Relation-like Function-like set
<:i,b4:> (#) the lmult of V2 is Relation-like the carrier of V2 -valued Function-like set
Sum (V1,V2,i,b4) is Element of the carrier of V2
(V1,V2,j,p2) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
the lmult of V2 .: (j,p2) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
<:j,p2:> is Relation-like Function-like set
<:j,p2:> (#) the lmult of V2 is Relation-like the carrier of V2 -valued Function-like set
Sum (V1,V2,j,p2) is Element of the carrier of V2
the carrier of V2 * is functional non empty FinSequence-membered FinSequenceSet of the carrier of V2
b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p1 is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of b1,b2, the carrier of V2
Indices p1 is set
width p1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p1 @ is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of V2 *
len (p1 @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(V2,(p1 @)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len (V2,(p1 @)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p2 is finite set
dom (V1,V2,j,p2) is finite set
len (V1,V2,j,p2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (V2,(p1 @))) is finite V43( len (V2,(p1 @))) Element of bool NAT
len p1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (V2,(p1 @)) is finite set
KL1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
j /. KL1 is Element of the carrier of V1
j . KL1 is set
p2 /. KL1 is Element of the carrier of V2
p2 . KL1 is set
dom (p1 @) is finite set
(p1 @) /. KL1 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of V2 *
(p1 @) . KL1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line ((p1 @),KL1) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (p1 @)) -tuples_on the carrier of V2
width (p1 @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width (p1 @)) -tuples_on the carrier of V2 is FinSequenceSet of the carrier of V2
Col (f,KL1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len f) -tuples_on the carrier of V1
(len f) -tuples_on the carrier of V1 is FinSequenceSet of the carrier of V1
mlt (i,(Col (f,KL1))) 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 multF 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 multF of V1 .: (i,(Col (f,KL1))) 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
<:i,(Col (f,KL1)):> is Relation-like Function-like set
<:i,(Col (f,KL1)):> (#) the multF of V1 is Relation-like the carrier of V1 -valued Function-like set
KL2 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
p3 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len p3 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p3 is finite set
len (Col (f,KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len ( the multF of V1 .: (i,(Col (f,KL1)))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom KL2 is finite set
dom i is finite set
len (Line ((p1 @),KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(p1 @) @ is Relation-like NAT -defined the carrier of V2 * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of V2 *
len ((p1 @) @) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (Line ((p1 @),KL1)) is finite set
Seg (len p3) is finite V43( len p3) Element of bool NAT
Seg (len i) is finite V43( len i) Element of bool NAT
dom f is finite set
Seg (len f) is finite V43( len f) Element of bool NAT
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
Seg (len ( the multF of V1 .: (i,(Col (f,KL1))))) is finite V43( len ( the multF of V1 .: (i,(Col (f,KL1))))) Element of bool NAT
dom ( the multF of V1 .: (i,(Col (f,KL1)))) is finite set
i /. p2 is Element of the carrier of V1
f * (p2,KL1) is Element of the carrier of V1
(i /. p2) * (f * (p2,KL1)) is Element of the carrier of V1
the multF of V1 . ((i /. p2),(f * (p2,KL1))) is Element of the carrier of V1
i . p2 is set
the multF of V1 . ((i . p2),(f * (p2,KL1))) is set
(Col (f,KL1)) . p2 is set
the multF of V1 . ((i . p2),((Col (f,KL1)) . p2)) is set
( the multF of V1 .: (i,(Col (f,KL1)))) . p2 is set
KL2 /. p2 is Element of the carrier of V1
dom p1 is finite set
[p2,KL1] is set
{p2,KL1} is non empty finite V40() set
{p2} is non empty trivial finite V40() V43(1) set
{{p2,KL1},{p2}} is non empty finite V40() set
Seg (width p1) is finite V43( width p1) Element of bool NAT
[:(dom p1),(Seg (width p1)):] is Relation-like finite set
Seg (width (p1 @)) is finite V43( width (p1 @)) Element of bool NAT
(Line ((p1 @),KL1)) . p2 is set
(p1 @) * (KL1,p2) is Element of the carrier of V2
p1 * (p2,KL1) is Element of the carrier of V2
(KL2 /. p2) * (p2 /. KL1) is Element of the carrier of V2
p3 . p2 is set
(V1,V2,j,p2) . KL1 is set
the lmult of V2 . ((j . KL1),(p2 . KL1)) is set
(j /. KL1) * (p2 /. KL1) is Element of the carrier of V2
Sum KL2 is Element of the carrier of V1
(Sum KL2) * (p2 /. KL1) is Element of the carrier of V2
Sum p3 is Element of the carrier of V2
Sum ((p1 @) /. KL1) is Element of the carrier of V2
(V2,(p1 @)) /. KL1 is Element of the carrier of V2
(V2,(p1 @)) . KL1 is set
dom (V1,V2,i,b4) is finite set
len (V1,V2,i,b4) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(V2,p1) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len (V2,p1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom (V2,p1) is finite set
b4 . KL1 is set
b4 /. KL1 is Element of the carrier of V2
i . KL1 is set
i /. KL1 is Element of the carrier of V1
Seg (len (V2,p1)) is finite V43( len (V2,p1)) Element of bool NAT
Seg (len p1) is finite V43( len p1) Element of bool NAT
p1 /. KL1 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of the carrier of V2 *
p1 . KL1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
Line (p1,KL1) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width p1) -tuples_on the carrier of V2
(width p1) -tuples_on the carrier of V2 is FinSequenceSet of the carrier of V2
Line (f,KL1) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width f) -tuples_on the carrier of V1
width f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(width f) -tuples_on the carrier of V1 is FinSequenceSet of the carrier of V1
(V1,V2,(Line (f,KL1)),p2) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
the lmult of V2 .: ((Line (f,KL1)),p2) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
<:(Line (f,KL1)),p2:> is Relation-like Function-like set
<:(Line (f,KL1)),p2:> (#) the lmult of V2 is Relation-like the carrier of V2 -valued Function-like set
KL2 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
len KL2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom KL2 is finite set
dom (Line (f,KL1)) is finite set
len (Line (f,KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (Line (f,KL1))) is finite V43( len (Line (f,KL1))) Element of bool NAT
Seg (len KL2) is finite V43( len KL2) Element of bool NAT
dom (V1,V2,(Line (f,KL1)),p2) is finite set
len (V1,V2,(Line (f,KL1)),p2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (Line (p1,KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (p1 /. KL1) is finite set
Seg (len p2) is finite V43( len p2) Element of bool NAT
p3 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(Line (f,KL1)) . p3 is set
f * (KL1,p3) is Element of the carrier of V1
[KL1,p3] is set
{KL1,p3} is non empty finite V40() set
{KL1} is non empty trivial finite V40() V43(1) set
{{KL1,p3},{KL1}} is non empty finite V40() set
p2 . p3 is set
p2 /. p3 is Element of the carrier of V2
(V1,V2,(Line (f,KL1)),p2) /. p3 is Element of the carrier of V2
(V1,V2,(Line (f,KL1)),p2) . p3 is set
the lmult of V2 . (((Line (f,KL1)) . p3),(p2 . p3)) is set
(f * (KL1,p3)) * (p2 /. p3) is Element of the carrier of V2
(p1 /. KL1) . p3 is set
p1 * (KL1,p3) is Element of the carrier of V2
(i /. KL1) * (f * (KL1,p3)) is Element of the carrier of V1
the multF of V1 . ((i /. KL1),(f * (KL1,p3))) is Element of the carrier of V1
((i /. KL1) * (f * (KL1,p3))) * (p2 /. p3) is Element of the carrier of V2
(i /. KL1) * ((V1,V2,(Line (f,KL1)),p2) /. p3) is Element of the carrier of V2
KL2 . p3 is set
p3 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL2 . p3 is set
(V1,V2,(Line (f,KL1)),p2) /. p3 is Element of the carrier of V2
(i /. KL1) * ((V1,V2,(Line (f,KL1)),p2) /. p3) is Element of the carrier of V2
dom ( the lmult of V2 .: (i,b4)) is finite set
(V1,V2,i,b4) . KL1 is set
the lmult of V2 . ((i . KL1),(b4 . KL1)) is set
(i /. KL1) * (b4 /. KL1) is Element of the carrier of V2
Sum (V1,V2,(Line (f,KL1)),p2) is Element of the carrier of V2
(i /. KL1) * (Sum (V1,V2,(Line (f,KL1)),p2)) is Element of the carrier of V2
Sum KL2 is Element of the carrier of V2
Sum (p1 /. KL1) is Element of the carrier of V2
(V2,p1) /. KL1 is Element of the carrier of V2
(V2,p1) . KL1 is set
Sum (V2,p1) is Element of the carrier of V2
Sum (V2,(p1 @)) is Element of the carrier of V2
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 K is non empty non trivial set
V1 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,a)
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
V2 is Element of the carrier of a
rng V1 is finite set
f is Basis of a
b1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
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
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
dom b2 is finite set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b2 /. i is Element of the carrier of K
V1 /. i is Element of the carrier of a
b1 . (V1 /. i) is Element of the carrier of K
Seg (len V1) is finite V43( len V1) Element of bool NAT
b2 . i is set
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
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
i is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
Sum i is Element of the carrier of a
Carrier i is finite Element of bool the carrier of a
bool the carrier of a is non empty set
j is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
Sum j is Element of the carrier of a
Carrier j is finite Element of bool the carrier of a
f is Basis of a
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b1 . p2 is set
b2 . p2 is set
dom b2 is finite set
dom b1 is finite set
b1 /. p2 is Element of the carrier of K
V1 /. p2 is Element of the carrier of a
i . (V1 /. p2) is Element of the carrier of K
j . (V1 /. p2) is Element of the carrier of K
b2 /. p2 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
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 (K,a)
dom V1 is finite set
V2 is Element of the carrier of a
(K,a,V1,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
the carrier of K is non empty non trivial set
dom (K,a,V1,V2) is finite set
len (K,a,V1,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len V1 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 (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 (K,a)
V2 is Element of the carrier of a
(K,a,V1,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
the carrier of K is non empty non trivial set
f is Element of the carrier of a
(K,a,V1,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
rng V1 is finite set
len (K,a,V1,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
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
len (K,a,V1,f) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
Sum b2 is Element of the carrier of a
Carrier b2 is finite Element of bool the carrier of a
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 /. i is Element of the carrier of a
b1 . (V1 /. i) is Element of the carrier of K
(K,a,V1,f) /. i is Element of the carrier of K
b2 . (V1 /. i) is Element of the carrier of K
(Carrier b1) \/ (Carrier b2) is finite Element of bool the carrier of a
i is Element of the carrier of a
b2 . i is Element of the carrier of K
0. K is V56(K) Element of the carrier of K
b1 . i is Element of the carrier of K
i is Element of the carrier of a
dom V1 is finite set
j is set
V1 . j is set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
V1 /. p2 is Element of the carrier of a
b1 . i is Element of the carrier of K
b2 . i is Element of the carrier of K
i 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
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 (K,a)
V2 is Element of the carrier of a
(K,a,V1,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
the carrier of K is non empty non trivial set
(K,a,(K,a,V1,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 .: ((K,a,V1,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
<:(K,a,V1,V2),V1:> is Relation-like Function-like set
<:(K,a,V1,V2),V1:> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set
Sum (K,a,(K,a,V1,V2),V1) is Element of the carrier of a
rng V1 is finite set
len (K,a,V1,V2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
f is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
Sum f is Element of the carrier of a
Carrier f is finite Element of bool the carrier of a
bool the carrier of a is non empty set
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,a,V1,V2) is finite set
dom V1 is finite set
dom (K,a,(K,a,V1,V2),V1) is finite set
f (#) 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
len (f (#) V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,(K,a,V1,V2),V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (f (#) V1) is finite set
b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 /. b1 is Element of the carrier of a
V1 . b1 is set
(K,a,V1,V2) /. b1 is Element of the carrier of K
(K,a,V1,V2) . b1 is set
(f (#) V1) . b1 is set
f . (V1 /. b1) is Element of the carrier of K
(f . (V1 /. b1)) * (V1 /. b1) is Element of the carrier of a
((K,a,V1,V2) /. b1) * (V1 /. b1) is Element of the carrier of a
the lmult of a . (((K,a,V1,V2) . b1),(V1 . b1)) is set
(K,a,(K,a,V1,V2),V1) . b1 is set
Sum (f (#) V1) 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 (K,a)
len V1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
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
(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
Sum (K,a,V2,V1) is Element of the carrier of a
(K,a,V1,(Sum (K,a,V2,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
bool the carrier of a is non empty set
rng V1 is finite set
dom V1 is finite set
0. K is V56(K) Element of the carrier of K
b1 is Element of the carrier of a
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
V1 /. b2 is Element of the carrier of a
V2 /. b2 is Element of the carrier of K
i is Element of the carrier of K
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 /. j is Element of the carrier of a
V1 . j is set
V1 . b2 is set
V2 /. j is Element of the carrier of K
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 /. j is Element of the carrier of a
V2 /. j is Element of the carrier of K
b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V1 /. b2 is Element of the carrier of a
V2 /. b2 is Element of the carrier of K
[: the carrier of a, the carrier of K:] is Relation-like non empty set
bool [: the carrier of a, the carrier of K:] is non empty set
b1 is Relation-like the carrier of a -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of K:]
f is finite Element of bool the carrier of a
i is Element of the carrier of a
b2 is finite Element of bool the carrier of a
b1 . i is Element of the carrier of K
b2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of K:]
dom b2 is non empty set
rng b2 is non empty set
Funcs ( the carrier of a, the carrier of K) is functional non empty FUNCTION_DOMAIN of the carrier of a, the carrier of K
b2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of K:]
dom b2 is non empty set
rng b2 is non empty set
i is finite Element of bool the carrier of a
b2 is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
i is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
V2 /. j is Element of the carrier of K
V1 /. j is Element of the carrier of a
i . (V1 /. j) is Element of the carrier of K
V1 . j is set
Carrier i is finite Element of bool the carrier of a
j is set
p2 is Element of the carrier of a
i . p2 is Element of the carrier of K
dom V2 is finite set
dom (K,a,V2,V1) is finite set
len (K,a,V2,V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i (#) 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
len (i (#) V1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom (i (#) V1) is finite set
V2 /. j is Element of the carrier of K
V2 . j is set
V1 /. j is Element of the carrier of a
V1 . j is set
(K,a,V2,V1) . j is set
the lmult of a . ((V2 . j),(V1 . j)) is set
(V2 /. j) * (V1 /. j) is Element of the carrier of a
i . (V1 /. j) is Element of the carrier of K
(i . (V1 /. j)) * (V1 /. j) is Element of the carrier of a
(i (#) V1) . j is set
Sum (i (#) V1) is Element of the carrier of a
Sum i is Element of the carrier of a
i is Relation-like the carrier of a -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of a
Carrier i is finite Element of bool the carrier of a
Sum i is Element of the carrier of a
K is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom K is finite set
len K is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
a 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
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 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 (K,a)
len f is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom f is finite set
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
b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
dom b1 is finite set
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
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
(K,V1,b2,(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
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 .: (b2,(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
<:b2,(V2 * f):> is Relation-like Function-like set
<:b2,(V2 * f):> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set
Sum (K,V1,b2,(V2 * f)) is Element of the carrier of V1
(K,V1,b1,(Sum (K,V1,b2,(V2 * 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
mlt (b2,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
the multF 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 multF of K .: (b2,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
<:b2,i:> is Relation-like Function-like set
<:b2,i:> (#) the multF of K is Relation-like the carrier of K -valued Function-like set
Sum (mlt (b2,i)) is Element of the carrier of K
j 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 carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p2 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support Matrix of len f, len b1, the carrier of K
Indices p2 is set
b4 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 b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom b4 is finite set
p1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(K,V1,b1,(Sum (K,V1,b2,(V2 * f)))) /. p1 is Element of the carrier of K
Col (p2,p1) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len p2) -tuples_on the carrier of K
len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(len p2) -tuples_on the carrier of K is FinSequenceSet of the carrier of K
len (Col (p2,p1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p2 is finite set
len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom j is finite set
width p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
KL2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
j /. KL1 is Element of the carrier of V1
(K,V1,b1,(j /. KL1)) 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 (K,V1,b1,(j /. KL1)) is finite set
len (K,V1,b1,(j /. KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (K,V1,b1,(j /. KL1))) is finite V43( len (K,V1,b1,(j /. KL1))) Element of bool NAT
Seg (width p2) is finite V43( width p2) Element of bool NAT
[KL1,KL2] is set
{KL1,KL2} is non empty finite V40() set
{KL1} is non empty trivial finite V40() V43(1) set
{{KL1,KL2},{KL1}} is non empty finite V40() set
[:(dom p2),(Seg (width p2)):] is Relation-like finite set
Line (p2,KL1) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width p2) -tuples_on the carrier of K
(width p2) -tuples_on the carrier of K is FinSequenceSet of the carrier of K
(Line (p2,KL1)) . KL2 is set
p2 * (KL1,KL2) is Element of the carrier of K
(K,V1,b1,(j /. KL1)) /. KL2 is Element of the carrier of K
(K,V1,b1,(j /. KL1)) . KL2 is set
len (Line (p2,KL1)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(K,V1,(K,V1,b1,(j /. KL1)),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 .: ((K,V1,b1,(j /. KL1)),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
<:(K,V1,b1,(j /. KL1)),b1:> is Relation-like Function-like set
<:(K,V1,b1,(j /. KL1)),b1:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set
Sum (K,V1,(K,V1,b1,(j /. KL1)),b1) is Element of the carrier of V1
(K,V1,(Line (p2,KL1)),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 .: ((Line (p2,KL1)),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
<:(Line (p2,KL1)),b1:> is Relation-like Function-like set
<:(Line (p2,KL1)),b1:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set
Sum (K,V1,(Line (p2,KL1)),b1) is Element of the carrier of V1
Seg (len b1) is finite V43( len b1) Element of bool NAT
KL1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom i is finite set
j /. KL1 is Element of the carrier of V1
j . KL1 is set
f . KL1 is set
V2 . (f . KL1) is set
f /. KL1 is Element of the carrier of a
V2 . (f /. KL1) is Element of the carrier of V1
[KL1,p1] is set
{KL1,p1} is non empty finite V40() set
{KL1} is non empty trivial finite V40() V43(1) set
{{KL1,p1},{KL1}} is non empty finite V40() set
(Col (p2,p1)) . KL1 is set
p2 * (KL1,p1) is Element of the carrier of K
(K,V1,b1,(V2 . (f /. KL1))) 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
(K,V1,b1,(V2 . (f /. KL1))) /. p1 is Element of the carrier of K
i . KL1 is set
(K,V1,b4,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 .: (b4,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
<:b4,b1:> is Relation-like Function-like set
<:b4,b1:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set
Sum (K,V1,b4,b1) is Element of the carrier of V1
(K,V1,b1,(Sum (K,V1,b4,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
(K,V1,b1,(Sum (K,V1,b4,b1))) /. p1 is Element of the carrier of K
b4 /. p1 is Element of the carrier of K
mlt (b2,(Col (p2,p1))) 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
the multF of K .: (b2,(Col (p2,p1))) 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
<:b2,(Col (p2,p1)):> is Relation-like Function-like set
<:b2,(Col (p2,p1)):> (#) the multF of K is Relation-like the carrier of K -valued Function-like set
Sum (mlt (b2,(Col (p2,p1)))) 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
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 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 non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
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
dom f is finite set
b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
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:]
b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom b2 is finite set
Seg (len f) is finite V43( len f) Element of bool NAT
rng b2 is finite set
f /. 1 is Element of the carrier of a
V2 . (f /. 1) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. 1))) 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 (K,V1,b1,(V2 . (f /. 1))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j is set
p2 is set
b2 . p2 is set
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b2 . b4 is set
f /. b4 is Element of the carrier of a
V2 . (f /. b4) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. b4))) 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
p1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len p1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,V1,b1,(V2 . (f /. b4))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
j is set
i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like tabular finite-support set
rng i is finite set
dom i is finite set
p2 is set
i . p2 is set
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
i . b4 is set
f /. b4 is Element of the carrier of a
V2 . (f /. b4) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. b4))) 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
p1 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
j is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
p2 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
len p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
p2 /. b4 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 *
f /. b4 is Element of the carrier of a
V2 . (f /. b4) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. b4))) 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 p2 is finite set
p2 . b4 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
p2 /. b4 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 *
f /. b4 is Element of the carrier of a
V2 . (f /. b4) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. b4))) 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
b2 is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding 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
i is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding 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
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b2 . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
i . j is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom i is finite set
dom b2 is finite set
b2 /. j 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 *
f /. j is Element of the carrier of a
V2 . (f /. j) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. 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
i /. j 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 *
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
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 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 (K,a)
dom f is finite set
b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
(K,a,V1,V2,f,b1) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
dom (K,a,V1,V2,f,b1) is finite set
len (K,a,V1,V2,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len f 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 (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 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 (K,a)
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 (K,V1)
(K,a,V1,V2,f,b1) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
len (K,a,V1,V2,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
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 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 (K,a)
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 (K,V1)
(K,a,V1,V2,f,b1) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
width (K,a,V1,V2,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,V1,V2,f,b1) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
rng (K,a,V1,V2,f,b1) is finite set
b2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,a,V1,V2,f,b1) is finite set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
(K,a,V1,V2,f,b1) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
dom f is finite set
(K,a,V1,V2,f,b1) /. i 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 *
f /. i is Element of the carrier of a
V2 . (f /. i) is Element of the carrier of V1
(K,V1,b1,(V2 . (f /. 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
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
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 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 NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,a)
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b2 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
(K,a,V1,V2,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(K,a,V1,f,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
rng b1 is finite set
dom f is non empty set
dom V2 is non empty set
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
dom (V2 * b1) is finite set
dom b1 is finite set
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
dom (f * b1) is finite set
i is set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b1 /. j is Element of the carrier of a
V2 . (b1 /. j) is Element of the carrier of V1
(K,V1,b2,(V2 . (b1 /. 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
(K,a,V1,f,b1,b2) /. j 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 *
f . (b1 /. j) is Element of the carrier of V1
(K,V1,b2,(f . (b1 /. 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
(V2 * b1) . i is set
b1 . i is set
V2 . (b1 . i) is set
b1 /. i is Element of the carrier of a
V2 . (b1 /. i) is Element of the carrier of V1
f . (b1 /. i) is Element of the carrier of V1
f . (b1 . i) is set
(f * b1) . i 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
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 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 non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K) VectSpStr over K
the carrier of V2 is non empty set
[: the carrier of V1, the carrier of V2:] is Relation-like non empty set
bool [: the carrier of V1, the carrier of V2:] is non empty set
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 V1 -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of V1, the carrier of V2:]
b1 * f is Relation-like the carrier of a -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of a, the carrier of V2:]
[: the carrier of a, the carrier of V2:] is Relation-like non empty set
bool [: the carrier of a, the carrier of V2:] is non empty set
b2 is Relation-like NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,a)
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
i is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
len i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
(K,a,V1,f,b2,i) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
j is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V2)
(K,a,V2,(b1 * f),b2,j) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
(K,V1,V2,b1,i,j) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
(K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
width (K,a,V1,f,b2,i) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,V1,V2,b1,i,j) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (K,a,V2,(b1 * f),b2,j) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (K,V1,V2,b1,i,j) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width ((K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,V2,(b1 * f),b2,j) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,V1,f,b2,i) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len ((K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,a,V2,(b1 * f),b2,j) is finite set
dom ((K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j)) is finite set
Indices (K,a,V2,(b1 * f),b2,j) is set
p2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
b4 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
[p2,b4] is set
{p2,b4} is non empty finite V40() set
{p2} is non empty trivial finite V40() V43(1) set
{{p2,b4},{p2}} is non empty finite V40() set
(K,a,V2,(b1 * f),b2,j) * (p2,b4) is Element of the carrier of K
((K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j)) * (p2,b4) is Element of the carrier of K
p1 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 p1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom p1 is finite set
Seg (width (K,a,V2,(b1 * f),b2,j)) is finite V43( width (K,a,V2,(b1 * f),b2,j)) Element of bool NAT
[:(dom (K,a,V2,(b1 * f),b2,j)),(Seg (width (K,a,V2,(b1 * f),b2,j))):] is Relation-like finite set
Col ((K,V1,V2,b1,i,j),b4) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (len (K,V1,V2,b1,i,j)) -tuples_on the carrier of K
(len (K,V1,V2,b1,i,j)) -tuples_on the carrier of K is FinSequenceSet of the carrier of K
len (Col ((K,V1,V2,b1,i,j),b4)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len i) is finite V43( len i) Element of bool NAT
Indices ((K,a,V1,f,b2,i) * (K,V1,V2,b1,i,j)) is set
Seg (len j) is finite V43( len j) Element of bool NAT
dom j is finite set
KL1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
dom i is finite set
dom (K,V1,V2,b1,i,j) is finite set
Seg (width (K,V1,V2,b1,i,j)) is finite V43( width (K,V1,V2,b1,i,j)) Element of bool NAT
[KL1,b4] is set
{KL1,b4} is non empty finite V40() set
{KL1} is non empty trivial finite V40() V43(1) set
{{KL1,b4},{KL1}} is non empty finite V40() set
[:(dom (K,V1,V2,b1,i,j)),(Seg (width (K,V1,V2,b1,i,j))):] is Relation-like finite set
Indices (K,V1,V2,b1,i,j) is set
(K,V1,V2,b1,i,j) . KL1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(K,V1,V2,b1,i,j) * (KL1,b4) is Element of the carrier of K
KL2 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
KL2 . b4 is set
(K,V1,V2,b1,i,j) /. KL1 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 *
i /. KL1 is Element of the carrier of V1
b1 . (i /. KL1) is Element of the carrier of V2
(K,V2,j,(b1 . (i /. KL1))) 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 KL2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len KL2) is finite V43( len KL2) Element of bool NAT
dom KL2 is finite set
(Col ((K,V1,V2,b1,i,j),b4)) . KL1 is set
(K,V2,j,(b1 . (i /. KL1))) /. b4 is Element of the carrier of K
p1 . KL1 is set
b2 /. p2 is Element of the carrier of a
dom f is non empty set
(K,a,V2,(b1 * f),b2,j) . p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
KL1 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
KL1 . b4 is set
f . (b2 /. p2) is Element of the carrier of V1
(K,V1,i,(f . (b2 /. p2))) 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 (K,V1,i,(f . (b2 /. p2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom b2 is finite set
(K,a,V2,(b1 * f),b2,j) /. p2 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 *
(b1 * f) . (b2 /. p2) is Element of the carrier of V2
(K,V2,j,((b1 * f) . (b2 /. p2))) 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 (K,a,V1,f,b2,i) is finite set
Line ((K,a,V1,f,b2,i),p2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like finite-support Element of (width (K,a,V1,f,b2,i)) -tuples_on the carrier of K
(width (K,a,V1,f,b2,i)) -tuples_on the carrier of K is FinSequenceSet of the carrier of K
(K,a,V1,f,b2,i) . p2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
(K,a,V1,f,b2,i) /. p2 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 *
len (K,V2,j,((b1 * f) . (b2 /. p2))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len (K,V2,j,((b1 * f) . (b2 /. p2)))) is finite V43( len (K,V2,j,((b1 * f) . (b2 /. p2)))) Element of bool NAT
dom KL1 is finite set
(K,V2,j,((b1 * f) . (b2 /. p2))) /. b4 is Element of the carrier of K
b1 . (f . (b2 /. p2)) is Element of the carrier of V2
(K,V2,j,(b1 . (f . (b2 /. p2)))) 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
(K,V2,j,(b1 . (f . (b2 /. p2)))) /. b4 is Element of the carrier of K
(K,V1,(K,V1,i,(f . (b2 /. p2))),i) 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 .: ((K,V1,i,(f . (b2 /. p2))),i) 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
<:(K,V1,i,(f . (b2 /. p2))),i:> is Relation-like Function-like set
<:(K,V1,i,(f . (b2 /. p2))),i:> (#) the lmult of V1 is Relation-like the carrier of V1 -valued Function-like set
Sum (K,V1,(K,V1,i,(f . (b2 /. p2))),i) is Element of the carrier of V1
b1 . (Sum (K,V1,(K,V1,i,(f . (b2 /. p2))),i)) is Element of the carrier of V2
(K,V2,j,(b1 . (Sum (K,V1,(K,V1,i,(f . (b2 /. p2))),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
(K,V2,j,(b1 . (Sum (K,V1,(K,V1,i,(f . (b2 /. p2))),i)))) /. b4 is Element of the carrier of K
b1 * i is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
(K,V2,(K,V1,i,(f . (b2 /. p2))),(b1 * i)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
the lmult of V2 is Relation-like [: the carrier of K, the carrier of V2:] -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of V2:], the carrier of V2:]
[: the carrier of K, the carrier of V2:] is Relation-like non empty set
[:[: the carrier of K, the carrier of V2:], the carrier of V2:] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of V2:], the carrier of V2:] is non empty set
the lmult of V2 .: ((K,V1,i,(f . (b2 /. p2))),(b1 * i)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support FinSequence of the carrier of V2
<:(K,V1,i,(f . (b2 /. p2))),(b1 * i):> is Relation-like Function-like set
<:(K,V1,i,(f . (b2 /. p2))),(b1 * i):> (#) the lmult of V2 is Relation-like the carrier of V2 -valued Function-like set
Sum (K,V2,(K,V1,i,(f . (b2 /. p2))),(b1 * i)) is Element of the carrier of V2
(K,V2,j,(Sum (K,V2,(K,V1,i,(f . (b2 /. p2))),(b1 * 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
(K,V2,j,(Sum (K,V2,(K,V1,i,(f . (b2 /. p2))),(b1 * i)))) /. b4 is Element of the carrier of K
mlt ((K,V1,i,(f . (b2 /. p2))),p1) 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
the multF 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 multF of K .: ((K,V1,i,(f . (b2 /. p2))),p1) 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
<:(K,V1,i,(f . (b2 /. p2))),p1:> is Relation-like Function-like set
<:(K,V1,i,(f . (b2 /. p2))),p1:> (#) the multF of K is Relation-like the carrier of K -valued Function-like set
Sum (mlt ((K,V1,i,(f . (b2 /. p2))),p1)) is Element of the carrier of K
(Line ((K,a,V1,f,b2,i),p2)) "*" (Col ((K,V1,V2,b1,i,j),b4)) is Element of the carrier of K
mlt ((Line ((K,a,V1,f,b2,i),p2)),(Col ((K,V1,V2,b1,i,j),b4))) 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
the multF of K .: ((Line ((K,a,V1,f,b2,i),p2)),(Col ((K,V1,V2,b1,i,j),b4))) 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
<:(Line ((K,a,V1,f,b2,i),p2)),(Col ((K,V1,V2,b1,i,j),b4)):> is Relation-like Function-like set
<:(Line ((K,a,V1,f,b2,i),p2)),(Col ((K,V1,V2,b1,i,j),b4)):> (#) the multF of K is Relation-like the carrier of K -valued Function-like set
Sum (mlt ((Line ((K,a,V1,f,b2,i),p2)),(Col ((K,V1,V2,b1,i,j),b4)))) 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
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 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:]
(K,a,V1,V2,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 NAT -defined the carrier of a -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,a)
b2 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
(K,a,V1,(K,a,V1,V2,f),b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K is non empty non trivial set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(K,a,V1,V2,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
(K,a,V1,f,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
(K,a,V1,V2,b1,b2) + (K,a,V1,f,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
len (K,a,V1,(K,a,V1,V2,f),b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,V1,V2,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,a,V1,(K,a,V1,V2,f),b1,b2) is finite set
dom (K,a,V1,V2,b1,b2) is finite set
width (K,a,V1,V2,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (K,a,V1,f,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (K,a,V1,(K,a,V1,V2,f),b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width ((K,a,V1,V2,b1,b2) + (K,a,V1,f,b1,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,a,V1,f,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,a,V1,f,b1,b2) is finite set
Indices (K,a,V1,(K,a,V1,V2,f),b1,b2) is set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
[i,j] is set
{i,j} is non empty finite V40() set
{i} is non empty trivial finite V40() V43(1) set
{{i,j},{i}} is non empty finite V40() set
(K,a,V1,(K,a,V1,V2,f),b1,b2) * (i,j) is Element of the carrier of K
((K,a,V1,V2,b1,b2) + (K,a,V1,f,b1,b2)) * (i,j) is Element of the carrier of K
Seg (width (K,a,V1,(K,a,V1,V2,f),b1,b2)) is finite V43( width (K,a,V1,(K,a,V1,V2,f),b1,b2)) Element of bool NAT
[:(dom (K,a,V1,(K,a,V1,V2,f),b1,b2)),(Seg (width (K,a,V1,(K,a,V1,V2,f),b1,b2))):] is Relation-like finite set
Indices (K,a,V1,V2,b1,b2) is set
Indices (K,a,V1,f,b1,b2) is set
(K,a,V1,V2,b1,b2) * (i,j) is Element of the carrier of K
(K,a,V1,f,b1,b2) * (i,j) is Element of the carrier of K
((K,a,V1,V2,b1,b2) * (i,j)) + ((K,a,V1,f,b1,b2) * (i,j)) 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 . (((K,a,V1,V2,b1,b2) * (i,j)),((K,a,V1,f,b1,b2) * (i,j))) is Element of the carrier of K
b1 /. i is Element of the carrier of a
f . (b1 /. i) is Element of the carrier of V1
rng b2 is finite set
(K,V1,b2,(f . (b1 /. 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 (K,V1,b2,(f . (b1 /. i))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
p2 is Relation-like the carrier of V1 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V1
Sum p2 is Element of the carrier of V1
Carrier p2 is finite Element of bool the carrier of V1
bool the carrier of V1 is non empty set
V2 . (b1 /. i) is Element of the carrier of V1
(K,V1,b2,(V2 . (b1 /. 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 (K,V1,b2,(V2 . (b1 /. i))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
b4 is Relation-like the carrier of V1 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V1
Sum b4 is Element of the carrier of V1
Carrier b4 is finite Element of bool the carrier of V1
dom b1 is finite set
(K,a,V1,(K,a,V1,V2,f),b1,b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
KL1 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
KL1 . j is set
(K,a,V1,V2,f) . (b1 /. i) is Element of the carrier of V1
(K,V1,b2,((K,a,V1,V2,f) . (b1 /. 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 (K,V1,b2,((K,a,V1,V2,f) . (b1 /. i))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL2 is Relation-like the carrier of V1 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V1
Sum KL2 is Element of the carrier of V1
Carrier KL2 is finite Element of bool the carrier of V1
p1 is Basis of V1
(V2 . (b1 /. i)) + (f . (b1 /. 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 . (b1 /. i)),(f . (b1 /. i))) is Element of the carrier of V1
b2 /. j is Element of the carrier of V1
KL2 . (b2 /. j) is Element of the carrier of K
b4 + p2 is Relation-like the carrier of V1 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V1
(b4 + p2) . (b2 /. j) is Element of the carrier of K
b4 . (b2 /. j) is Element of the carrier of K
p2 . (b2 /. j) is Element of the carrier of K
(b4 . (b2 /. j)) + (p2 . (b2 /. j)) is Element of the carrier of K
the addF of K . ((b4 . (b2 /. j)),(p2 . (b2 /. j))) is Element of the carrier of K
(K,a,V1,(K,a,V1,V2,f),b1,b2) /. i 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 *
(K,a,V1,f,b1,b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p3 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
p3 . j is set
(K,a,V1,V2,b1,b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 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
p2 . j is set
Seg (len b1) is finite V43( len b1) Element of bool NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len b2) is finite V43( len b2) Element of bool NAT
KL1 /. j is Element of the carrier of K
dom b2 is finite set
(K,a,V1,f,b1,b2) /. i 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 *
dom p3 is finite set
p3 /. j is Element of the carrier of K
(K,a,V1,V2,b1,b2) /. i 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 *
dom p2 is finite set
p2 /. j is Element of the carrier of K
dom KL1 is finite set
len ((K,a,V1,V2,b1,b2) + (K,a,V1,f,b1,b2)) 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
0. K is V56(K) Element of the carrier of K
a is Element of the carrier of K
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
V2 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 V2 is non empty set
[: the carrier of V1, the carrier of V2:] is Relation-like non empty set
bool [: the carrier of V1, the carrier of V2:] is non empty set
f is Relation-like the carrier of V1 -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of V1, the carrier of V2:]
(K,V1,V2,f,a) is Relation-like the carrier of V1 -defined the carrier of V2 -valued Function-like non empty total quasi_total Element of bool [: the carrier of V1, the carrier of V2:]
b1 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V1)
b2 is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like finite-support (K,V2)
(K,V1,V2,(K,V1,V2,f,a),b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(K,V1,V2,f,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
a * (K,V1,V2,f,b1,b2) is Relation-like NAT -defined the carrier of K * -valued Function-like finite FinSequence-like FinSubsequence-like V144() tabular FinSequence-yielding finite-support FinSequence of the carrier of K *
width (K,V1,V2,(K,V1,V2,f,a),b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (K,V1,V2,f,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
width (a * (K,V1,V2,f,b1,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,V1,V2,(K,V1,V2,f,a),b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len b1 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
len (K,V1,V2,f,b1,b2) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
dom (K,V1,V2,(K,V1,V2,f,a),b1,b2) is finite set
dom (K,V1,V2,f,b1,b2) is finite set
Indices (K,V1,V2,(K,V1,V2,f,a),b1,b2) is set
i is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
j is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() set
[i,j] is set
{i,j} is non empty finite V40() set
{i} is non empty trivial finite V40() V43(1) set
{{i,j},{i}} is non empty finite V40() set
(K,V1,V2,(K,V1,V2,f,a),b1,b2) * (i,j) is Element of the carrier of K
(a * (K,V1,V2,f,b1,b2)) * (i,j) is Element of the carrier of K
Seg (width (K,V1,V2,(K,V1,V2,f,a),b1,b2)) is finite V43( width (K,V1,V2,(K,V1,V2,f,a),b1,b2)) Element of bool NAT
[:(dom (K,V1,V2,(K,V1,V2,f,a),b1,b2)),(Seg (width (K,V1,V2,(K,V1,V2,f,a),b1,b2))):] is Relation-like finite set
Indices (K,V1,V2,f,b1,b2) is set
(K,V1,V2,f,b1,b2) * (i,j) is Element of the carrier of K
a * ((K,V1,V2,f,b1,b2) * (i,j)) is Element of the carrier of K
the multF of K is Relation-like [: the carrier of K, the carrier of K:] -defined the carrier of K -valued Function-like 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 multF of K . (a,((K,V1,V2,f,b1,b2) * (i,j))) is Element of the carrier of K
(K,V1,V2,f,b1,b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p2 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
p2 . j is set
dom b1 is finite set
(K,V1,V2,f,b1,b2) /. i 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 *
b1 /. i is Element of the carrier of V1
f . (b1 /. i) is Element of the carrier of V2
(K,V2,b2,(f . (b1 /. 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
rng b2 is finite set
(K,V1,V2,(K,V1,V2,f,a),b1,b2) . i is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like finite-support set
p1 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
p1 . j is set
(K,V1,V2,f,a) . (b1 /. i) is Element of the carrier of V2
(K,V2,b2,((K,V1,V2,f,a) . (b1 /. 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 (K,V2,b2,((K,V1,V2,f,a) . (b1 /. i))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL1 is Relation-like the carrier of V2 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V2
Sum KL1 is Element of the carrier of V2
Carrier KL1 is finite Element of bool the carrier of V2
bool the carrier of V2 is non empty set
len (K,V2,b2,(f . (b1 /. i))) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
KL2 is Relation-like the carrier of V2 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V2
Sum KL2 is Element of the carrier of V2
Carrier KL2 is finite Element of bool the carrier of V2
b4 is Basis of V2
a * (f . (b1 /. i)) is Element of the carrier of V2
b2 /. j is Element of the carrier of V2
KL1 . (b2 /. j) is Element of the carrier of K
a * KL2 is Relation-like the carrier of V2 -defined the carrier of K -valued Function-like total quasi_total Linear_Combination of V2
(a * KL2) . (b2 /. j) is Element of the carrier of K
KL2 . (b2 /. j) is Element of the carrier of K
a * (KL2 . (b2 /. j)) is Element of the carrier of K
the multF of K . (a,(KL2 . (b2 /. j))) is Element of the carrier of K
Seg (len b1) is finite V43( len b1) Element of bool NAT
len b2 is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT
Seg (len b2) is finite V43( len b2) Element of bool NAT
p2 /. j is Element of the carrier of K
dom b2 is finite set
dom (K,V2,b2,(f . (b1 /. i))) is finite set
(K,V1,V2,(K,V1,V2,f,a),b1,b2) /. i 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 *
dom p1 is finite set
p1 /. j is Element of the carrier of K
len (a * (K,V1,V2,f,b1,b2)) is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() Element of NAT