:: VECTSP_9 semantic presentation

REAL is set

NAT is V6() V7() V8() non empty V19() non finite cardinal limit_cardinal Element of K27(REAL)

K27(REAL) is non empty set

NAT is V6() V7() V8() non empty V19() non finite cardinal limit_cardinal set

K27(NAT) is non empty V19() non finite set

K27(NAT) is non empty V19() non finite set

COMPLEX is set

RAT is set

INT is set

{} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() set

2 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

3 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

card {} is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() set

Seg 1 is non empty V19() finite 1 -element Element of K27(NAT)

0 is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() Element of NAT

GF is non empty 1-sorted

the carrier of GF is non empty set

K27( the carrier of GF) is non empty set

the non empty Element of K27( the carrier of GF) is non empty Element of K27( the carrier of GF)

n is set

GF is set

{n} is non empty V19() finite 1 -element set

GF \ {n} is Element of K27(GF)

K27(GF) is non empty set

(GF \ {n}) \/ {n} is non empty set

{n} \/ (GF \ {n}) is non empty set

{n} \/ GF is non empty set

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

dom W is finite Element of K27(NAT)

K28((dom W),(dom W)) is Relation-like finite set

K27(K28((dom W),(dom W))) is non empty finite V28() set

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

V (#) W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W) is Element of the carrier of n

V (#) x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) x) is Element of the carrier of n

A is Relation-like dom W -defined dom W -valued Function-like one-to-one finite total quasi_total onto bijective Element of K27(K28((dom W),(dom W)))

W * A is Relation-like dom W -defined the carrier of n -valued Function-like finite Element of K27(K28((dom W), the carrier of n))

K28((dom W), the carrier of n) is Relation-like set

K27(K28((dom W), the carrier of n)) is non empty set

len x is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len W is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len (V (#) W) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom (V (#) W) is finite Element of K27(NAT)

(V (#) W) * A is Relation-like dom W -defined the carrier of n -valued Function-like finite Element of K27(K28((dom W), the carrier of n))

B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len B is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom B is finite Element of K27(NAT)

len (V (#) x) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom (V (#) x) is finite Element of K27(NAT)

dom x is finite Element of K27(NAT)

I1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

A . I1 is set

dom A is finite set

rng A is finite set

x /. I1 is Element of the carrier of n

x . I1 is set

W . (A . I1) is set

I1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

W /. I1 is Element of the carrier of n

(V (#) x) . I1 is set

V . (W /. I1) is Element of the carrier of GF

(V . (W /. I1)) * (W /. I1) is Element of the carrier of n

(V (#) W) . (A . I1) is set

B . I1 is set

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

V is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier V is finite Element of K27( the carrier of n)

K27( the carrier of n) is non empty set

W is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

x is set

<*x*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

W ^ <*x*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

V (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W1) is Element of the carrier of n

{x} is non empty V19() finite 1 -element set

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

rng A is finite set

(Carrier V) /\ (rng W1) is finite Element of K27( the carrier of n)

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

B is Element of the carrier of n

<*B*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng <*B*> is non empty V19() finite 1 -element set

(rng W1) \/ (rng <*B*>) is non empty finite set

(Carrier V) /\ ((rng W1) \/ (rng <*B*>)) is finite Element of K27( the carrier of n)

{B} is non empty V19() finite 1 -element Element of K27( the carrier of n)

(rng W1) \/ {B} is non empty finite set

(Carrier V) /\ ((rng W1) \/ {B}) is finite Element of K27( the carrier of n)

(Carrier V) /\ (rng W1) is finite Element of K27( the carrier of n)

(Carrier V) /\ {B} is finite Element of K27( the carrier of n)

((Carrier V) /\ (rng W1)) \/ ((Carrier V) /\ {B}) is finite Element of K27( the carrier of n)

V (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W1) is Element of the carrier of n

V . B is Element of the carrier of GF

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

V (#) A is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(V (#) W1) ^ (V (#) A) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((V (#) W1) ^ (V (#) A)) is Element of the carrier of n

Sum (V (#) A) is Element of the carrier of n

(Sum (V (#) W1)) + (Sum (V (#) A)) is Element of the carrier of n

(V . B) * B is Element of the carrier of n

<*((V . B) * B)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum <*((V . B) * B)*> is Element of the carrier of n

(0. n) + (Sum <*((V . B) * B)*>) is Element of the carrier of n

(0. GF) * B is Element of the carrier of n

W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W is finite set

V (#) W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W) is Element of the carrier of n

<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() FinSequence of the carrier of n

K28(NAT, the carrier of n) is Relation-like non empty V19() non finite set

W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W is finite set

V (#) W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W) is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng V is finite set

K27((rng V)) is non empty finite V28() set

x is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier x is finite Element of K27( the carrier of n)

K27( the carrier of n) is non empty set

x (#) V is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (x (#) V) is Element of the carrier of n

Sum x is Element of the carrier of n

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

x (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (x (#) W1) is Element of the carrier of n

W1 is finite Element of K27((rng V))

W1 ` is finite Element of K27((rng V))

(rng V) \ W1 is finite set

V - (W1 `) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

W is finite Element of K27((rng V))

W \ (W1 `) is finite Element of K27((rng V))

(W1 `) ` is finite Element of K27((rng V))

(rng V) \ (W1 `) is finite set

W /\ ((W1 `) `) is finite Element of K27((rng V))

rng (V - (W1 `)) is finite set

dom W1 is finite Element of K27(NAT)

K28((dom W1),(dom W1)) is Relation-like finite set

K27(K28((dom W1),(dom W1))) is non empty finite V28() set

V - W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng I1 is finite set

(rng V) \ (rng W1) is finite Element of K27((rng V))

dom V is finite Element of K27(NAT)

K28((dom V),(dom V)) is Relation-like finite set

K27(K28((dom V),(dom V))) is non empty finite V28() set

(V - (W1 `)) ^ (V - W1) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B ^ I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

x (#) (B ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (x (#) (B ^ I1)) is Element of the carrier of n

x (#) B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

x (#) I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(x (#) B) ^ (x (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((x (#) B) ^ (x (#) I1)) is Element of the carrier of n

Sum (x (#) B) is Element of the carrier of n

Sum (x (#) I1) is Element of the carrier of n

(Sum (x (#) B)) + (Sum (x (#) I1)) is Element of the carrier of n

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

(Sum (x (#) B)) + (0. n) is Element of the carrier of n

(Sum (x (#) W1)) + (0. n) is Element of the carrier of n

I2 is Relation-like dom V -defined dom V -valued Function-like one-to-one finite total quasi_total onto bijective Element of K27(K28((dom V),(dom V)))

V * I2 is Relation-like dom V -defined the carrier of n -valued Function-like finite Element of K27(K28((dom V), the carrier of n))

K28((dom V), the carrier of n) is Relation-like set

K27(K28((dom V), the carrier of n)) is non empty set

I2 is Relation-like dom W1 -defined dom W1 -valued Function-like one-to-one finite total quasi_total onto bijective Element of K27(K28((dom W1),(dom W1)))

W1 * I2 is Relation-like dom W1 -defined the carrier of n -valued Function-like finite Element of K27(K28((dom W1), the carrier of n))

K28((dom W1), the carrier of n) is Relation-like set

K27(K28((dom W1), the carrier of n)) is non empty set

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier V is finite Element of K27( the carrier of n)

K27( the carrier of n) is non empty set

W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W is finite set

(rng W) /\ (Carrier V) is finite Element of K27( the carrier of n)

V (#) W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

W1 is set

V . W1 is set

W1 is Element of the carrier of n

V . W1 is Element of the carrier of GF

K28( the carrier of n, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of n, the carrier of GF)) is non empty set

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of n, the carrier of GF))

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of n, the carrier of GF))

W1 is Element of the carrier of n

x is finite Element of K27( the carrier of n)

x /\ (Carrier V) is finite Element of K27( the carrier of n)

W1 . W1 is Element of the carrier of GF

W1 . W1 is Element of the carrier of GF

V . W1 is set

V . W1 is Element of the carrier of GF

Funcs ( the carrier of n, the carrier of GF) is functional non empty FUNCTION_DOMAIN of the carrier of n, the carrier of GF

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Element of Funcs ( the carrier of n, the carrier of GF)

B is set

I1 is Element of the carrier of n

V . I1 is Element of the carrier of GF

A is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

A . I1 is Element of the carrier of GF

Carrier A is finite Element of K27( the carrier of n)

A (#) W is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len (V (#) W) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len W is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len (A (#) W) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom (V (#) W) is finite Element of K27(NAT)

dom (A (#) W) is finite Element of K27(NAT)

dom W is finite Element of K27(NAT)

I2 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

W /. I2 is Element of the carrier of n

A . (W /. I2) is Element of the carrier of GF

V . (W /. I2) is set

W . I2 is set

(V (#) W) . I2 is set

V . (W /. I2) is Element of the carrier of GF

(V . (W /. I2)) * (W /. I2) is Element of the carrier of n

(A (#) W) . I2 is set

B is set

I1 is Element of the carrier of n

A . I1 is Element of the carrier of GF

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

W is Element of K27( the carrier of n)

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of (Lin W) is non empty set

x is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

x + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

len W1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

V (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W1) is Element of the carrier of n

W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

A is set

<*A*> is Relation-like NAT -defined Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like set

W1 ^ <*A*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B ^ <*A*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set

rng (B ^ <*A*>) is non empty finite set

rng B is finite set

rng <*A*> is non empty V19() finite 1 -element set

(rng B) \/ (rng <*A*>) is non empty finite set

{A} is non empty V19() finite 1 -element set

(rng B) \/ {A} is non empty finite set

I2 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum I2 is Element of the carrier of n

I1 is Element of the carrier of n

<*I1*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

B ^ <*I1*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len (B ^ <*I1*>) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

len B is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len <*I1*> is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

(len B) + (len <*I1*>) is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

(len B) + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

V (#) B is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) B) is Element of the carrier of n

A is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum A is Element of the carrier of n

V . I1 is Element of the carrier of GF

(V . I1) * I2 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

A + ((V . I1) * I2) is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

V (#) I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(V (#) B) ^ (V (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((V (#) B) ^ (V (#) I1)) is Element of the carrier of n

Sum (V (#) I1) is Element of the carrier of n

(Sum A) + (Sum (V (#) I1)) is Element of the carrier of n

(V . I1) * I1 is Element of the carrier of n

<*((V . I1) * I1)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum <*((V . I1) * I1)*> is Element of the carrier of n

(Sum A) + (Sum <*((V . I1) * I1)*>) is Element of the carrier of n

(V . I1) * (Sum I2) is Element of the carrier of n

(Sum A) + ((V . I1) * (Sum I2)) is Element of the carrier of n

Sum ((V . I1) * I2) is Element of the carrier of n

(Sum A) + (Sum ((V . I1) * I2)) is Element of the carrier of n

Sum (A + ((V . I1) * I2)) is Element of the carrier of n

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng x is finite set

V (#) x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) x) is Element of the carrier of n

len x is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

len W1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

V (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) W1) is Element of the carrier of n

<*> the carrier of n is Relation-like non-empty empty-yielding NAT -defined the carrier of n -valued V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() FinSequence of the carrier of n

K28(NAT, the carrier of n) is Relation-like non empty V19() non finite set

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

ZeroLC n is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Sum (ZeroLC n) is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier V is finite Element of K27( the carrier of n)

Sum V is Element of the carrier of n

W is Element of K27( the carrier of n)

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of (Lin W) is non empty set

x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng x is finite set

V (#) x is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (V (#) x) is Element of the carrier of n

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum W1 is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

W is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier W is finite Element of K27( the carrier of n)

K27( the carrier of n) is non empty set

W | the carrier of V is Relation-like the carrier of n -defined the carrier of V -defined the carrier of n -defined the carrier of GF -valued Function-like Element of K27(K28( the carrier of n, the carrier of GF))

K28( the carrier of n, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of n, the carrier of GF)) is non empty set

Sum W is Element of the carrier of n

x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier x is finite Element of K27( the carrier of V)

K27( the carrier of V) is non empty set

Sum x is Element of the carrier of V

dom x is set

W1 is set

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

W1 is Element of the carrier of V

x . W1 is Element of the carrier of GF

W . W1 is set

W1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng W1 is finite set

x (#) W1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (x (#) W1) is Element of the carrier of V

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng W1 is finite set

W (#) W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (W (#) W1) is Element of the carrier of n

A is set

B is Element of the carrier of n

W . B is Element of the carrier of GF

x . B is set

dom W1 is finite Element of K27(NAT)

K28((dom W1),(dom W1)) is Relation-like finite set

K27(K28((dom W1),(dom W1))) is non empty finite V28() set

A is Relation-like dom W1 -defined dom W1 -valued Function-like one-to-one finite total quasi_total onto bijective Element of K27(K28((dom W1),(dom W1)))

W1 * A is Relation-like dom W1 -defined the carrier of V -valued Function-like finite Element of K27(K28((dom W1), the carrier of V))

K28((dom W1), the carrier of V) is Relation-like set

K27(K28((dom W1), the carrier of V)) is non empty set

len (x (#) W1) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

len W1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom (x (#) W1) is finite Element of K27(NAT)

(x (#) W1) * A is Relation-like dom W1 -defined the carrier of V -valued Function-like finite Element of K27(K28((dom W1), the carrier of V))

B is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

len B is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom B is finite Element of K27(NAT)

rng B is finite set

K28(NAT, the carrier of V) is Relation-like non empty V19() non finite set

K27(K28(NAT, the carrier of V)) is non empty V19() non finite set

Sum B is Element of the carrier of V

0. V is V51(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

I1 is Relation-like NAT -defined the carrier of V -valued Function-like non empty total quasi_total Element of K27(K28(NAT, the carrier of V))

I1 . (len B) is Element of the carrier of V

I1 . 0 is Element of the carrier of V

dom I1 is non empty set

rng I1 is non empty set

K28(NAT, the carrier of n) is Relation-like non empty V19() non finite set

K27(K28(NAT, the carrier of n)) is non empty V19() non finite set

I2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

len I2 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

A is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of K27(K28(NAT, the carrier of n))

A is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

A + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

I2 . (A + 1) is set

A . (A + 1) is Element of the carrier of n

A . A is Element of the carrier of n

A9 is Element of the carrier of n

(A . A) + A9 is Element of the carrier of n

I1 . (A + 1) is Element of the carrier of V

I1 . A is Element of the carrier of V

x is Element of the carrier of V

(I1 . A) + x is Element of the carrier of V

len W1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom W1 is finite Element of K27(NAT)

len (W (#) W1) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

dom (W (#) W1) is finite Element of K27(NAT)

A is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

W1 /. A is Element of the carrier of n

A . A is set

W1 . A is set

dom A is finite set

rng A is finite set

w2 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

W1 /. w2 is Element of the carrier of V

W1 . (A . A) is set

B . A is set

(x (#) W1) . w2 is set

w1 is Element of the carrier of V

x . w1 is Element of the carrier of GF

(x . w1) * w1 is Element of the carrier of V

W . (W1 /. A) is Element of the carrier of GF

(W . (W1 /. A)) * w1 is Element of the carrier of V

(W . (W1 /. A)) * (W1 /. A) is Element of the carrier of n

(W (#) W1) . A is set

K28((dom (x (#) W1)),(dom (x (#) W1))) is Relation-like finite set

K27(K28((dom (x (#) W1)),(dom (x (#) W1)))) is non empty finite V28() set

A is Relation-like dom (x (#) W1) -defined dom (x (#) W1) -valued Function-like one-to-one finite total quasi_total onto bijective Element of K27(K28((dom (x (#) W1)),(dom (x (#) W1))))

(x (#) W1) * A is Relation-like dom (x (#) W1) -defined the carrier of V -valued Function-like finite Element of K27(K28((dom (x (#) W1)), the carrier of V))

K28((dom (x (#) W1)), the carrier of V) is Relation-like set

K27(K28((dom (x (#) W1)), the carrier of V)) is non empty set

A . (len I2) is Element of the carrier of n

A . 0 is Element of the carrier of n

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

W is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier W is finite Element of K27( the carrier of V)

K27( the carrier of V) is non empty set

Sum W is Element of the carrier of V

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

K28( the carrier of V, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of V, the carrier of GF)) is non empty set

K27( the carrier of n) is non empty set

W1 is set

W . W1 is set

A is Element of the carrier of n

B is Element of the carrier of V

W . B is Element of the carrier of GF

W . B is set

A is Element of the carrier of n

A is Element of the carrier of n

K28( the carrier of n, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of n, the carrier of GF)) is non empty set

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of n, the carrier of GF))

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of n, the carrier of GF))

A is Element of the carrier of n

W1 is finite Element of K27( the carrier of n)

W . A is set

W1 . A is Element of the carrier of GF

Funcs ( the carrier of n, the carrier of GF) is functional non empty FUNCTION_DOMAIN of the carrier of n, the carrier of GF

A is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

A | the carrier of V is Relation-like the carrier of n -defined the carrier of V -defined the carrier of n -defined the carrier of GF -valued Function-like Element of K27(K28( the carrier of n, the carrier of GF))

Carrier A is finite Element of K27( the carrier of n)

Sum A is Element of the carrier of n

I1 is set

I2 is Element of the carrier of n

A . I2 is Element of the carrier of GF

W . I2 is set

I1 is set

A . I1 is set

W . I1 is set

x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of V, the carrier of GF))

x . I1 is set

B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of V, the carrier of GF))

B . I1 is set

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

the carrier of GF is non empty V19() set

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

W is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier W is finite Element of K27( the carrier of n)

K27( the carrier of n) is non empty set

Sum W is Element of the carrier of n

K27( the carrier of V) is non empty set

K28( the carrier of V, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of V, the carrier of GF)) is non empty set

W | the carrier of V is Relation-like the carrier of n -defined the carrier of V -defined the carrier of n -defined the carrier of GF -valued Function-like Element of K27(K28( the carrier of n, the carrier of GF))

K28( the carrier of n, the carrier of GF) is Relation-like non empty set

K27(K28( the carrier of n, the carrier of GF)) is non empty set

W1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like non empty total quasi_total Element of K27(K28( the carrier of V, the carrier of GF))

Funcs ( the carrier of V, the carrier of GF) is functional non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF

dom W1 is non empty set

W1 is Element of the carrier of V

x is finite Element of K27( the carrier of V)

W . W1 is set

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

W1 . W1 is Element of the carrier of GF

W1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier W1 is finite Element of K27( the carrier of V)

Sum W1 is Element of the carrier of V

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

V is Basis of n

Lin V is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W is Element of the carrier of n

the U5 of n is Relation-like K28( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K27(K28(K28( the carrier of n, the carrier of n), the carrier of n))

K28( the carrier of n, the carrier of n) is Relation-like non empty set

K28(K28( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set

K27(K28(K28( the carrier of n, the carrier of n), the carrier of n)) is non empty set

the ZeroF of n is Element of the carrier of n

the lmult of n is Relation-like K28( the carrier of GF, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K27(K28(K28( the carrier of GF, the carrier of n), the carrier of n))

the carrier of GF is non empty V19() set

K28( the carrier of GF, the carrier of n) is Relation-like non empty set

K28(K28( the carrier of GF, the carrier of n), the carrier of n) is Relation-like non empty set

K27(K28(K28( the carrier of GF, the carrier of n), the carrier of n)) is non empty set

VectSpStr(# the carrier of n, the U5 of n, the ZeroF of n, the lmult of n #) is non empty strict VectSpStr over GF

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

{} n is Relation-like non-empty empty-yielding NAT -defined V6() V7() V8() V10() V11() V12() Function-like one-to-one constant functional empty proper finite finite-yielding V28() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V38() V58() linearly-independent Element of K27( the carrier of n)

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

K27( the carrier of V) is non empty set

W is Element of K27( the carrier of V)

x is Element of K27( the carrier of n)

the carrier of GF is non empty V19() set

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of x

Sum W1 is Element of the carrier of n

Carrier W1 is finite Element of K27( the carrier of n)

W1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier W1 is finite Element of K27( the carrier of V)

Sum W1 is Element of the carrier of V

A is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum A is Element of the carrier of V

0. V is V51(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

K27( the carrier of V) is non empty set

W is Element of K27( the carrier of n)

x is Element of K27( the carrier of V)

the carrier of GF is non empty V19() set

0. V is V51(V) Element of the carrier of V

the ZeroF of V is Element of the carrier of V

W1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of x

Sum W1 is Element of the carrier of V

Carrier W1 is finite Element of K27( the carrier of V)

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier W1 is finite Element of K27( the carrier of n)

Sum W1 is Element of the carrier of n

A is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum A is Element of the carrier of n

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W is Basis of V

the carrier of n is non empty set

K27( the carrier of n) is non empty set

x is linearly-independent Element of K27( the carrier of n)

W1 is Basis of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is Element of K27( the carrier of n)

W is Element of the carrier of n

{W} is non empty V19() finite 1 -element Element of K27( the carrier of n)

V \ {W} is Element of K27( the carrier of n)

K27(V) is non empty set

Lin {W} is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of GF is non empty V19() set

x is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of {W}

Sum x is Element of the carrier of n

W1 is Element of K27( the carrier of n)

Lin W1 is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W1 \/ {W} is non empty Element of K27( the carrier of n)

V \/ V is Element of K27( the carrier of n)

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W1

Sum W1 is Element of the carrier of n

Carrier W1 is finite Element of K27( the carrier of n)

Carrier x is finite Element of K27( the carrier of n)

(Carrier W1) \/ (Carrier x) is finite Element of K27( the carrier of n)

W1 - x is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier (W1 - x) is finite Element of K27( the carrier of n)

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

A is Element of the carrier of n

x . A is Element of the carrier of GF

A is set

B is Element of the carrier of n

W1 . B is Element of the carrier of GF

(W1 - x) . B is Element of the carrier of GF

x . B is Element of the carrier of GF

(W1 . B) - (x . B) is Element of the carrier of GF

(W1 . B) - (0. GF) is Element of the carrier of GF

- (0. GF) is Element of the carrier of GF

(W1 . B) + (- (0. GF)) is Element of the carrier of GF

(W1 . B) + (0. GF) is Element of the carrier of GF

0. n is V51(n) Element of the carrier of n

the ZeroF of n is Element of the carrier of n

A is set

- (Sum x) is Element of the carrier of n

(Sum W1) + (- (Sum x)) is Element of the carrier of n

- x is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Sum (- x) is Element of the carrier of n

(Sum W1) + (Sum (- x)) is Element of the carrier of n

W1 + (- x) is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Sum (W1 + (- x)) is Element of the carrier of n

Sum (W1 - x) is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is Basis of n

W is non empty Element of K27( the carrier of n)

V \/ W is non empty Element of K27( the carrier of n)

x is set

W1 is Element of K27( the carrier of n)

W1 is Element of the carrier of n

{W1} is non empty V19() finite 1 -element Element of K27( the carrier of n)

W1 \ {W1} is Element of K27( the carrier of n)

V \ {W1} is Element of K27( the carrier of n)

A is Element of K27( the carrier of n)

Lin V is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

Lin A is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

W is Element of K27( the carrier of n)

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

x is set

the carrier of (Lin W) is non empty set

the carrier of GF is non empty V19() set

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum W1 is Element of the carrier of n

Carrier W1 is finite Element of K27( the carrier of n)

W1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier W1 is finite Element of K27( the carrier of V)

K27( the carrier of V) is non empty set

Sum W1 is Element of the carrier of V

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

the carrier of V is non empty set

K27( the carrier of V) is non empty set

W is Element of K27( the carrier of n)

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

x is Element of K27( the carrier of V)

Lin x is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of V

W1 is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

W1 is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

A is set

the carrier of (Lin W) is non empty set

the carrier of GF is non empty V19() set

B is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum B is Element of the carrier of n

Carrier B is finite Element of K27( the carrier of n)

I1 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V

Carrier I1 is finite Element of K27( the carrier of V)

Sum I1 is Element of the carrier of V

I2 is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of x

Sum I2 is Element of the carrier of V

the carrier of (Lin x) is non empty set

A is set

B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of x

Sum B is Element of the carrier of V

Carrier B is finite Element of K27( the carrier of V)

I1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier I1 is finite Element of K27( the carrier of n)

Sum I1 is Element of the carrier of n

I2 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of W

Sum I2 is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is finite Element of K27( the carrier of n)

W is finite Element of K27( the carrier of n)

V \/ W is finite Element of K27( the carrier of n)

Lin (V \/ W) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

x is Element of the carrier of n

{x} is non empty V19() finite 1 -element Element of K27( the carrier of n)

the carrier of GF is non empty V19() set

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of V \/ W

Sum W1 is Element of the carrier of n

Lin {x} is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of {x}

Sum W1 is Element of the carrier of n

Carrier W1 is finite Element of K27( the carrier of n)

0. GF is V51(GF) Element of the carrier of GF

the ZeroF of GF is Element of the carrier of GF

A is set

B is Element of the carrier of n

W1 . B is Element of the carrier of GF

A is Element of the carrier of n

W1 . A is Element of the carrier of GF

A is Element of the carrier of n

W1 . A is Element of the carrier of GF

{A} is non empty V19() finite 1 -element Element of K27( the carrier of n)

(V \/ W) \ {A} is finite Element of K27( the carrier of n)

((V \/ W) \ {A}) \/ {x} is non empty finite Element of K27( the carrier of n)

Lin (((V \/ W) \ {A}) \/ {x}) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng I1 is finite set

W1 (#) I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (W1 (#) I1) is Element of the carrier of n

I1 -| A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

I1 |-- A is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

I2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng I2 is finite set

I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

rng I1 is finite set

I2 ^ I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

I1 - {A} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng (I2 ^ I1) is finite set

(Carrier W1) \ {A} is finite Element of K27( the carrier of n)

<*A*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

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

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

<*A*> ^ I1 is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

I2 ^ (<*A*> ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

W1 (#) I2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

W1 (#) (<*A*> ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) I2) ^ (W1 (#) (<*A*> ^ I1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

W1 (#) <*A*> is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

W1 (#) I1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) <*A*>) ^ (W1 (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) I2) ^ ((W1 (#) <*A*>) ^ (W1 (#) I1)) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) I2) ^ (W1 (#) <*A*>) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

((W1 (#) I2) ^ (W1 (#) <*A*>)) ^ (W1 (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 . A) * A is Element of the carrier of n

<*((W1 . A) * A)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V19() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) I2) ^ <*((W1 . A) * A)*> is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

((W1 (#) I2) ^ <*((W1 . A) * A)*>) ^ (W1 (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

<*((W1 . A) * A)*> ^ (W1 (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(W1 (#) I2) ^ (<*((W1 . A) * A)*> ^ (W1 (#) I1)) is Relation-like NAT -defined the carrier of n -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((W1 (#) I2) ^ (<*((W1 . A) * A)*> ^ (W1 (#) I1))) is Element of the carrier of n

Sum (W1 (#) I2) is Element of the carrier of n

Sum (<*((W1 . A) * A)*> ^ (W1 (#) I1)) is Element of the carrier of n

(Sum (W1 (#) I2)) + (Sum (<*((W1 . A) * A)*> ^ (W1 (#) I1))) is Element of the carrier of n

Sum <*((W1 . A) * A)*> is Element of the carrier of n

Sum (W1 (#) I1) is Element of the carrier of n

(Sum <*((W1 . A) * A)*>) + (Sum (W1 (#) I1)) is Element of the carrier of n

(Sum (W1 (#) I2)) + ((Sum <*((W1 . A) * A)*>) + (Sum (W1 (#) I1))) is Element of the carrier of n

(Sum (W1 (#) I1)) + ((W1 . A) * A) is Element of the carrier of n

(Sum (W1 (#) I2)) + ((Sum (W1 (#) I1)) + ((W1 . A) * A)) is Element of the carrier of n

(Sum (W1 (#) I2)) + (Sum (W1 (#) I1)) is Element of the carrier of n

((Sum (W1 (#) I2)) + (Sum (W1 (#) I1))) + ((W1 . A) * A) is Element of the carrier of n

(W1 (#) I2) ^ (W1 (#) I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum ((W1 (#) I2) ^ (W1 (#) I1)) is Element of the carrier of n

(Sum ((W1 (#) I2) ^ (W1 (#) I1))) + ((W1 . A) * A) is Element of the carrier of n

W1 (#) (I2 ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (W1 (#) (I2 ^ I1)) is Element of the carrier of n

(Sum (W1 (#) (I2 ^ I1))) + ((W1 . A) * A) is Element of the carrier of n

(rng (I2 ^ I1)) /\ (Carrier W1) is finite Element of K27( the carrier of n)

A is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier A is finite Element of K27( the carrier of n)

A (#) (I2 ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

(rng I1) \ {A} is finite Element of K27((rng I1))

K27((rng I1)) is non empty finite V28() set

(W1 . A) " is Element of the carrier of GF

A9 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of (V \/ W) \ {A}

- A9 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

(- A9) + W1 is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

((W1 . A) ") * ((- A9) + W1) is Relation-like the carrier of n -defined the carrier of GF -valued Function-like total quasi_total Linear_Combination of n

Carrier ((- A9) + W1) is finite Element of K27( the carrier of n)

Carrier (- A9) is finite Element of K27( the carrier of n)

Carrier W1 is finite Element of K27( the carrier of n)

(Carrier (- A9)) \/ (Carrier W1) is finite Element of K27( the carrier of n)

Carrier A9 is finite Element of K27( the carrier of n)

(Carrier A9) \/ (Carrier W1) is finite Element of K27( the carrier of n)

Carrier (((W1 . A) ") * ((- A9) + W1)) is finite Element of K27( the carrier of n)

A9 (#) (I2 ^ I1) is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n

Sum (A9 (#) (I2 ^ I1)) is Element of the carrier of n

Sum A9 is Element of the carrier of n

((W1 . A) ") * x is Element of the carrier of n

((W1 . A) ") * (Sum A9) is Element of the carrier of n

((W1 . A) ") * ((W1 . A) * A) is Element of the carrier of n

(((W1 . A) ") * (Sum A9)) + (((W1 . A) ") * ((W1 . A) * A)) is Element of the carrier of n

(((W1 . A) ") * (Sum A9)) + A is Element of the carrier of n

(((W1 . A) ") * x) - (((W1 . A) ") * (Sum A9)) is Element of the carrier of n

x - (Sum A9) is Element of the carrier of n

((W1 . A) ") * (x - (Sum A9)) is Element of the carrier of n

- (Sum A9) is Element of the carrier of n

(- (Sum A9)) + x is Element of the carrier of n

((W1 . A) ") * ((- (Sum A9)) + x) is Element of the carrier of n

Sum (- A9) is Element of the carrier of n

(Sum (- A9)) + (Sum W1) is Element of the carrier of n

((W1 . A) ") * ((Sum (- A9)) + (Sum W1)) is Element of the carrier of n

Sum ((- A9) + W1) is Element of the carrier of n

((W1 . A) ") * (Sum ((- A9) + W1)) is Element of the carrier of n

Sum (((W1 . A) ") * ((- A9) + W1)) is Element of the carrier of n

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

the U5 of n is Relation-like K28( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K27(K28(K28( the carrier of n, the carrier of n), the carrier of n))

K28( the carrier of n, the carrier of n) is Relation-like non empty set

K28(K28( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set

K27(K28(K28( the carrier of n, the carrier of n), the carrier of n)) is non empty set

the ZeroF of n is Element of the carrier of n

the lmult of n is Relation-like K28( the carrier of GF, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K27(K28(K28( the carrier of GF, the carrier of n), the carrier of n))

the carrier of GF is non empty V19() set

K28( the carrier of GF, the carrier of n) is Relation-like non empty set

K28(K28( the carrier of GF, the carrier of n), the carrier of n) is Relation-like non empty set

K27(K28(K28( the carrier of GF, the carrier of n), the carrier of n)) is non empty set

VectSpStr(# the carrier of n, the U5 of n, the ZeroF of n, the lmult of n #) is non empty strict VectSpStr over GF

V is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

V + 1 is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

W is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

W - (V + 1) is ext-real V38() V58() set

x is finite Element of K27( the carrier of n)

card x is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

W1 is finite Element of K27( the carrier of n)

card W1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

Lin x is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W1 is set

A is Element of the carrier of n

{A} is non empty V19() finite 1 -element Element of K27( the carrier of n)

W1 \ {A} is finite Element of K27( the carrier of n)

K27(W1) is non empty finite V28() set

card (W1 \ {A}) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

card {A} is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

(card W1) - (card {A}) is ext-real V38() V58() set

(V + 1) - 1 is ext-real V38() V58() set

W - V is ext-real V38() V58() set

I1 is finite Element of K27( the carrier of n)

card I1 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

(W1 \ {A}) \/ I1 is finite Element of K27( the carrier of n)

Lin ((W1 \ {A}) \/ I1) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

Lin (W1 \ {A}) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

V - V is ext-real V38() V58() set

I2 is finite Element of K27( the carrier of n)

card I2 is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

(W1 \ {A}) \/ I2 is finite Element of K27( the carrier of n)

Lin ((W1 \ {A}) \/ I2) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

I1 \/ (W1 \ {A}) is finite Element of K27( the carrier of n)

I2 is Element of the carrier of n

{I2} is non empty V19() finite 1 -element Element of K27( the carrier of n)

(I1 \/ (W1 \ {A})) \ {I2} is finite Element of K27( the carrier of n)

((I1 \/ (W1 \ {A})) \ {I2}) \/ {A} is non empty finite Element of K27( the carrier of n)

Lin (((I1 \/ (W1 \ {A})) \ {I2}) \/ {A}) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

I1 \ {I2} is finite Element of K27( the carrier of n)

(W1 \ {A}) \ {I2} is finite Element of K27( the carrier of n)

((W1 \ {A}) \ {I2}) \/ {A} is non empty finite Element of K27( the carrier of n)

(W1 \ {A}) \/ {A} is non empty finite Element of K27( the carrier of n)

(I1 \ {I2}) \/ (((W1 \ {A}) \ {I2}) \/ {A}) is non empty finite Element of K27( the carrier of n)

(I1 \ {I2}) \/ ((W1 \ {A}) \/ {A}) is non empty finite Element of K27( the carrier of n)

W1 \/ (I1 \ {I2}) is finite Element of K27( the carrier of n)

K27(I1) is non empty finite V28() set

card (I1 \ {I2}) is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

card {I2} is V6() V7() V8() V12() non empty finite cardinal ext-real positive non negative V38() V58() Element of NAT

(card I1) - (card {I2}) is ext-real V38() V58() set

(W - V) - 1 is ext-real V38() V58() set

(I1 \ {I2}) \/ ((W1 \ {A}) \ {I2}) is finite Element of K27( the carrier of n)

((I1 \ {I2}) \/ ((W1 \ {A}) \ {I2})) \/ {A} is non empty finite Element of K27( the carrier of n)

Lin (W1 \/ (I1 \ {I2})) is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

(I1 \ {I2}) \/ {I2} is non empty finite Element of K27( the carrier of n)

A is set

the carrier of (Lin (W1 \/ (I1 \ {I2}))) is non empty set

the carrier of (Lin ((W1 \ {A}) \/ I1)) is non empty set

V is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() set

V - 0 is ext-real non negative V38() V58() set

W is finite Element of K27( the carrier of n)

card W is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

x is finite Element of K27( the carrier of n)

card x is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

Lin W is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

x \/ W is finite Element of K27( the carrier of n)

V is finite Element of K27( the carrier of n)

Lin V is non empty V72() strict V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() Subspace of n

W is finite Element of K27( the carrier of n)

card W is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

card V is V6() V7() V8() V12() finite cardinal ext-real non negative V38() V58() Element of NAT

(card V) - (card W) is ext-real V38() V58() set

GF is non empty non degenerated V49() V72() V92() V96() V98() V100() right-distributive left-distributive right_unital well-unital V106() left_unital V116() V117() V118() L11()

n is non empty V72() V109(GF) V110(GF) V111(GF) V112(GF) V116() V117() V118() VectSpStr over GF

the carrier of n is non empty set

K27( the carrier of n) is non empty set

V is finite Element of K27( the carrier of n)

W is Basis of n

x is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set

rng x is finite set

the carrier of GF is non empty V19() set

W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n