:: MATRLIN2 semantic presentation

REAL is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal Element of bool REAL

the carrier of K583() is set
NAT is non empty non trivial V21() V22() V23() non finite cardinal limit_cardinal set
bool NAT is non trivial non finite set
bool NAT is non trivial non finite set

RAT is set
INT is set

2 is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT
1 is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

K521(0,1,2) is finite set
[:K521(0,1,2),K521(0,1,2):] is Relation-like finite set
[:[:K521(0,1,2),K521(0,1,2):],K521(0,1,2):] is Relation-like finite set
bool [:[:K521(0,1,2),K521(0,1,2):],K521(0,1,2):] is finite V32() set
bool [:K521(0,1,2),K521(0,1,2):] is finite V32() set

{{},1} is non empty finite V32() set
K670() is set
bool K670() is set
K671() is Element of bool K670()
3 is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

Seg 1 is non empty trivial finite 1 -element V136() Element of bool NAT
{ b1 where b1 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty trivial finite V32() 1 -element set
Seg 2 is non empty finite 2 -element V136() Element of bool NAT
{ b1 where b1 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty finite V32() set

the carrier of A is non empty set
the carrier of (V2 /\ V3) is non empty set
AI is set
AI is set
the carrier of (V2 + V3) is non empty set

the carrier of AI is non empty set
S is set
the carrier of V1 is non empty set
KER is Element of the carrier of V1
MAI is Element of the carrier of V1
KER + MAI is Element of the carrier of V1
MK is Element of the carrier of AI
x is Element of the carrier of AI
MK + x is Element of the carrier of AI
S is set
the carrier of f is non empty set
KER is Element of the carrier of f
MAI is Element of the carrier of f
KER + MAI is Element of the carrier of f
the carrier of V1 is non empty set
MK is Element of the carrier of V1
x is Element of the carrier of V1
MK + x is Element of the carrier of V1

the carrier of V2 is non empty set
bool the carrier of V2 is set
the carrier of V3 is non empty set
bool the carrier of V3 is set

the carrier of (V2 + V3) is non empty set
bool the carrier of (V2 + V3) is set
A is linearly-independent Element of bool the carrier of V2
A is linearly-independent Element of bool the carrier of V3
A \/ A is set
AI is Element of bool the carrier of (V2 + V3)
the carrier of K is non empty non trivial set

Sum MAI is Element of the carrier of (V2 + V3)
0. (V2 + V3) is V47(V2 + V3) Element of the carrier of (V2 + V3)
the ZeroF of (V2 + V3) is Element of the carrier of (V2 + V3)
Carrier MAI is finite Element of bool the carrier of (V2 + V3)
0. K is V47(K) Element of the carrier of K
the ZeroF of K is Element of the carrier of K
{ b1 where b1 is Element of the carrier of (V2 + V3) : not MAI . b1 = 0. K } is set
(0. (V2 + V3)) + (0. (V2 + V3)) is Element of the carrier of (V2 + V3)
(Carrier MAI) /\ A is finite Element of bool the carrier of V2
(Carrier MAI) \ A is finite Element of bool the carrier of (V2 + V3)
w is finite Element of bool the carrier of (V2 + V3)
KER is Element of bool the carrier of (V2 + V3)
W is set
S is Element of bool the carrier of (V2 + V3)

S is Element of bool the carrier of (V2 + V3)
0. V2 is V47(V2) Element of the carrier of V2
the ZeroF of V2 is Element of the carrier of V2
0. V3 is V47(V3) Element of the carrier of V3
the ZeroF of V3 is Element of the carrier of V3
W is set
LLw is Element of the carrier of (V2 + V3)
MAI . LLw is Element of the carrier of K
MAI . W is set
[: the carrier of (V2 + V3), the carrier of K:] is Relation-like set
bool [: the carrier of (V2 + V3), the carrier of K:] is set
W is Relation-like Function-like non empty total quasi_total Element of bool [: the carrier of (V2 + V3), the carrier of K:]
LLw is set
i is Element of the carrier of (V2 + V3)
MAI . i is Element of the carrier of K
MAI . LLw is set
LLw is Relation-like Function-like non empty total quasi_total Element of bool [: the carrier of (V2 + V3), the carrier of K:]
Funcs ( the carrier of (V2 + V3), the carrier of K) is functional non empty FUNCTION_DOMAIN of the carrier of (V2 + V3), the carrier of K
i is Relation-like Function-like total quasi_total Element of Funcs ( the carrier of (V2 + V3), the carrier of K)
A12 is Element of the carrier of (V2 + V3)
i . A12 is Element of the carrier of K

Carrier A12 is finite Element of bool the carrier of (V2 + V3)
{ b1 where b1 is Element of the carrier of (V2 + V3) : not A12 . b1 = 0. K } is set
i is set
fb is Element of the carrier of (V2 + V3)
A12 . fb is Element of the carrier of K
x is finite Element of bool the carrier of (V2 + V3)
fb is Relation-like Function-like total quasi_total Element of Funcs ( the carrier of (V2 + V3), the carrier of K)
fbi is Element of the carrier of (V2 + V3)
fb . fbi is Element of the carrier of K

Carrier fbi is finite Element of bool the carrier of (V2 + V3)
{ b1 where b1 is Element of the carrier of (V2 + V3) : not fbi . b1 = 0. K } is set
b2n is set
v is Element of the carrier of (V2 + V3)
fbi . v is Element of the carrier of K
the carrier of f is non empty set

Carrier b2n is finite Element of bool the carrier of (V2 + V3)
{ b1 where b1 is Element of the carrier of (V2 + V3) : not b2n . b1 = 0. K } is set
Sum b2n is Element of the carrier of (V2 + V3)

Carrier v is finite Element of bool the carrier of f
bool the carrier of f is set
{ b1 where b1 is Element of the carrier of f : not v . b1 = 0. K } is set
Sum v is Element of the carrier of f

v is Element of the carrier of (V2 + V3)
MAI . v is Element of the carrier of K
(b2n + i) . v is Element of the carrier of K
b2n . v is Element of the carrier of K
i . v is Element of the carrier of K
(b2n . v) + (i . v) is Element of the carrier of K
(MAI . v) + (i . v) is Element of the carrier of K
(MAI . v) + (0. K) is Element of the carrier of K
b2n . v is Element of the carrier of K
i . v is Element of the carrier of K
(b2n . v) + (i . v) is Element of the carrier of K
(i . v) + (0. K) is Element of the carrier of K
b2n . v is Element of the carrier of K
i . v is Element of the carrier of K
(b2n . v) + (i . v) is Element of the carrier of K
(0. K) + (i . v) is Element of the carrier of K
(0. K) + (0. K) is Element of the carrier of K
Sum i is Element of the carrier of (V2 + V3)
(Sum b2n) + (Sum i) is Element of the carrier of (V2 + V3)
Carrier i is finite Element of bool the carrier of (V2 + V3)
{ b1 where b1 is Element of the carrier of (V2 + V3) : not i . b1 = 0. K } is set
the carrier of g is non empty set

Carrier v is finite Element of bool the carrier of g
bool the carrier of g is set
{ b1 where b1 is Element of the carrier of g : not v . b1 = 0. K } is set
Sum v is Element of the carrier of g
0. f is V47(f) Element of the carrier of f
the ZeroF of f is Element of the carrier of f
0. g is V47(g) Element of the carrier of g
the ZeroF of g is Element of the carrier of g

f is Basis of V2
g is Basis of V3
f \/ g is set
the carrier of V3 is non empty set
the carrier of (V2 + V3) is non empty set
the carrier of V2 is non empty set
bool the carrier of (V2 + V3) is set

the addF of V3 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V3, the carrier of V3:], the carrier of V3:]
[: the carrier of V3, the carrier of V3:] is Relation-like set
[:[: the carrier of V3, the carrier of V3:], the carrier of V3:] is Relation-like set
bool [:[: the carrier of V3, the carrier of V3:], the carrier of V3:] is set
the ZeroF of V3 is Element of the carrier of V3
the lmult of V3 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of K, the carrier of V3:], the carrier of V3:]
the carrier of K is non empty non trivial set
[: the carrier of K, the carrier of V3:] is Relation-like set
[:[: the carrier of K, the carrier of V3:], the carrier of V3:] is Relation-like set
bool [:[: the carrier of K, the carrier of V3:], the carrier of V3:] is set
VectSpStr(# the carrier of V3, the addF of V3, the ZeroF of V3, the lmult of V3 #) is non empty strict VectSpStr over K

AI is Element of bool the carrier of (V2 + V3)

A is Element of bool the carrier of (V2 + V3)

A is Element of bool the carrier of (V2 + V3)

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

the carrier of (Lin A) is non empty set
S is set
KER is Element of the carrier of (V2 + V3)
the carrier of V1 is non empty set
MAI is Element of the carrier of V1
MK is Element of the carrier of V1
MAI + MK is Element of the carrier of V1
x is Element of the carrier of (V2 + V3)
v is Element of the carrier of (V2 + V3)
x + v is Element of the carrier of (V2 + V3)
the carrier of (Lin AI) is non empty set
the carrier of (Lin A) is non empty set
the addF of (V2 + V3) is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of (V2 + V3), the carrier of (V2 + V3):], the carrier of (V2 + V3):]
[: the carrier of (V2 + V3), the carrier of (V2 + V3):] is Relation-like set
[:[: the carrier of (V2 + V3), the carrier of (V2 + V3):], the carrier of (V2 + V3):] is Relation-like set
bool [:[: the carrier of (V2 + V3), the carrier of (V2 + V3):], the carrier of (V2 + V3):] is set
the ZeroF of (V2 + V3) is Element of the carrier of (V2 + V3)
the lmult of (V2 + V3) is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of K, the carrier of (V2 + V3):], the carrier of (V2 + V3):]
[: the carrier of K, the carrier of (V2 + V3):] is Relation-like set
[:[: the carrier of K, the carrier of (V2 + V3):], the carrier of (V2 + V3):] is Relation-like set
bool [:[: the carrier of K, the carrier of (V2 + V3):], the carrier of (V2 + V3):] is set
VectSpStr(# the carrier of (V2 + V3), the addF of (V2 + V3), the ZeroF of (V2 + V3), the lmult of (V2 + V3) #) is non empty strict VectSpStr over K

the carrier of V1 is non empty set
the addF of V1 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is Relation-like set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
the ZeroF of V1 is Element of the carrier of V1
the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is 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
the carrier of ((Omega). V1) is non empty set

rng V2 is finite set
V3 is Basis of (Omega). V1
bool the carrier of V1 is set
f is linearly-independent Element of bool the carrier of V1

the carrier of V1 is non empty set
bool the carrier of V1 is set
V2 is finite Element of bool the carrier of V1

dim (Lin V2) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
card V2 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
the carrier of (Lin V2) is non empty set
f is set
bool the carrier of (Lin V2) is set
f is Element of bool the carrier of (Lin V2)

g is Element of bool the carrier of (Lin V2)

A is finite Element of bool the carrier of (Lin V2)

dim A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
card A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

the carrier of V1 is non empty set
bool the carrier of V1 is set
V2 is finite Element of bool the carrier of V1

dim (Lin V2) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
card V2 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
the carrier of (Lin V2) is non empty set
f is set
bool the carrier of (Lin V2) is set
f is Element of bool the carrier of (Lin V2)

g is Element of bool the carrier of (Lin V2)

A is finite Element of bool the carrier of (Lin V2)
card A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

dim A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set

dom V2 is finite Element of bool NAT

the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (V3,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
dom (lmlt (V3,V2)) is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom V3) /\ (dom V2) is finite Element of bool NAT
rng V3 is finite set
rng V2 is finite set
[:(rng V3),(rng V2):] is Relation-like finite set
dom the lmult of V1 is set

the carrier of K is non empty non trivial set

dom V1 is finite Element of bool NAT

the addF of K is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the addF of K .: (V1,V2) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
dom (V1 + V2) is finite Element of bool NAT
dom V2 is finite Element of bool NAT
(dom V1) /\ (dom V2) is finite Element of bool NAT
rng V1 is finite set
rng V2 is finite set
[:(rng V1),(rng V2):] is Relation-like finite set
dom the addF of K is set

the carrier of V1 is non empty set

dom V2 is finite Element of bool NAT

the addF of V1 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is Relation-like set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
the addF of V1 .: (V2,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
dom (V2 + V3) is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom V2) /\ (dom V3) is finite Element of bool NAT
rng V2 is finite set
rng V3 is finite set
[:(rng V2),(rng V3):] is Relation-like finite set
dom the addF of V1 is set

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set

the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (V3,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

the addF of K is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of K:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
the addF of K .: (V3,f) is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of K
lmlt ((V3 + f),V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the lmult of V1 .: ((V3 + f),V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

the lmult of V1 .: (f,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(lmlt (V3,V2)) + (lmlt (f,V2)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the addF of V1 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is Relation-like set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
the addF of V1 .: ((lmlt (V3,V2)),(lmlt (f,V2))) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
dom ((lmlt (V3,V2)) + (lmlt (f,V2))) is finite Element of bool NAT
dom (lmlt (V3,V2)) is finite Element of bool NAT
dom (lmlt (f,V2)) is finite Element of bool NAT
(dom (lmlt (V3,V2))) /\ (dom (lmlt (f,V2))) is finite Element of bool NAT
dom (lmlt ((V3 + f),V2)) is finite Element of bool NAT
dom (V3 + f) is finite Element of bool NAT
dom V2 is finite Element of bool NAT
(dom (V3 + f)) /\ (dom V2) is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom V3) /\ (dom V2) is finite Element of bool NAT

(dom f) /\ (dom V2) is finite Element of bool NAT
((dom V3) /\ (dom V2)) /\ (dom f) is finite Element of bool NAT
(((dom V3) /\ (dom V2)) /\ (dom f)) /\ (dom V2) is finite Element of bool NAT
(dom V3) /\ (dom f) is finite Element of bool NAT
((dom V3) /\ (dom f)) /\ (dom V2) is finite Element of bool NAT
(((dom V3) /\ (dom f)) /\ (dom V2)) /\ (dom V2) is finite Element of bool NAT
(dom V2) /\ (dom V2) is finite Element of bool NAT
((dom V3) /\ (dom f)) /\ ((dom V2) /\ (dom V2)) is finite Element of bool NAT
AI is set
(lmlt (f,V2)) /. AI is Element of the carrier of V1
(lmlt (f,V2)) . AI is set
f /. AI is Element of the carrier of K
f . AI is set
(V3 + f) . AI is set
(V3 + f) /. AI is Element of the carrier of K
V3 /. AI is Element of the carrier of K
V3 . AI is set
V2 /. AI is Element of the carrier of V1
V2 . AI is set
(lmlt (V3,V2)) /. AI is Element of the carrier of V1
(lmlt (V3,V2)) . AI is set
((lmlt (V3,V2)) + (lmlt (f,V2))) . AI is set
((lmlt (V3,V2)) /. AI) + ((lmlt (f,V2)) /. AI) is Element of the carrier of V1
the lmult of V1 . ((V3 /. AI),(V2 /. AI)) is Element of the carrier of V1
( the lmult of V1 . ((V3 /. AI),(V2 /. AI))) + ((lmlt (f,V2)) /. AI) is Element of the carrier of V1
(V3 /. AI) * (V2 /. AI) is Element of the carrier of V1
(f /. AI) * (V2 /. AI) is Element of the carrier of V1
the lmult of V1 . ((f /. AI),(V2 /. AI)) is Element of the carrier of V1
((V3 /. AI) * (V2 /. AI)) + ((f /. AI) * (V2 /. AI)) is Element of the carrier of V1
(V3 /. AI) + (f /. AI) is Element of the carrier of K
((V3 /. AI) + (f /. AI)) * (V2 /. AI) is Element of the carrier of V1
the lmult of V1 . (((V3 /. AI) + (f /. AI)),(V2 /. AI)) is Element of the carrier of V1
((V3 + f) /. AI) * (V2 /. AI) is Element of the carrier of V1
the lmult of V1 . (((V3 + f) /. AI),(V2 /. AI)) is Element of the carrier of V1
(lmlt ((V3 + f),V2)) . AI is set

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set

the addF of V1 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is Relation-like set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
the addF of V1 .: (V2,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

lmlt (f,(V2 + V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (f,(V2 + V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

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

the lmult of V1 .: (f,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(lmlt (f,V2)) + (lmlt (f,V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the addF of V1 .: ((lmlt (f,V2)),(lmlt (f,V3))) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
dom ((lmlt (f,V2)) + (lmlt (f,V3))) is finite Element of bool NAT
dom (lmlt (f,V2)) is finite Element of bool NAT
dom (lmlt (f,V3)) is finite Element of bool NAT
(dom (lmlt (f,V2))) /\ (dom (lmlt (f,V3))) is finite Element of bool NAT
dom (lmlt (f,(V2 + V3))) is finite Element of bool NAT

dom (V2 + V3) is finite Element of bool NAT
(dom f) /\ (dom (V2 + V3)) is finite Element of bool NAT
dom V2 is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom V2) /\ (dom V3) is finite Element of bool NAT
(dom f) /\ (dom V2) is finite Element of bool NAT
(dom f) /\ (dom V3) is finite Element of bool NAT
((dom f) /\ (dom V2)) /\ (dom f) is finite Element of bool NAT
(((dom f) /\ (dom V2)) /\ (dom f)) /\ (dom V3) is finite Element of bool NAT
(dom f) /\ (dom f) is finite Element of bool NAT
((dom f) /\ (dom f)) /\ (dom V2) is finite Element of bool NAT
(((dom f) /\ (dom f)) /\ (dom V2)) /\ (dom V3) is finite Element of bool NAT
AI is set
(lmlt (f,V3)) /. AI is Element of the carrier of V1
(lmlt (f,V3)) . AI is set
V3 /. AI is Element of the carrier of V1
V3 . AI is set
(V2 + V3) . AI is set
(V2 + V3) /. AI is Element of the carrier of V1
f /. AI is Element of the carrier of K
f . AI is set
V2 /. AI is Element of the carrier of V1
V2 . AI is set
(lmlt (f,V2)) /. AI is Element of the carrier of V1
(lmlt (f,V2)) . AI is set
((lmlt (f,V2)) + (lmlt (f,V3))) . AI is set
((lmlt (f,V2)) /. AI) + ((lmlt (f,V3)) /. AI) is Element of the carrier of V1
the lmult of V1 . ((f /. AI),(V2 /. AI)) is Element of the carrier of V1
( the lmult of V1 . ((f /. AI),(V2 /. AI))) + ((lmlt (f,V3)) /. AI) is Element of the carrier of V1
(f /. AI) * (V2 /. AI) is Element of the carrier of V1
(f /. AI) * (V3 /. AI) is Element of the carrier of V1
the lmult of V1 . ((f /. AI),(V3 /. AI)) is Element of the carrier of V1
((f /. AI) * (V2 /. AI)) + ((f /. AI) * (V3 /. AI)) is Element of the carrier of V1
(V2 /. AI) + (V3 /. AI) is Element of the carrier of V1
(f /. AI) * ((V2 /. AI) + (V3 /. AI)) is Element of the carrier of V1
the lmult of V1 . ((f /. AI),((V2 /. AI) + (V3 /. AI))) is Element of the carrier of V1
(f /. AI) * ((V2 + V3) /. AI) is Element of the carrier of V1
the lmult of V1 . ((f /. AI),((V2 + V3) /. AI)) is Element of the carrier of V1
(lmlt (f,(V2 + V3))) . AI is set

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set

len V2 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

len V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

len f is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (f,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

len g is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

lmlt ((f ^ g),(V2 ^ V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the lmult of V1 .: ((f ^ g),(V2 ^ V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

the lmult of V1 .: (g,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(lmlt (f,V2)) ^ (lmlt (g,V3)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
(len g) -tuples_on the carrier of V1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
(len f) -tuples_on the carrier of V1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
(len f) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
(len g) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

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

the lmult of V1 .: (S,A) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
( the lmult of V1 .: (AI,A)) ^ ( the lmult of V1 .: (S,A)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

the carrier of V1 is non empty set

len V2 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
Sum V2 is Element of the carrier of V1

len V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

the addF of V1 is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:]
[: the carrier of V1, the carrier of V1:] is Relation-like set
[:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of V1, the carrier of V1:], the carrier of V1:] is set
the addF of V1 .: (V2,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Sum (V2 + V3) is Element of the carrier of V1
Sum V3 is Element of the carrier of V1
(Sum V2) + (Sum V3) is Element of the carrier of V1
(len V2) -tuples_on the carrier of V1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1

the addF of V1 .: (f,g) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Sum (f + g) is Element of the carrier of V1

the carrier of K is non empty non trivial set
V1 is Element of the carrier of K

the carrier of V2 is non empty set

len V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

(len V3) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
lmlt (((len V3) |-> V1),V3) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V2:], the carrier of V2:] is Relation-like set
bool [:[: the carrier of K, the carrier of V2:], the carrier of V2:] is set
the lmult of V2 .: (((len V3) |-> V1),V3) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum (lmlt (((len V3) |-> V1),V3)) is Element of the carrier of V2
Sum V3 is Element of the carrier of V2
V1 * (Sum V3) is Element of the carrier of V2
the lmult of V2 . (V1,(Sum V3)) is Element of the carrier of V2
f is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
f + 1 is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

len A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
Sum A is Element of the carrier of V2
A is Element of the carrier of K

(len A) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
lmlt (((len A) |-> A),A) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 .: (((len A) |-> A),A) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum (lmlt (((len A) |-> A),A)) is Element of the carrier of V2
A * (Sum A) is Element of the carrier of V2
the lmult of V2 . (A,(Sum A)) is Element of the carrier of V2

{ b1 where b1 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT : ( 1 <= b1 & b1 <= f ) } is set

len (A | f) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
dom (A | f) is finite Element of bool NAT

A /. (f + 1) is Element of the carrier of V2
A . (f + 1) is set

[1,A] is set
{1,A} is non empty finite set
{{1,A},{1}} is non empty finite V32() set

[1,(A /. (f + 1))] is set
{1,(A /. (f + 1))} is non empty finite set
{{1,(A /. (f + 1))},{1}} is non empty finite V32() set
{[1,(A /. (f + 1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
lmlt (<*A*>,<*(A /. (f + 1))*>) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 .: (<*A*>,<*(A /. (f + 1))*>) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
A * (A /. (f + 1)) is Element of the carrier of V2
the lmult of V2 . (A,(A /. (f + 1))) is Element of the carrier of V2
<*(A * (A /. (f + 1)))*> is Relation-like NAT -defined the carrier of V2 -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
[1,(A * (A /. (f + 1)))] is set
{1,(A * (A /. (f + 1)))} is non empty finite set
{{1,(A * (A /. (f + 1)))},{1}} is non empty finite V32() set
{[1,(A * (A /. (f + 1)))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
len <*A*> is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

[1,(A . (f + 1))] is set
{1,(A . (f + 1))} is non empty finite set
{{1,(A . (f + 1))},{1}} is non empty finite V32() set
{[1,(A . (f + 1))]} is Relation-like Function-like constant non empty trivial finite 1 -element set
len <*(A . (f + 1))*> is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

(f + 1) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K

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

len (f |-> A) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

lmlt ((f |-> A),(A | f)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 .: ((f |-> A),(A | f)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
(lmlt ((f |-> A),(A | f))) ^ (lmlt (<*A*>,<*(A /. (f + 1))*>)) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum ((lmlt ((f |-> A),(A | f))) ^ (lmlt (<*A*>,<*(A /. (f + 1))*>))) is Element of the carrier of V2
Sum (lmlt ((f |-> A),(A | f))) is Element of the carrier of V2
Sum (lmlt (<*A*>,<*(A /. (f + 1))*>)) is Element of the carrier of V2
(Sum (lmlt ((f |-> A),(A | f)))) + (Sum (lmlt (<*A*>,<*(A /. (f + 1))*>))) is Element of the carrier of V2
Sum (A | f) is Element of the carrier of V2
A * (Sum (A | f)) is Element of the carrier of V2
the lmult of V2 . (A,(Sum (A | f))) is Element of the carrier of V2
Sum <*(A * (A /. (f + 1)))*> is Element of the carrier of V2
(A * (Sum (A | f))) + (Sum <*(A * (A /. (f + 1)))*>) is Element of the carrier of V2
(A * (Sum (A | f))) + (A * (A /. (f + 1))) is Element of the carrier of V2
(Sum (A | f)) + (A /. (f + 1)) is Element of the carrier of V2
A * ((Sum (A | f)) + (A /. (f + 1))) is Element of the carrier of V2
the lmult of V2 . (A,((Sum (A | f)) + (A /. (f + 1)))) is Element of the carrier of V2

len f is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
Sum f is Element of the carrier of V2
g is Element of the carrier of K

(len f) -tuples_on the carrier of K is functional non empty FinSequence-membered FinSequenceSet of the carrier of K
lmlt (((len f) |-> g),f) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 .: (((len f) |-> g),f) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum (lmlt (((len f) |-> g),f)) is Element of the carrier of V2
g * (Sum f) is Element of the carrier of V2
the lmult of V2 . (g,(Sum f)) is Element of the carrier of V2
len ((len f) |-> g) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
dom ((len f) |-> g) is finite len f -element Element of bool NAT

dom (lmlt (((len f) |-> g),f)) is finite Element of bool NAT
len (lmlt (((len f) |-> g),f)) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

0. V2 is V47(V2) Element of the carrier of V2
the ZeroF of V2 is Element of the carrier of V2

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set
V2 is Element of the carrier of V1

len V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

(len V3) -tuples_on the carrier of V1 is functional non empty FinSequence-membered FinSequenceSet of the carrier of V1
lmlt (V3,((len V3) |-> V2)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (V3,((len V3) |-> V2)) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1
Sum (lmlt (V3,((len V3) |-> V2))) is Element of the carrier of V1
Sum V3 is Element of the carrier of K
(Sum V3) * V2 is Element of the carrier of V1
the lmult of V1 . ((Sum V3),V2) is Element of the carrier of V1
len ((len V3) |-> V2) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
dom ((len V3) |-> V2) is finite len V3 -element Element of bool NAT
dom V3 is finite Element of bool NAT
dom (lmlt (V3,((len V3) |-> V2))) is finite Element of bool NAT
A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
A is Element of the carrier of K
V3 . A is set
Seg (len V3) is finite len V3 -element V136() Element of bool NAT
{ b1 where b1 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT : ( 1 <= b1 & b1 <= len V3 ) } is set
((len V3) |-> V2) . A is set
(lmlt (V3,((len V3) |-> V2))) . A is set
A * V2 is Element of the carrier of V1
the lmult of V1 . (A,V2) is Element of the carrier of V1
len (lmlt (V3,((len V3) |-> V2))) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

the carrier of K is non empty non trivial set
V1 is Element of the carrier of K

the carrier of V2 is non empty set

V1 multfield is Relation-like 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:] is Relation-like set
bool [: the carrier of K, the carrier of K:] is set
the multF of K is Relation-like Function-like 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:], the carrier of K:] is Relation-like set
bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is set
id the carrier of K is Relation-like the carrier of K -defined the carrier of K -valued Function-like one-to-one non empty total quasi_total Element of bool [: the carrier of K, the carrier of K:]
K378( the carrier of K, the carrier of K, the multF of K,V1,(id the carrier of K)) is Relation-like Function-like non empty total quasi_total Element of bool [: the carrier of K, the carrier of K:]

lmlt ((V1 * f),V3) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
the lmult of V2 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V2:], the carrier of V2:] is Relation-like set
bool [:[: the carrier of K, the carrier of V2:], the carrier of V2:] is set
the lmult of V2 .: ((V1 * f),V3) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum (lmlt ((V1 * f),V3)) is Element of the carrier of V2

the lmult of V2 .: (f,V3) is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V2
Sum (lmlt (f,V3)) is Element of the carrier of V2
V1 * (Sum (lmlt (f,V3))) is Element of the carrier of V2
the lmult of V2 . (V1,(Sum (lmlt (f,V3)))) is Element of the carrier of V2
len (V1 * f) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
len f is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
dom (V1 * f) is finite Element of bool NAT

dom (lmlt ((V1 * f),V3)) is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom (V1 * f)) /\ (dom V3) is finite Element of bool NAT
dom (lmlt (f,V3)) is finite Element of bool NAT
(dom f) /\ (dom V3) is finite Element of bool NAT
A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
(lmlt (f,V3)) . A is set
(lmlt ((V1 * f),V3)) . A is set
AI is Element of the carrier of V2
V1 * AI is Element of the carrier of V2
the lmult of V2 . (V1,AI) is Element of the carrier of V2
V3 /. A is Element of the carrier of V2
V3 . A is set
f /. A is Element of the carrier of K
f . A is set
(V1 * f) . A is set
V1 * (f /. A) is Element of the carrier of K
(V1 * (f /. A)) * (V3 /. A) is Element of the carrier of V2
the lmult of V2 . ((V1 * (f /. A)),(V3 /. A)) is Element of the carrier of V2
(f /. A) * (V3 /. A) is Element of the carrier of V2
the lmult of V2 . ((f /. A),(V3 /. A)) is Element of the carrier of V2
V1 * ((f /. A) * (V3 /. A)) is Element of the carrier of V2
the lmult of V2 . (V1,((f /. A) * (V3 /. A))) is Element of the carrier of V2
len (lmlt (f,V3)) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
len (lmlt ((V1 * f),V3)) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

the carrier of K is non empty non trivial set

the carrier of V1 is non empty set

the lmult of V1 is Relation-like Function-like 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 set
[:[: the carrier of K, the carrier of V1:], the carrier of V1:] is Relation-like set
bool [:[: the carrier of K, the carrier of V1:], the carrier of V1:] is set
the lmult of V1 .: (V2,V3) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

the carrier of f is non empty set

the lmult of f is Relation-like Function-like total quasi_total Element of bool [:[: the carrier of K, the carrier of f:], the carrier of f:]
[: the carrier of K, the carrier of f:] is Relation-like set
[:[: the carrier of K, the carrier of f:], the carrier of f:] is Relation-like set
bool [:[: the carrier of K, the carrier of f:], the carrier of f:] is set
the lmult of f .: (V2,g) is Relation-like NAT -defined the carrier of f -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of f
dom (lmlt (V2,V3)) is finite Element of bool NAT
dom V2 is finite Element of bool NAT
dom V3 is finite Element of bool NAT
(dom V2) /\ (dom V3) is finite Element of bool NAT
dom (lmlt (V2,g)) is finite Element of bool NAT

(dom V2) /\ (dom g) is finite Element of bool NAT
AI is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
V2 . AI is set
V2 /. AI is Element of the carrier of K
g . AI is set
g /. AI is Element of the carrier of f
V3 . AI is set
V3 /. AI is Element of the carrier of V1
(lmlt (V2,V3)) . AI is set
(V2 /. AI) * (V3 /. AI) is Element of the carrier of V1
the lmult of V1 . ((V2 /. AI),(V3 /. AI)) is Element of the carrier of V1
(V2 /. AI) * (g /. AI) is Element of the carrier of f
the lmult of f . ((V2 /. AI),(g /. AI)) is Element of the carrier of f
(lmlt (V2,g)) . AI is set

the carrier of V1 is non empty set

Sum V2 is Element of the carrier of V1

the carrier of V3 is non empty set

Sum f is Element of the carrier of V3
g is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() set
g + 1 is non empty V21() V22() V23() V27() finite cardinal ext-real positive non negative V93() V94() Element of NAT

len A is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
Sum A is Element of the carrier of V1

the carrier of AI is non empty set

Sum S is Element of the carrier of AI

{ b1 where b1 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT : ( 1 <= b1 & b1 <= g ) } is set

len (A | g) is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT
Sum (A | g) is Element of the carrier of V1