:: RLVECT_5 semantic presentation

REAL is non empty V12() non finite V129() V130() V131() V135() set
NAT is non empty V12() V18() V19() V20() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() Element of K19(REAL)
K19(REAL) is non empty V12() non finite set
NAT is non empty V12() V18() V19() V20() non finite cardinal limit_cardinal V129() V130() V131() V132() V133() V134() V135() set
K19(NAT) is non empty V12() non finite set
K19(NAT) is non empty V12() non finite set
COMPLEX is non empty V12() non finite V129() V135() set
RAT is non empty V12() non finite V129() V130() V131() V132() V135() set
INT is non empty V12() non finite V129() V130() V131() V132() V133() V135() set
{} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() set
2 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
1 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
3 is non empty ext-real positive non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
0 is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty ext-real non negative V18() V19() V20() V22() V23() V24() V25() V26() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V117() V118() V129() V130() V131() V132() V133() V134() V135() Element of NAT
card {} is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() set
Seg 1 is non empty V12() finite 1 -element V129() V130() V131() V132() V133() V134() Element of K19(NAT)
0 " is V25() set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier V is finite Element of K19( the carrier of n)
Sum V is Element of the carrier of n
W is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier W is finite Element of K19( the carrier of n)
Sum W is Element of the carrier of n
x is Element of K19( the carrier of n)
(Carrier V) \/ (Carrier W) is finite Element of K19( the carrier of n)
(Sum V) - (Sum W) is Element of the carrier of n
- (Sum V) is Element of the carrier of n
(Sum V) + (- (Sum V)) is Element of the carrier of n
0. n is V64(n) Element of the carrier of n
V - W is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier (V - W) is finite Element of K19( the carrier of n)
Sum (V - W) is Element of the carrier of n
W1 is Element of the carrier of n
(V - W) . W1 is ext-real V25() V26() Element of REAL
V . W1 is ext-real V25() V26() Element of REAL
W . W1 is ext-real V25() V26() Element of REAL
(V . W1) - (W . W1) is ext-real V25() V26() Element of REAL
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Element of K19( the carrier of n)
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
W is Element of K19( the carrier of n)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is Basis of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier V is finite Element of K19( the carrier of n)
K19( the carrier of n) is non empty set
W is Element of the carrier of n
{ b₁ where b₁ is Element of the carrier of n : not V . b₁ = 0 } is set
x is Element of the carrier of n
V . x is ext-real V25() V26() Element of REAL
V is set
n is set
{V} is non empty V12() finite 1 -element set
n \ {V} is Element of K19(n)
K19(n) is non empty set
(n \ {V}) \/ {V} is non empty set
{V} \/ (n \ {V}) is non empty set
{V} \/ n is non empty set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is Relation-like the carrier of n -defined REAL -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 V129() V130() V131() V132() V133() V134() Element of K19(NAT)
K20((dom W),(dom W)) is Relation-like finite set
K19(K20((dom W),(dom W))) is non empty finite V37() 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 total quasi_total onto bijective finite Element of K19(K20((dom W),(dom W)))
W * A is Relation-like dom W -defined the carrier of n -valued Function-like finite Element of K19(K20((dom W), the carrier of n))
K20((dom W), the carrier of n) is Relation-like set
K19(K20((dom W), the carrier of n)) is non empty set
len x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len (V (#) W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom (V (#) W) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
(V (#) W) * A is Relation-like dom W -defined the carrier of n -valued Function-like finite Element of K19(K20((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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom B is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
len (V (#) x) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom (V (#) x) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
dom x is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
I1 is non negative V18() V19() V20() V24() finite cardinal 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W /. I1 is Element of the carrier of n
(V (#) x) . I1 is set
V . (W /. I1) is ext-real V25() V26() Element of REAL
(V . (W /. I1)) * (W /. I1) is Element of the carrier of n
(V (#) W) . (A . I1) is set
B . I1 is set
Sum B is Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
0. n is V64(n) Element of the carrier of n
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier V is finite Element of K19( the carrier of n)
K19( 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 V12() 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 V12() 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 K19( 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 V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
rng <*B*> is non empty V12() finite 1 -element set
(rng W1) \/ (rng <*B*>) is non empty finite set
(Carrier V) /\ ((rng W1) \/ (rng <*B*>)) is finite Element of K19( the carrier of n)
{B} is non empty V12() finite 1 -element Element of K19( the carrier of n)
(rng W1) \/ {B} is non empty finite set
(Carrier V) /\ ((rng W1) \/ {B}) is finite Element of K19( the carrier of n)
(Carrier V) /\ (rng W1) is finite Element of K19( the carrier of n)
(Carrier V) /\ {B} is finite Element of K19( the carrier of n)
((Carrier V) /\ (rng W1)) \/ ((Carrier V) /\ {B}) is finite Element of K19( 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 ext-real V25() V26() Element of REAL
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 V12() 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 * 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 Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() FinSequence of the carrier of n
K20(NAT, the carrier of n) is Relation-like non empty V12() 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
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
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
K19((rng V)) is non empty finite V37() set
x is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier x is finite Element of K19( the carrier of n)
K19( 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 K19((rng V))
W1 ` is finite Element of K19((rng V))
V - (W1 `) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
W is finite Element of K19((rng V))
W \ (W1 `) is finite Element of K19((rng V))
(W1 `) ` is finite Element of K19((rng V))
W /\ ((W1 `) `) is finite Element of K19((rng V))
rng (V - (W1 `)) is finite set
dom W1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
K20((dom W1),(dom W1)) is Relation-like finite set
K19(K20((dom W1),(dom W1))) is non empty finite V37() set
V - W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
(rng V) \ (rng W1) is finite Element of K19((rng 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
rng I1 is finite set
(rng I1) /\ (rng W1) is finite set
((rng V) \ (rng W1)) /\ (rng W1) is finite Element of K19((rng V))
dom V is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
K20((dom V),(dom V)) is Relation-like finite set
K19(K20((dom V),(dom V))) is non empty finite V37() 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 V64(n) 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 total quasi_total onto bijective finite Element of K19(K20((dom V),(dom V)))
V * I2 is Relation-like dom V -defined the carrier of n -valued Function-like finite Element of K19(K20((dom V), the carrier of n))
K20((dom V), the carrier of n) is Relation-like set
K19(K20((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 total quasi_total onto bijective finite Element of K19(K20((dom W1),(dom W1)))
W1 * I2 is Relation-like dom W1 -defined the carrier of n -valued Function-like finite Element of K19(K20((dom W1), the carrier of n))
K20((dom W1), the carrier of n) is Relation-like set
K19(K20((dom W1), the carrier of n)) is non empty set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier V is finite Element of K19( the carrier of n)
K19( 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 K19( 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
W1 is set
V . W1 is set
W1 is Element of the carrier of n
V . W1 is ext-real V25() V26() Element of REAL
K20( the carrier of n,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of n,REAL)) is non empty V12() non finite set
W1 is Relation-like the carrier of n -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of n,REAL))
W1 is Relation-like the carrier of n -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of n,REAL))
W1 is Element of the carrier of n
x is finite Element of K19( the carrier of n)
x /\ (Carrier V) is finite Element of K19( the carrier of n)
W1 . W1 is ext-real V25() V26() Element of REAL
V . W1 is ext-real V25() V26() Element of REAL
W1 . W1 is ext-real V25() V26() Element of REAL
Funcs ( the carrier of n,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of n, REAL
W1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Element of Funcs ( the carrier of n,REAL)
B is set
I1 is Element of the carrier of n
V . I1 is ext-real V25() V26() Element of REAL
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
A . I1 is ext-real V25() V26() Element of REAL
{ b₁ where b₁ is Element of the carrier of n : not A . b₁ = 0 } is set
Carrier A is finite Element of K19( 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len (A (#) W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom (V (#) W) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
dom (A (#) W) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
dom W is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
I2 is non negative V18() V19() V20() V24() finite cardinal set
W /. I2 is Element of the carrier of n
A . (W /. I2) is ext-real V25() V26() Element of REAL
V . (W /. I2) is set
W . I2 is set
(V (#) W) . I2 is set
V . (W /. I2) is ext-real V25() V26() Element of REAL
(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 ext-real V25() V26() Element of REAL
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
W is Element of K19( the carrier of n)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of (Lin W) is non empty set
x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x + 1 is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 V12() 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 V12() finite 1 -element set
(rng B) \/ (rng <*A*>) is non empty finite set
{A} is non empty V12() finite 1 -element set
(rng B) \/ {A} is non empty finite set
I2 is Relation-like the carrier of n -defined REAL -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 V12() 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 non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len B is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len <*I1*> is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(len B) + (len <*I1*>) is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(len B) + 1 is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 REAL -valued Function-like total quasi_total Linear_Combination of W
Sum A is Element of the carrier of n
V . I1 is ext-real V25() V26() Element of REAL
(V . I1) * I2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
A + ((V . I1) * I2) is Relation-like the carrier of n -defined REAL -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 V12() 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() FinSequence of the carrier of n
K20(NAT, the carrier of n) is Relation-like non empty V12() non finite set
0. n is V64(n) Element of the carrier of n
ZeroLC n is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Sum (ZeroLC n) is Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier V is finite Element of K19( the carrier of n)
Sum V is Element of the carrier of n
W is Element of K19( the carrier of n)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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 REAL -valued Function-like total quasi_total Linear_Combination of W
Sum W1 is Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
W is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier W is finite Element of K19( the carrier of n)
K19( 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 REAL -valued Function-like Element of K19(K20( the carrier of n,REAL))
K20( the carrier of n,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of n,REAL)) is non empty V12() non finite set
Sum W is Element of the carrier of n
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier x is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
Sum x is Element of the carrier of V
dom x is set
W1 is set
W1 is Element of the carrier of V
x . W1 is ext-real V25() V26() Element of REAL
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 ext-real V25() V26() Element of REAL
x . B is set
dom W1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
K20((dom W1),(dom W1)) is Relation-like finite set
K19(K20((dom W1),(dom W1))) is non empty finite V37() set
A is Relation-like dom W1 -defined dom W1 -valued Function-like one-to-one total quasi_total onto bijective finite Element of K19(K20((dom W1),(dom W1)))
W1 * A is Relation-like dom W1 -defined the carrier of V -valued Function-like finite Element of K19(K20((dom W1), the carrier of V))
K20((dom W1), the carrier of V) is Relation-like set
K19(K20((dom W1), the carrier of V)) is non empty set
len (x (#) W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
len W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom (x (#) W1) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
(x (#) W1) * A is Relation-like dom W1 -defined the carrier of V -valued Function-like finite Element of K19(K20((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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom B is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
rng B is finite set
K20(NAT, the carrier of V) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of V)) is non empty V12() non finite set
Sum B is Element of the carrier of V
0. V is V64(V) 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 K19(K20(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
K20(NAT, the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(NAT, the carrier of n)) is non empty V12() 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
A is Relation-like NAT -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(NAT, the carrier of n))
A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
A + 1 is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom W1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
len (W (#) W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
dom (W (#) W1) is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
A is non negative V18() V19() V20() V24() finite cardinal 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() 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 ext-real V25() V26() Element of REAL
(x . w1) * w1 is Element of the carrier of V
W . (W1 /. A) is ext-real V25() V26() Element of REAL
(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
K20((dom (x (#) W1)),(dom (x (#) W1))) is Relation-like finite set
K19(K20((dom (x (#) W1)),(dom (x (#) W1)))) is non empty finite V37() set
A is Relation-like dom (x (#) W1) -defined dom (x (#) W1) -valued Function-like one-to-one total quasi_total onto bijective finite Element of K19(K20((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 K19(K20((dom (x (#) W1)), the carrier of V))
K20((dom (x (#) W1)), the carrier of V) is Relation-like set
K19(K20((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 V64(n) Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
W is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
Sum W is Element of the carrier of V
K20( the carrier of V,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of V,REAL)) is non empty V12() non finite set
K19( 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 ext-real V25() V26() Element of REAL
W . B is set
A is Element of the carrier of n
A is Element of the carrier of n
K20( the carrier of n,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of n,REAL)) is non empty V12() non finite set
W1 is Relation-like the carrier of n -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of n,REAL))
W1 is Relation-like the carrier of n -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of n,REAL))
A is Element of the carrier of n
W1 is finite Element of K19( the carrier of n)
W . A is set
W1 . A is ext-real V25() V26() Element of REAL
Funcs ( the carrier of n,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of n, REAL
A is Relation-like the carrier of n -defined REAL -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 REAL -valued Function-like Element of K19(K20( the carrier of n,REAL))
Carrier A is finite Element of K19( 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 ext-real V25() V26() Element of REAL
W . I2 is set
I1 is set
A . I1 is set
W . I1 is set
x is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of V,REAL))
x . I1 is set
B is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of V,REAL))
B . I1 is set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
W is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier W is finite Element of K19( the carrier of n)
K19( the carrier of n) is non empty set
Sum W is Element of the carrier of n
K19( the carrier of V) is non empty set
K20( the carrier of V,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of V,REAL)) is non empty V12() non finite set
W | the carrier of V is Relation-like the carrier of n -defined the carrier of V -defined the carrier of n -defined REAL -valued Function-like Element of K19(K20( the carrier of n,REAL))
K20( the carrier of n,REAL) is Relation-like non empty V12() non finite set
K19(K20( the carrier of n,REAL)) is non empty V12() non finite set
W1 is Relation-like the carrier of V -defined REAL -valued Function-like non empty total quasi_total Element of K19(K20( the carrier of V,REAL))
Funcs ( the carrier of V,REAL) is functional non empty FUNCTION_DOMAIN of the carrier of V, REAL
dom W1 is non empty set
W1 is Element of the carrier of V
x is finite Element of K19( the carrier of V)
W . W1 is set
W1 . W1 is ext-real V25() V26() Element of REAL
W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W1 is finite Element of K19( the carrier of V)
Sum W1 is Element of the carrier of V
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
V is Basis of n
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
W is Element of the carrier of n
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
K19( the carrier of V) is non empty set
W is Element of K19( the carrier of V)
x is Element of K19( the carrier of n)
0. n is V64(n) Element of the carrier of n
W1 is Relation-like the carrier of n -defined REAL -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 K19( the carrier of n)
W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W1 is finite Element of K19( the carrier of V)
Sum W1 is Element of the carrier of V
A is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Sum A is Element of the carrier of V
0. V is V64(V) Element of the carrier of V
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
K19( the carrier of V) is non empty set
W is Element of K19( the carrier of n)
x is Element of K19( the carrier of V)
0. V is V64(V) Element of the carrier of V
W1 is Relation-like the carrier of V -defined REAL -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 K19( the carrier of V)
W1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier W1 is finite Element of K19( the carrier of n)
Sum W1 is Element of the carrier of n
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Sum A is Element of the carrier of n
0. n is V64(n) Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
W is Basis of V
the carrier of n is non empty set
K19( the carrier of n) is non empty set
x is Basis of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Element of K19( the carrier of n)
W is Element of the carrier of n
{W} is non empty V12() finite 1 -element Element of K19( the carrier of n)
V \ {W} is Element of K19( the carrier of n)
K19(V) is non empty set
Lin {W} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of {W}
Sum x is Element of the carrier of n
W1 is Element of K19( the carrier of n)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
W1 \/ {W} is non empty Element of K19( the carrier of n)
V \/ V is Element of K19( the carrier of n)
W1 is Relation-like the carrier of n -defined REAL -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 K19( the carrier of n)
Carrier x is finite Element of K19( the carrier of n)
(Carrier W1) \/ (Carrier x) is finite Element of K19( the carrier of n)
W1 - x is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier (W1 - x) is finite Element of K19( the carrier of n)
A is Element of the carrier of n
x . A is ext-real V25() V26() Element of REAL
A is set
B is Element of the carrier of n
W1 . B is ext-real V25() V26() Element of REAL
(W1 - x) . B is ext-real V25() V26() Element of REAL
x . B is ext-real V25() V26() Element of REAL
(W1 . B) - (x . B) is ext-real V25() V26() Element of REAL
(W1 . B) - 0 is ext-real V25() V26() Element of REAL
0. n is V64(n) 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 REAL -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 REAL -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
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Basis of n
W is non empty Element of K19( the carrier of n)
V \/ W is non empty Element of K19( the carrier of n)
x is set
W1 is Element of K19( the carrier of n)
W1 is Element of the carrier of n
{W1} is non empty V12() finite 1 -element Element of K19( the carrier of n)
W1 \ {W1} is Element of K19( the carrier of n)
V \ {W1} is Element of K19( the carrier of n)
A is Element of K19( the carrier of n)
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
Lin A is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
W is Element of K19( the carrier of n)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is set
the carrier of (Lin W) is non empty set
W1 is Relation-like the carrier of n -defined REAL -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 K19( the carrier of n)
W1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier W1 is finite Element of K19( the carrier of V)
K19( the carrier of V) is non empty set
Sum W1 is Element of the carrier of V
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the carrier of V is non empty set
K19( the carrier of V) is non empty set
W is Element of K19( the carrier of n)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is Element of K19( the carrier of V)
Lin x is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
W1 is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
W1 is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
A is set
the carrier of (Lin W) is non empty set
B is Relation-like the carrier of n -defined REAL -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 K19( the carrier of n)
I1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Carrier I1 is finite Element of K19( the carrier of V)
Sum I1 is Element of the carrier of V
I2 is Relation-like the carrier of V -defined REAL -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 REAL -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 K19( the carrier of V)
I1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier I1 is finite Element of K19( the carrier of n)
Sum I1 is Element of the carrier of n
I2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Sum I2 is Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
W is finite Element of K19( the carrier of n)
V \/ W is finite Element of K19( the carrier of n)
Lin (V \/ W) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is Element of the carrier of n
{x} is non empty V12() finite 1 -element Element of K19( the carrier of n)
W1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of V \/ W
Sum W1 is Element of the carrier of n
Carrier W1 is finite Element of K19( the carrier of n)
W1 is set
A is Element of the carrier of n
W1 . A is ext-real V25() V26() Element of REAL
W1 is Element of the carrier of n
W1 . W1 is ext-real V25() V26() Element of REAL
W1 is Element of the carrier of n
W1 . W1 is ext-real V25() V26() Element of REAL
{W1} is non empty V12() finite 1 -element Element of K19( the carrier of n)
(V \/ W) \ {W1} is finite Element of K19( the carrier of n)
((V \/ W) \ {W1}) \/ {x} is non empty finite Element of K19( the carrier of n)
Lin (((V \/ W) \ {W1}) \/ {x}) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace 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
rng B is finite set
W1 (#) 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 (W1 (#) B) is Element of the carrier of n
B -| W1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
B |-- 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
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 ^ I2 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
B - {W1} is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
rng (I1 ^ I2) is finite set
(Carrier W1) \ {W1} is finite Element of K19( the carrier of n)
<*W1*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(B -| W1) ^ <*W1*> is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
((B -| W1) ^ <*W1*>) ^ (B |-- W1) is Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like set
<*W1*> ^ I2 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
I1 ^ (<*W1*> ^ I2) 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 (#) 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 (#) (<*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 (#) I1) ^ (W1 (#) (<*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 (#) <*W1*> 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 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(W1 (#) <*W1*>) ^ (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 (#) I1) ^ ((W1 (#) <*W1*>) ^ (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 (#) I1) ^ (W1 (#) <*W1*>) 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) ^ (W1 (#) <*W1*>)) ^ (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 . W1) * W1 is Element of the carrier of n
<*((W1 . W1) * W1)*> is Relation-like NAT -defined the carrier of n -valued Function-like constant non empty V12() finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of n
(W1 (#) I1) ^ <*((W1 . W1) * W1)*> 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 (#) I1) ^ <*((W1 . W1) * W1)*>) ^ (W1 (#) I2) 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 . W1) * W1)*> ^ (W1 (#) I2) 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 (#) I1) ^ (<*((W1 . W1) * W1)*> ^ (W1 (#) I2)) 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 (#) I1) ^ (<*((W1 . W1) * W1)*> ^ (W1 (#) I2))) is Element of the carrier of n
Sum (W1 (#) I1) is Element of the carrier of n
Sum (<*((W1 . W1) * W1)*> ^ (W1 (#) I2)) is Element of the carrier of n
(Sum (W1 (#) I1)) + (Sum (<*((W1 . W1) * W1)*> ^ (W1 (#) I2))) is Element of the carrier of n
Sum <*((W1 . W1) * W1)*> is Element of the carrier of n
Sum (W1 (#) I2) is Element of the carrier of n
(Sum <*((W1 . W1) * W1)*>) + (Sum (W1 (#) I2)) is Element of the carrier of n
(Sum (W1 (#) I1)) + ((Sum <*((W1 . W1) * W1)*>) + (Sum (W1 (#) I2))) is Element of the carrier of n
(Sum (W1 (#) I2)) + ((W1 . W1) * W1) is Element of the carrier of n
(Sum (W1 (#) I1)) + ((Sum (W1 (#) I2)) + ((W1 . W1) * W1)) is Element of the carrier of n
(Sum (W1 (#) I1)) + (Sum (W1 (#) I2)) is Element of the carrier of n
((Sum (W1 (#) I1)) + (Sum (W1 (#) I2))) + ((W1 . W1) * W1) is Element of the carrier of n
(W1 (#) I1) ^ (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
Sum ((W1 (#) I1) ^ (W1 (#) I2)) is Element of the carrier of n
(Sum ((W1 (#) I1) ^ (W1 (#) I2))) + ((W1 . W1) * W1) is Element of the carrier of n
W1 (#) (I1 ^ I2) 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 ^ I2)) is Element of the carrier of n
(Sum (W1 (#) (I1 ^ I2))) + ((W1 . W1) * W1) is Element of the carrier of n
Lin {x} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of {x}
Sum A is Element of the carrier of n
(rng (I1 ^ I2)) /\ (Carrier W1) is finite Element of K19( the carrier of n)
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier A is finite Element of K19( the carrier of n)
A (#) (I1 ^ 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 B) \ {W1} is finite Element of K19((rng B))
K19((rng B)) is non empty finite V37() set
(W1 . W1) " is ext-real V25() V26() Element of REAL
A9 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of (V \/ W) \ {W1}
- A9 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
(- A9) + A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
((W1 . W1) ") * ((- A9) + A) is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of n
Carrier (((W1 . W1) ") * ((- A9) + A)) is finite Element of K19( the carrier of n)
Carrier ((- A9) + A) is finite Element of K19( the carrier of n)
Carrier (- A9) is finite Element of K19( the carrier of n)
Carrier A is finite Element of K19( the carrier of n)
(Carrier (- A9)) \/ (Carrier A) is finite Element of K19( the carrier of n)
Carrier A9 is finite Element of K19( the carrier of n)
(Carrier A9) \/ (Carrier A) is finite Element of K19( the carrier of n)
A9 (#) (I1 ^ I2) 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 (#) (I1 ^ I2)) is Element of the carrier of n
Sum A9 is Element of the carrier of n
((W1 . W1) ") * x is Element of the carrier of n
((W1 . W1) ") * (Sum A9) is Element of the carrier of n
((W1 . W1) ") * ((W1 . W1) * W1) is Element of the carrier of n
(((W1 . W1) ") * (Sum A9)) + (((W1 . W1) ") * ((W1 . W1) * W1)) is Element of the carrier of n
((W1 . W1) ") * (W1 . W1) is ext-real V25() V26() Element of REAL
(((W1 . W1) ") * (W1 . W1)) * W1 is Element of the carrier of n
(((W1 . W1) ") * (Sum A9)) + ((((W1 . W1) ") * (W1 . W1)) * W1) is Element of the carrier of n
1 * W1 is Element of the carrier of n
(((W1 . W1) ") * (Sum A9)) + (1 * W1) is Element of the carrier of n
(((W1 . W1) ") * (Sum A9)) + W1 is Element of the carrier of n
(((W1 . W1) ") * x) - (((W1 . W1) ") * (Sum A9)) is Element of the carrier of n
x - (Sum A9) is Element of the carrier of n
((W1 . W1) ") * (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 . W1) ") * ((- (Sum A9)) + x) is Element of the carrier of n
Sum (- A9) is Element of the carrier of n
(Sum (- A9)) + (Sum A) is Element of the carrier of n
((W1 . W1) ") * ((Sum (- A9)) + (Sum A)) is Element of the carrier of n
Sum ((- A9) + A) is Element of the carrier of n
((W1 . W1) ") * (Sum ((- A9) + A)) is Element of the carrier of n
Sum (((W1 . W1) ") * ((- A9) + A)) is Element of the carrier of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V + 1 is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W - (V + 1) is ext-real V25() V26() Element of REAL
x is finite Element of K19( the carrier of n)
card x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is finite Element of K19( the carrier of n)
card W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Lin x is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
W1 is set
A is Element of the carrier of n
{A} is non empty V12() finite 1 -element Element of K19( the carrier of n)
W1 \ {A} is finite Element of K19( the carrier of n)
K19(W1) is non empty finite V37() set
card (W1 \ {A}) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card {A} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(card W1) - (card {A}) is set
(V + 1) - 1 is ext-real V25() V26() Element of REAL
W - V is ext-real V25() V26() Element of REAL
I1 is finite Element of K19( the carrier of n)
card I1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(W1 \ {A}) \/ I1 is finite Element of K19( the carrier of n)
Lin ((W1 \ {A}) \/ I1) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
Lin (W1 \ {A}) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
V - V is ext-real V25() V26() Element of REAL
I2 is finite Element of K19( the carrier of n)
card I2 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(W1 \ {A}) \/ I2 is finite Element of K19( the carrier of n)
Lin ((W1 \ {A}) \/ I2) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
I1 \/ (W1 \ {A}) is finite Element of K19( the carrier of n)
I2 is Element of the carrier of n
{I2} is non empty V12() finite 1 -element Element of K19( the carrier of n)
(I1 \/ (W1 \ {A})) \ {I2} is finite Element of K19( the carrier of n)
((I1 \/ (W1 \ {A})) \ {I2}) \/ {A} is non empty finite Element of K19( the carrier of n)
Lin (((I1 \/ (W1 \ {A})) \ {I2}) \/ {A}) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
I1 \ {I2} is finite Element of K19( the carrier of n)
(W1 \ {A}) \ {I2} is finite Element of K19( the carrier of n)
((W1 \ {A}) \ {I2}) \/ {A} is non empty finite Element of K19( the carrier of n)
(W1 \ {A}) \/ {A} is non empty finite Element of K19( the carrier of n)
(I1 \ {I2}) \/ (((W1 \ {A}) \ {I2}) \/ {A}) is non empty finite Element of K19( the carrier of n)
(I1 \ {I2}) \/ ((W1 \ {A}) \/ {A}) is non empty finite Element of K19( the carrier of n)
W1 \/ (I1 \ {I2}) is finite Element of K19( the carrier of n)
K19(I1) is non empty finite V37() set
card (I1 \ {I2}) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card {I2} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(card I1) - (card {I2}) is set
(W - V) - 1 is ext-real V25() V26() Element of REAL
(I1 \ {I2}) \/ ((W1 \ {A}) \ {I2}) is finite Element of K19( the carrier of n)
((I1 \ {I2}) \/ ((W1 \ {A}) \ {I2})) \/ {A} is non empty finite Element of K19( the carrier of n)
Lin (W1 \/ (I1 \ {I2})) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
(I1 \ {I2}) \/ {I2} is non empty finite Element of K19( 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 ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V - 0 is ext-real V25() V26() Element of REAL
W is finite Element of K19( the carrier of n)
card W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is finite Element of K19( the carrier of n)
card x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x \/ W is finite Element of K19( the carrier of n)
V is finite Element of K19( the carrier of n)
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
W is finite Element of K19( the carrier of n)
card W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(card V) - (card W) is set
the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is non empty set
K19( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) is non empty set
{} the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() Element of K19( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ))
V is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() Element of K19( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ))
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of (0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(0). ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of (0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the ZeroF of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is Element of the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )
the U5 of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is Relation-like K20( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) -defined the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )))
K20( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) is Relation-like non empty set
K20(K20( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) is Relation-like non empty set
K19(K20(K20( the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ))) is non empty set
the Mult of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) is Relation-like K20(REAL, the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) -defined the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )))
K20(REAL, the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct )), the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ))) is non empty V12() non finite set
RLSStruct(# the carrier of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the ZeroF of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the U5 of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ), the Mult of ((0). the non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ) #) is strict RLSStruct
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is finite Element of K19( 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
W1 is Relation-like NAT -defined the carrier of n -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of n
dom W1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
{ (Carrier b₁) where b₁ is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W : ex b₂ being ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT st
( b₂ in dom W1 & Sum b₁ = W1 . b₂ ) } is set
union { (Carrier b₁) where b₁ is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W : ex b₂ being ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT st
( b₂ in dom W1 & Sum b₁ = W1 . b₂ ) } is set
B is set
I1 is set
I2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier I2 is finite Element of K19( the carrier of n)
I1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Sum I2 is Element of the carrier of n
W1 . I1 is set
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
B is Element of K19( the carrier of n)
Lin B is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
I1 is Element of the carrier of n
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
I2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of V
Sum I2 is Element of the carrier of n
Carrier I2 is finite Element of K19( the carrier of n)
the carrier of (Lin B) is non empty set
I1 is set
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
A is Element of the carrier of n
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Sum A is Element of the carrier of n
Carrier A is finite Element of K19( the carrier of n)
A9 is set
W1 . A9 is set
A9 is set
I1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of B
Sum I1 is Element of the carrier of n
the carrier of RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is set
the carrier of ((Omega). n) is non empty set
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
W \ B is Element of K19( the carrier of n)
I1 is set
I1 is Element of K19( the carrier of n)
I1 \ B is Element of K19( the carrier of n)
B \/ (I1 \ B) is Element of K19( the carrier of n)
B \/ I1 is Element of K19( the carrier of n)
I2 is non empty Element of K19( the carrier of n)
B \/ I2 is non empty Element of K19( the carrier of n)
len W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Seg (len W1) is finite len W1 -element V129() V130() V131() V132() V133() V134() Element of K19(NAT)
I1 is non negative V18() V19() V20() V24() finite cardinal set
W1 . I1 is set
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
I2 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Sum I2 is Element of the carrier of n
Carrier I2 is finite Element of K19( the carrier of n)
I1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier I1 is finite Element of K19( the carrier of n)
Sum I1 is Element of the carrier of n
I1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom I1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
I1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
dom I1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
I2 is non negative V18() V19() V20() V24() finite cardinal set
W1 . I2 is set
I1 is set
A is set
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier A is finite Element of K19( the carrier of n)
Sum A is Element of the carrier of n
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier A is finite Element of K19( the carrier of n)
Sum A is Element of the carrier of n
A9 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier A9 is finite Element of K19( the carrier of n)
Sum A9 is Element of the carrier of n
A9 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier A9 is finite Element of K19( the carrier of n)
Sum A9 is Element of the carrier of n
I2 is set
I1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier I1 is finite Element of K19( the carrier of n)
Sum I1 is Element of the carrier of n
A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 . A is set
A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 . A is set
I1 . A is set
A is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier A is finite Element of K19( the carrier of n)
Sum A is Element of the carrier of n
rng I1 is finite set
I2 is set
I1 is Relation-like the carrier of n -defined REAL -valued Function-like total quasi_total Linear_Combination of W
Carrier I1 is finite Element of K19( the carrier of n)
A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Sum I1 is Element of the carrier of n
W1 . A is set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Element of K19( the carrier of n)
W is Basis of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
V is Basis of n
card V is V18() V19() V20() cardinal set
W is Basis of n
card W is V18() V19() V20() cardinal set
the carrier of n is non empty set
K19( the carrier of n) is non empty set
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
x is finite Element of K19( the carrier of n)
card x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is finite Element of K19( the carrier of n)
card W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(0). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K19( the carrier of V) is non empty set
{} the carrier of V is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() Element of K19( the carrier of V)
the carrier of n is non empty set
0. n is V64(n) Element of the carrier of n
{(0. n)} is non empty V12() finite 1 -element Element of K19( the carrier of n)
K19( the carrier of n) is non empty set
0. V is V64(V) Element of the carrier of V
{(0. V)} is non empty V12() finite 1 -element Element of K19( the carrier of V)
(0). V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
the carrier of ((0). V) is non empty set
W is finite Element of K19( the carrier of V)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of V
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
the Basis of V is Basis of V
x is Basis of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
(0). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(0). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
card V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is Basis of n
card x is V18() V19() V20() cardinal set
V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
K19( the carrier of n) is non empty set
x is finite Element of K19( the carrier of n)
card x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the Basis of W is Basis of W
the carrier of n is non empty set
K19( the carrier of n) is non empty set
the Basis of V is Basis of V
the carrier of V is non empty set
K19( the carrier of V) is non empty set
A is Element of K19( the carrier of V)
W1 is finite Element of K19( the carrier of n)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
the carrier of W is non empty set
the ZeroF of W is Element of the carrier of W
the U5 of W is Relation-like K20( the carrier of W, the carrier of W) -defined the carrier of W -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of W, the carrier of W), the carrier of W))
K20( the carrier of W, the carrier of W) is Relation-like non empty set
K20(K20( the carrier of W, the carrier of W), the carrier of W) is Relation-like non empty set
K19(K20(K20( the carrier of W, the carrier of W), the carrier of W)) is non empty set
the Mult of W is Relation-like K20(REAL, the carrier of W) -defined the carrier of W -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of W), the carrier of W))
K20(REAL, the carrier of W) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of W), the carrier of W) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of W), the carrier of W)) is non empty V12() non finite set
RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) is strict RLSStruct
B is finite Element of K19( the carrier of n)
card B is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card A is V18() V19() V20() cardinal set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is Element of K19( the carrier of n)
card V is V18() V19() V20() cardinal set
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
((Lin V)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is set
the carrier of (Lin V) is non empty set
K19( the carrier of (Lin V)) is non empty set
x is linearly-independent Element of K19( the carrier of (Lin V))
Lin x is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of Lin V
W1 is Basis of Lin V
card W1 is V18() V19() V20() cardinal set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(((Omega). n)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(Omega). V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
the carrier of n is non empty set
K19( the carrier of n) is non empty set
W is finite Element of K19( the carrier of n)
the Basis of V is Basis of V
W1 is Basis of n
the carrier of V is non empty set
card the Basis of V is V18() V19() V20() cardinal set
card W1 is V18() V19() V20() cardinal set
A is finite Element of K19( the carrier of n)
card A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is finite Element of K19( the carrier of n)
card W1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
K19( the carrier of V) is non empty set
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
B is Element of K19( the carrier of n)
Lin B is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
I1 is Element of K19( the carrier of V)
Lin I1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
the ZeroF of V is Element of the carrier of V
the U5 of V is Relation-like K20( the carrier of V, the carrier of V) -defined the carrier of V -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of V, the carrier of V), the carrier of V))
K20( the carrier of V, the carrier of V) is Relation-like non empty set
K20(K20( the carrier of V, the carrier of V), the carrier of V) is Relation-like non empty set
K19(K20(K20( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is Relation-like K20(REAL, the carrier of V) -defined the carrier of V -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of V), the carrier of V))
K20(REAL, the carrier of V) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of V), the carrier of V) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of V), the carrier of V)) is non empty V12() non finite set
RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) is strict RLSStruct
x is finite Element of K19( the carrier of V)
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
Lin x is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
W1 is Element of K19( the carrier of n)
card W1 is V18() V19() V20() cardinal set
W1 is Element of K19( the carrier of V)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
((Lin W1)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card W1 is V18() V19() V20() cardinal set
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(0). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
the carrier of n is non empty set
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
W is finite Element of K19( the carrier of n)
card W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
{} the carrier of n is Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional empty proper non negative V18() V19() V20() V22() V23() V24() finite finite-yielding V37() cardinal {} -element FinSequence-like FinSubsequence-like FinSequence-membered V129() V130() V131() V132() V133() V134() V135() Element of K19( the carrier of n)
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
Lin W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
0. n is V64(n) Element of the carrier of n
{(0. n)} is non empty V12() finite 1 -element Element of K19( the carrier of n)
Lin V is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
0. n is V64(n) Element of the carrier of n
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
card V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is set
{W} is non empty V12() finite 1 -element set
x is Element of the carrier of n
{x} is non empty V12() finite 1 -element Element of K19( the carrier of n)
Lin {x} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
V is Element of the carrier of n
{V} is non empty V12() finite 1 -element Element of K19( the carrier of n)
Lin {V} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card {V} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
K19( the carrier of n) is non empty set
V is finite Element of K19( the carrier of n)
card V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is set
x is Element of the carrier of n
{x} is non empty V12() finite 1 -element Element of K19( the carrier of n)
card {x} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is set
W1 is Element of the carrier of n
{x,W1} is non empty finite Element of K19( the carrier of n)
A is set
{x,W1,A} is non empty finite set
B is set
card {x,W1,A} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
A is set
Lin {x,W1} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
V is Element of the carrier of n
W is Element of the carrier of n
{V,W} is non empty finite Element of K19( the carrier of n)
Lin {V,W} is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card {V,W} is non empty ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
V + W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
((V + W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V /\ W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
((V /\ W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((V + W)) + ((V /\ W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(V) + (W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
W1 is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
W1 is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
W1 /\ W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
the carrier of (W1 /\ W1) is non empty set
K19( the carrier of (W1 /\ W1)) is non empty set
A is finite Element of K19( the carrier of (W1 /\ W1))
B is Basis of W1
I1 is Basis of W1
the carrier of W1 is non empty set
K19( the carrier of W1) is non empty set
the carrier of W1 is non empty set
K19( the carrier of W1) is non empty set
I1 is finite Element of K19( the carrier of W1)
the carrier of x is non empty set
K19( the carrier of x) is non empty set
I2 is finite Element of K19( the carrier of W1)
I1 /\ I2 is finite Element of K19( the carrier of W1)
A is set
Lin I1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1
the ZeroF of W1 is Element of the carrier of W1
the U5 of W1 is Relation-like K20( the carrier of W1, the carrier of W1) -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of W1, the carrier of W1), the carrier of W1))
K20( the carrier of W1, the carrier of W1) is Relation-like non empty set
K20(K20( the carrier of W1, the carrier of W1), the carrier of W1) is Relation-like non empty set
K19(K20(K20( the carrier of W1, the carrier of W1), the carrier of W1)) is non empty set
the Mult of W1 is Relation-like K20(REAL, the carrier of W1) -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of W1), the carrier of W1))
K20(REAL, the carrier of W1) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of W1), the carrier of W1) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of W1), the carrier of W1)) is non empty V12() non finite set
RLSStruct(# the carrier of W1, the ZeroF of W1, the U5 of W1, the Mult of W1 #) is strict RLSStruct
x is set
{A} is non empty V12() finite 1 -element set
A \/ {A} is non empty finite set
w1 is set
A is linearly-independent Element of K19( the carrier of x)
x is Element of K19( the carrier of x)
A9 is Element of the carrier of x
Lin I2 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1
the ZeroF of W1 is Element of the carrier of W1
the U5 of W1 is Relation-like K20( the carrier of W1, the carrier of W1) -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of W1, the carrier of W1), the carrier of W1))
K20( the carrier of W1, the carrier of W1) is Relation-like non empty set
K20(K20( the carrier of W1, the carrier of W1), the carrier of W1) is Relation-like non empty set
K19(K20(K20( the carrier of W1, the carrier of W1), the carrier of W1)) is non empty set
the Mult of W1 is Relation-like K20(REAL, the carrier of W1) -defined the carrier of W1 -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of W1), the carrier of W1))
K20(REAL, the carrier of W1) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of W1), the carrier of W1) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of W1), the carrier of W1)) is non empty V12() non finite set
RLSStruct(# the carrier of W1, the ZeroF of W1, the U5 of W1, the Mult of W1 #) is strict RLSStruct
the carrier of W1 /\ the carrier of W1 is set
the ZeroF of (W1 /\ W1) is Element of the carrier of (W1 /\ W1)
the U5 of (W1 /\ W1) is Relation-like K20( the carrier of (W1 /\ W1), the carrier of (W1 /\ W1)) -defined the carrier of (W1 /\ W1) -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of (W1 /\ W1), the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1)))
K20( the carrier of (W1 /\ W1), the carrier of (W1 /\ W1)) is Relation-like non empty set
K20(K20( the carrier of (W1 /\ W1), the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1)) is Relation-like non empty set
K19(K20(K20( the carrier of (W1 /\ W1), the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1))) is non empty set
the Mult of (W1 /\ W1) is Relation-like K20(REAL, the carrier of (W1 /\ W1)) -defined the carrier of (W1 /\ W1) -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1)))
K20(REAL, the carrier of (W1 /\ W1)) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1)) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of (W1 /\ W1)), the carrier of (W1 /\ W1))) is non empty V12() non finite set
RLSStruct(# the carrier of (W1 /\ W1), the ZeroF of (W1 /\ W1), the U5 of (W1 /\ W1), the Mult of (W1 /\ W1) #) is strict RLSStruct
Lin A is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1 /\ W1
w1 is Element of K19( the carrier of x)
Lin w1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
x \ {A} is Element of K19( the carrier of x)
A \ {A} is finite Element of K19( the carrier of (W1 /\ W1))
I1 \/ I2 is finite set
A is set
A9 is Element of the carrier of x
W1 + W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
the carrier of (W1 + W1) is non empty set
K19( the carrier of (W1 + W1)) is non empty set
A is finite Element of K19( the carrier of (W1 + W1))
card A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card I1 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card I2 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(card I1) + (card I2) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
card A is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((card I1) + (card I2)) - (card A) is ext-real V25() V26() Element of REAL
0. (W1 + W1) is V64(W1 + W1) Element of the carrier of (W1 + W1)
w2 is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of A
Sum w2 is Element of the carrier of (W1 + W1)
Carrier w2 is finite Element of K19( the carrier of (W1 + W1))
(Carrier w2) \ I1 is finite Element of K19( the carrier of (W1 + W1))
(Carrier w2) /\ I1 is finite Element of K19( the carrier of W1)
K1 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
rng K1 is finite set
w2 (#) K1 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
Sum (w2 (#) K1) is Element of the carrier of (W1 + W1)
K19((rng K1)) is non empty finite V37() set
w2 is finite Element of K19((rng K1))
w2 ` is finite Element of K19((rng K1))
K1 - (w2 `) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
K1 - w2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
K2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
rng K2 is finite set
(rng K2) /\ (Carrier w2) is finite Element of K19( the carrier of (W1 + W1))
w2 (#) K2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
L1 is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 + W1
Carrier L1 is finite Element of K19( the carrier of (W1 + W1))
L1 (#) K2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
Sum (w2 (#) K2) is Element of the carrier of (W1 + W1)
Sum L1 is Element of the carrier of (W1 + W1)
L2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
rng L2 is finite set
(rng L2) /\ (Carrier w2) is finite Element of K19( the carrier of (W1 + W1))
w2 (#) L2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
L is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 + W1
Carrier L is finite Element of K19( the carrier of (W1 + W1))
L (#) L2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
Sum (w2 (#) L2) is Element of the carrier of (W1 + W1)
Sum L is Element of the carrier of (W1 + W1)
L is finite Element of K19((rng K1))
L \ (w2 `) is finite Element of K19((rng K1))
(w2 `) ` is finite Element of K19((rng K1))
L /\ ((w2 `) `) is finite Element of K19((rng K1))
(Carrier w2) /\ (Carrier w2) is finite Element of K19( the carrier of (W1 + W1))
I1 /\ ((Carrier w2) /\ (Carrier w2)) is finite Element of K19( the carrier of (W1 + W1))
w1 is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1 + W1
the carrier of w1 is non empty set
K1 is Relation-like the carrier of w1 -defined REAL -valued Function-like total quasi_total Linear_Combination of w1
Carrier K1 is finite Element of K19( the carrier of w1)
K19( the carrier of w1) is non empty set
Sum K1 is Element of the carrier of w1
(Carrier w2) \ ((Carrier w2) /\ I1) is finite Element of K19( the carrier of (W1 + W1))
(Carrier L1) /\ (Carrier L) is finite Element of K19( the carrier of (W1 + W1))
I1 /\ ((Carrier w2) \ I1) is finite Element of K19( the carrier of (W1 + W1))
(Carrier w2) /\ (I1 /\ ((Carrier w2) \ I1)) is finite Element of K19( the carrier of (W1 + W1))
(Carrier w2) /\ {} is Relation-like finite V129() V130() V131() V132() V133() V134() Element of K19( the carrier of (W1 + W1))
x is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1 + W1
the carrier of x is non empty set
K2 is Relation-like the carrier of x -defined REAL -valued Function-like total quasi_total Linear_Combination of x
Carrier K2 is finite Element of K19( the carrier of x)
K19( the carrier of x) is non empty set
Sum K2 is Element of the carrier of x
dom K1 is finite V129() V130() V131() V132() V133() V134() Element of K19(NAT)
K20((dom K1),(dom K1)) is Relation-like finite set
K19(K20((dom K1),(dom K1))) is non empty finite V37() set
(K1 - (w2 `)) ^ (K1 - w2) is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
K2 ^ L2 is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
w2 (#) (K2 ^ L2) is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
Sum (w2 (#) (K2 ^ L2)) is Element of the carrier of (W1 + W1)
(w2 (#) K2) ^ (w2 (#) L2) is Relation-like NAT -defined the carrier of (W1 + W1) -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (W1 + W1)
Sum ((w2 (#) K2) ^ (w2 (#) L2)) is Element of the carrier of (W1 + W1)
(Sum L1) + (Sum L) is Element of the carrier of (W1 + W1)
KI is Relation-like dom K1 -defined dom K1 -valued Function-like one-to-one total quasi_total onto bijective finite Element of K19(K20((dom K1),(dom K1)))
K1 * KI is Relation-like dom K1 -defined the carrier of (W1 + W1) -valued Function-like finite Element of K19(K20((dom K1), the carrier of (W1 + W1)))
K20((dom K1), the carrier of (W1 + W1)) is Relation-like set
K19(K20((dom K1), the carrier of (W1 + W1))) is non empty set
- (Sum L) is Element of the carrier of (W1 + W1)
- (Sum K2) is Element of the carrier of x
KI is Relation-like the carrier of (W1 /\ W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of A
Sum KI is Element of the carrier of (W1 /\ W1)
(Carrier L1) \/ (Carrier L) is finite Element of K19( the carrier of (W1 + W1))
L1 + L is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 + W1
Carrier (L1 + L) is finite Element of K19( the carrier of (W1 + W1))
LI is set
K is Element of the carrier of (W1 + W1)
(L1 + L) . K is ext-real V25() V26() Element of REAL
L1 . K is ext-real V25() V26() Element of REAL
L . K is ext-real V25() V26() Element of REAL
(L1 . K) + (L . K) is ext-real V25() V26() Element of REAL
K is Element of the carrier of (W1 + W1)
L1 . K is ext-real V25() V26() Element of REAL
K is Element of the carrier of (W1 + W1)
L . K is ext-real V25() V26() Element of REAL
A \/ I2 is finite set
Carrier KI is finite Element of K19( the carrier of (W1 /\ W1))
LI is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 + W1
Carrier LI is finite Element of K19( the carrier of (W1 + W1))
Sum LI is Element of the carrier of (W1 + W1)
A9 is linearly-independent Element of K19( the carrier of (W1 + W1))
LI + L is Relation-like the carrier of (W1 + W1) -defined REAL -valued Function-like total quasi_total Linear_Combination of W1 + W1
Carrier (LI + L) is finite Element of K19( the carrier of (W1 + W1))
(Carrier LI) \/ (Carrier L) is finite Element of K19( the carrier of (W1 + W1))
Sum (LI + L) is Element of the carrier of (W1 + W1)
K is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of W1
Carrier K is finite Element of K19( the carrier of W1)
Sum K is Element of the carrier of W1
0. W1 is V64(W1) Element of the carrier of W1
(Sum LI) + (Sum L) is Element of the carrier of (W1 + W1)
K is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of I2
Sum K is Element of the carrier of W1
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is set
w1 is Element of the carrier of x
w2 is Element of the carrier of x
w1 + w2 is Element of the carrier of x
w1 is Element of the carrier of W1
K1 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of I1
Sum K1 is Element of the carrier of W1
w2 is Element of the carrier of W1
K2 is Relation-like the carrier of W1 -defined REAL -valued Function-like total quasi_total Linear_Combination of I2
Sum K2 is Element of the carrier of W1
Carrier K2 is finite Element of K19( the carrier of W1)
L2 is Relation-like the carrier of x -defined REAL -valued Function-like total quasi_total Linear_Combination of x
Carrier L2 is finite Element of K19( the carrier of x)
Sum L2 is Element of the carrier of x
Carrier K1 is finite Element of K19( the carrier of W1)
L1 is Relation-like the carrier of x -defined REAL -valued Function-like total quasi_total Linear_Combination of x
Carrier L1 is finite Element of K19( the carrier of x)
Sum L1 is Element of the carrier of x
L1 + L2 is Relation-like the carrier of x -defined REAL -valued Function-like total quasi_total Linear_Combination of x
Carrier (L1 + L2) is finite Element of K19( the carrier of x)
(Carrier L1) \/ (Carrier L2) is finite Element of K19( the carrier of x)
A9 is Element of K19( the carrier of x)
L is Relation-like the carrier of x -defined REAL -valued Function-like total quasi_total Linear_Combination of A9
Sum L is Element of the carrier of x
Lin A9 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of x
the carrier of (Lin A9) is non empty set
Lin A is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital Subspace of W1 + W1
((W1 + W1)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((W1 /\ W1)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(V) + (W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((V) + (W)) - (n) is ext-real V25() V26() Element of REAL
V /\ W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
((V /\ W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V + W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
((V + W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((V /\ W)) - (n) is ext-real V25() V26() Element of REAL
(n) + (((V /\ W)) - (n)) is ext-real V25() V26() Element of REAL
((V + W)) + ((V /\ W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(((V + W)) + ((V /\ W))) - (n) is ext-real V25() V26() Element of REAL
((V + W)) + (((V /\ W)) - (n)) is ext-real V25() V26() Element of REAL
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(n) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(V) + (W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
the ZeroF of n is Element of the carrier of n
the U5 of n is Relation-like K20( the carrier of n, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20( the carrier of n, the carrier of n), the carrier of n))
K20( the carrier of n, the carrier of n) is Relation-like non empty set
K20(K20( the carrier of n, the carrier of n), the carrier of n) is Relation-like non empty set
K19(K20(K20( the carrier of n, the carrier of n), the carrier of n)) is non empty set
the Mult of n is Relation-like K20(REAL, the carrier of n) -defined the carrier of n -valued Function-like non empty total quasi_total Element of K19(K20(K20(REAL, the carrier of n), the carrier of n))
K20(REAL, the carrier of n) is Relation-like non empty V12() non finite set
K20(K20(REAL, the carrier of n), the carrier of n) is Relation-like non empty V12() non finite set
K19(K20(K20(REAL, the carrier of n), the carrier of n)) is non empty V12() non finite set
RLSStruct(# the carrier of n, the ZeroF of n, the U5 of n, the Mult of n #) is strict RLSStruct
V + W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
V /\ W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(0). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(Omega). (V /\ W) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V /\ W
(0). (V /\ W) is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V /\ W
((V /\ W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((V + W)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
((V + W)) + 0 is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(Omega). n is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(((Omega). n)) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of V is non empty set
K19( the carrier of V) is non empty set
W is finite Element of K19( the carrier of V)
card W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
K19(W) is non empty finite V37() set
x is finite Element of K19(W)
card x is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is Element of K19( the carrier of V)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
x is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
n is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of x
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(x) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
V is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of n is non empty set
K19( the carrier of n) is non empty set
{ (Lin b₁) where b₁ is Element of K19( the carrier of n) : ( b₁ is linearly-independent & card b₁ = V ) } is set
x is set
W1 is Element of K19( the carrier of n)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card W1 is V18() V19() V20() cardinal set
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is Element of K19( the carrier of n)
Lin W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card W1 is V18() V19() V20() cardinal set
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
the carrier of W1 is non empty set
K19( the carrier of W1) is non empty set
W1 is finite Element of K19( the carrier of W1)
A is Element of K19( the carrier of W1)
Lin A is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of W1
B is linearly-independent Element of K19( the carrier of n)
Lin B is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
card B is V18() V19() V20() cardinal set
x is set
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
W1 is set
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W is set
x is set
W1 is set
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of n
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(V,n) is set
W is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
(W) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(V) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
(V,n) is set
W is set
x is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
(x) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
n is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
V is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () RLSStruct
(V,n) is set
W is non empty V83() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V
(W,n) is set
x is set
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of W
(W1) is ext-real non negative V18() V19() V20() V24() V25() V26() finite cardinal V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT
W1 is non empty V83() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital () Subspace of V