:: MATRLIN2 semantic presentation

REAL is set

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

bool REAL is set

K583() is strict doubleLoopStr

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

COMPLEX is set

RAT is set

INT is set

{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V93() V94() 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

0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non 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

[:REAL,REAL:] is Relation-like set

bool [:REAL,REAL:] is 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

card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V93() V94() set

Seg 1 is non empty trivial finite 1 -element V136() Element of bool NAT

{ b

{1} is non empty trivial finite V32() 1 -element set

Seg 2 is non empty finite 2 -element V136() Element of bool NAT

{ b

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 VectSpStr over K

f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

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

V3 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

V2 /\ V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

V2 + V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

g is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of f

A is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of f

g /\ A is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of f

g + A is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of f

A is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

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

AI is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 VectSpStr over K

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

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

V3 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

V2 /\ V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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

V2 + V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

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

MAI is Relation-like Function-like total quasi_total Linear_Combination of AI

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

{ b

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

(0). (V2 + V3) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2 + V3

f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2 + V3

g is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2 + V3

f /\ g is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2 + V3

f + g is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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

A12 is Relation-like Function-like total quasi_total Linear_Combination of V2 + V3

Carrier A12 is finite Element of bool the carrier of (V2 + V3)

{ b

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

fbi is Relation-like Function-like total quasi_total Linear_Combination of V2 + V3

Carrier fbi is finite Element of bool the carrier of (V2 + V3)

{ b

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

b2n is Relation-like Function-like total quasi_total Linear_Combination of S

Carrier b2n is finite Element of bool the carrier of (V2 + V3)

{ b

Sum b2n is Element of the carrier of (V2 + V3)

v is Relation-like Function-like total quasi_total Linear_Combination of f

Carrier v is finite Element of bool the carrier of f

bool the carrier of f is set

{ b

Sum v is Element of the carrier of f

i is Relation-like Function-like total quasi_total Linear_Combination of KER

b2n + i is Relation-like Function-like total quasi_total Linear_Combination of V2 + V3

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)

{ b

the carrier of g is non empty set

v is Relation-like Function-like total quasi_total Linear_Combination of g

Carrier v is finite Element of bool the carrier of g

bool the carrier of g is set

{ b

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

{} \/ {} is Relation-like finite V32() set

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 VectSpStr over K

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

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

V3 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

V2 /\ V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

V2 + V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V1

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

(Omega). V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V3

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

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

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

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

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

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

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

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

(Lin A) + (Lin AI) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2 + V3

(Omega). V2 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V2

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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 finite-dimensional VectSpStr over K

(Omega). V1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of V1

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

V2 is Relation-like NAT -defined the carrier of ((Omega). V1) -valued Function-like finite FinSequence-like FinSubsequence-like OrdBasis of (Omega). V1

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

Lin f is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of V1

Lin V3 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of (Omega). V1

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 VectSpStr over K

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

Lin V2 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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)

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

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

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

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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 VectSpStr over K

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

Lin V2 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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)

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

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

Lin g is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

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 V2 is finite Element of bool NAT

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

V1 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 is finite Element of bool NAT

V2 is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier 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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 finite-dimensional VectSpStr over K

the carrier of V1 is non empty set

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 V2 is finite Element of bool NAT

V3 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier 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 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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

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

V3 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,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,V2) is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

f is Relation-like NAT -defined the carrier of K -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier 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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

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

V3 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier 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 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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

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 V2 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

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 V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

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

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

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

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

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

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

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

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

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

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

AI is Relation-like NAT -defined the carrier of K -valued Function-like finite len f -element FinSequence-like FinSubsequence-like Element of (len f) -tuples_on the carrier of K

A is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len f -element FinSequence-like FinSubsequence-like Element of (len f) -tuples_on the carrier of V1

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

S is Relation-like NAT -defined the carrier of K -valued Function-like finite len g -element FinSequence-like FinSubsequence-like Element of (len g) -tuples_on the carrier of K

A is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len g -element FinSequence-like FinSubsequence-like Element of (len g) -tuples_on 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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 finite-dimensional VectSpStr over K

the carrier of V1 is non empty set

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

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 V3 is V21() V22() V23() V27() finite cardinal ext-real non negative V93() V94() Element of NAT

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

f is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len V2 -element FinSequence-like FinSubsequence-like Element of (len V2) -tuples_on the carrier of V1

g is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len V2 -element FinSequence-like FinSubsequence-like Element of (len V2) -tuples_on the carrier of V1

f + g is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len V2 -element FinSequence-like FinSubsequence-like Element of (len V2) -tuples_on 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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

V1 is Element of the carrier of K

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

the carrier of V2 is non empty set

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

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

(len V3) |-> V1 is Relation-like NAT -defined the carrier of K -valued Function-like finite len V3 -element FinSequence-like FinSubsequence-like Element of (len V3) -tuples_on the carrier of K

(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

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

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) |-> A is Relation-like NAT -defined the carrier of K -valued Function-like finite len A -element FinSequence-like FinSubsequence-like Element of (len A) -tuples_on 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

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

Seg f is finite f -element V136() Element of bool NAT

{ b

A | (Seg f) is Relation-like NAT -defined Seg f -defined NAT -defined the carrier of V2 -valued Function-like finite FinSubsequence-like 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

dom A is finite Element of bool NAT

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

A . (f + 1) is set

<*A*> is Relation-like NAT -defined the carrier of K -valued Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of K

[1,A] is set

{1,A} is non empty finite set

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

{[1,A]} is Relation-like Function-like constant non empty trivial finite 1 -element set

<*(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 /. (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

<*(A . (f + 1))*> is Relation-like NAT -defined Function-like constant non empty trivial finite 1 -element FinSequence-like FinSubsequence-like 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

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) |-> A is Relation-like NAT -defined the carrier of K -valued Function-like finite f + 1 -element FinSequence-like FinSubsequence-like Element of (f + 1) -tuples_on the carrier of K

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

f |-> A is Relation-like NAT -defined the carrier of K -valued Function-like finite f -element FinSequence-like FinSubsequence-like Element of f -tuples_on the carrier of K

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

(f |-> A) ^ <*A*> is Relation-like NAT -defined the carrier of K -valued Function-like non empty finite f + 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of K

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

(A | f) ^ <*(A . (f + 1))*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

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

f is Relation-like NAT -defined the carrier of V2 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence 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) |-> g is Relation-like NAT -defined the carrier of K -valued Function-like finite len f -element FinSequence-like FinSubsequence-like Element of (len f) -tuples_on 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 f is finite 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

<*> the carrier of V2 is Relation-like non-empty empty-yielding NAT -defined the carrier of V2 -valued Function-like one-to-one constant functional empty V21() V22() V23() V25() V26() V27() finite finite-yielding V32() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V93() V94() FinSequence of the carrier of V2

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

the ZeroF of V2 is Element of the carrier of V2

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

V2 is Element of the carrier of V1

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

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

(len V3) |-> V2 is Relation-like NAT -defined the carrier of V1 -valued Function-like finite len V3 -element FinSequence-like FinSubsequence-like Element of (len V3) -tuples_on the carrier of V1

(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

{ b

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

V1 is Element of the carrier of K

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

the carrier of V2 is non empty set

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

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

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

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

(V1 multfield) * 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 ((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

lmlt (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 .: (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 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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty non trivial set

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

the carrier of V1 is non empty set

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

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 (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 .: (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

f is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of V1

the carrier of f is non empty set

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

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

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

K is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative right-distributive left-distributive right_unital well-unital distributive 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 finite-dimensional VectSpStr over K

the carrier of V1 is non empty set

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 V2 is Element of the carrier of V1

V3 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of V1

the carrier of V3 is non empty set

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

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

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

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

AI is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed finite-dimensional Subspace of V1

the carrier of AI is non empty set

S is Relation-like NAT -defined the carrier of AI -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of AI

Sum S is Element of the carrier of AI

A | g is Relation-like NAT -defined the carrier of V1 -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V1

Seg g is finite g -element V136() Element of bool NAT

{ b

A | (Seg g) is Relation-like NAT -defined Seg g -defined NAT -defined the carrier of V1 -valued Function-like finite FinSubsequence-like 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

S | g is Relation-like NAT -defined the carrier of AI -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of AI

S | (Seg g) is Relation-like NAT -defined Seg g -defined NAT -defined the