:: MATRLIN semantic presentation

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

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

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

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

a is V24() V25() V26() V30() V31() ext-real non negative V35() finite V41() 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

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
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

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

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

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

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

(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

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

len i 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

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

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

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

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

K . (len K) is set

V1 is 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

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

the carrier of K is non empty non trivial set

the carrier of a is non empty set
bool the carrier of a is non empty set

Carrier V1 is finite Element of bool the carrier of a
Sum V1 is Element of the carrier 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

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

the carrier of K is non empty non trivial set

the carrier of a is non empty set
bool the carrier of a is non empty set

Carrier V1 is finite Element of bool the carrier of a
Sum V1 is Element of the carrier of a

Carrier V2 is finite Element of bool the carrier of a
Sum V2 is Element of the carrier 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

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

the carrier of K is non empty non trivial set
0. K is V56(K) Element of the carrier of 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

Carrier V2 is finite Element of bool the carrier of a
Sum V2 is Element of the carrier 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

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

the carrier of K is non empty non trivial set

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

Sum f is Element of the carrier 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

the carrier of () is non empty set
bool the carrier of () is non empty set

the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
the ZeroF of () is Element of the carrier of ()
the lmult of () is Relation-like [: the carrier of K, the carrier of ():] -defined the carrier of () -valued Function-like non empty total quasi_total Element of bool [:[: the carrier of K, the carrier of ():], the carrier of ():]
the carrier of K is non empty non trivial set
[: the carrier of K, the carrier of ():] is Relation-like non empty set
[:[: the carrier of K, the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of K, the carrier of ():], the carrier of ():] is non empty set
VectSpStr(# the carrier of (), the addF of (), the ZeroF of (), the lmult of () #) is non empty strict 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

rng V2 is finite set

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

the carrier of K is non empty non trivial set

the carrier of a is non empty set
V1 is Element 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

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

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

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

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

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

len p2 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
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

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

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 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 functional non empty FinSequence-membered FinSequenceSet of the carrier of K
0. K is V56(K) Element of the carrier of K

the carrier of K is non empty non trivial set

the carrier of a is non empty set
V1 is Element 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 K
(Sum V2) * V1 is Element 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

the carrier of K is non empty set
0. K is V56(K) Element of the carrier of K

dom a is finite set
Sum a is Element 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

the carrier of K * is functional non empty FinSequence-membered FinSequenceSet 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 functional non empty FinSequence-membered FinSequenceSet of the carrier of K

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

the carrier of K is non empty non trivial set

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,V2:> (#) the lmult of a is Relation-like the carrier of a -valued Function-like set

the carrier of K is non empty non trivial set

the carrier of a is non empty set

dom V1 is finite set

dom V2 is finite 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

<: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
the carrier of K is non empty set
the carrier of K * is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

len a 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 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

Sum (a /. 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
dom V1 is finite set

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

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

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

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

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

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

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

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

rng V2 is finite set

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

Sum (V2 /. f) is Element of the carrier of V1
K is non empty set
a is Element of K

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

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

the carrier of a is non empty set

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:]

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

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

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

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

the carrier of a * is functional non empty FinSequence-membered FinSequenceSet 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

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

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 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 functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
Sum (<*> the carrier of V1) is Element 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

the carrier of K is non empty non trivial set

the carrier of a is non empty set

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:]

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
(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:> (#) 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

(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

the carrier of K is non empty non trivial set

the carrier of a is non empty set

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:]

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
(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:> (#) 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

the carrier of K is non empty non trivial set

the carrier of a is non empty set