:: RUSUB_4 semantic presentation

REAL is set
NAT is non empty V5() V7() V8() V9() non finite cardinal limit_cardinal Element of K11(REAL)
K11(REAL) is non empty set
NAT is non empty V5() V7() V8() V9() non finite cardinal limit_cardinal set
K11(NAT) is non empty V5() non finite set
K11(NAT) is non empty V5() non finite set
COMPLEX is set
RAT is set
INT is set
{} is set
the ext-real non negative empty V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered set is ext-real non negative empty V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered set
2 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
K12(NAT,REAL) is set
K11(K12(NAT,REAL)) is non empty set
1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
3 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
0 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {} is V7() V8() V9() cardinal set
0 " is ext-real non negative V14() V15() set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is finite Element of K11( the carrier of V)
M \/ N is finite Element of K11( the carrier of V)
Lin (M \/ N) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)
y is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M \/ N
Sum y is Element of the carrier of V
Lin {x} is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
a is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of {x}
Sum a is Element of the carrier of V
Carrier y is finite Element of K11( the carrier of V)
u1 is set
v1 is Element of the carrier of V
y . v1 is ext-real V14() V15() Element of REAL
u1 is Element of the carrier of V
y . u1 is ext-real V14() V15() Element of REAL
u1 is Element of the carrier of V
y . u1 is ext-real V14() V15() Element of REAL
v1 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v1 is finite set
y (#) v1 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (y (#) v1) is Element of the carrier of V
v1 -| u1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
v1 |-- u1 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
u2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng u2 is finite set
v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng v2 is finite set
u2 ^ v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (u2 ^ v2) is finite set
(rng (u2 ^ v2)) /\ (Carrier y) is finite Element of K11( the carrier of V)
y (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier A is finite Element of K11( the carrier of V)
A (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
{u1} is non empty V5() finite 1 -element Element of K11( the carrier of V)
v1 - {u1} is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
(Carrier y) \ {u1} is finite Element of K11( the carrier of V)
(M \/ N) \ {u1} is finite Element of K11( the carrier of V)
((M \/ N) \ {u1}) \/ {x} is finite Element of K11( the carrier of V)
Lin (((M \/ N) \ {u1}) \/ {x}) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
(y . u1) " is ext-real V14() V15() Element of REAL
<*u1*> is non empty V5() V16() V19( NAT ) V20( the carrier of V) Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(v1 -| u1) ^ <*u1*> is non empty V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
((v1 -| u1) ^ <*u1*>) ^ (v1 |-- u1) is non empty V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
<*u1*> ^ v2 is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
u2 ^ (<*u1*> ^ v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) u2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) (<*u1*> ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (y (#) (<*u1*> ^ v2)) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) <*u1*> is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
y (#) v2 is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) <*u1*>) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ ((y (#) <*u1*>) ^ (y (#) v2)) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (y (#) <*u1*>) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
((y (#) u2) ^ (y (#) <*u1*>)) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y . u1) * u1 is Element of the carrier of V
<*((y . u1) * u1)*> is non empty V5() V16() V19( NAT ) V20( the carrier of V) Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ <*((y . u1) * u1)*> is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
((y (#) u2) ^ <*((y . u1) * u1)*>) ^ (y (#) v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
<*((y . u1) * u1)*> ^ (y (#) v2) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
(y (#) u2) ^ (<*((y . u1) * u1)*> ^ (y (#) v2)) is non empty V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((y (#) u2) ^ (<*((y . u1) * u1)*> ^ (y (#) v2))) is Element of the carrier of V
Sum (y (#) u2) is Element of the carrier of V
Sum (<*((y . u1) * u1)*> ^ (y (#) v2)) is Element of the carrier of V
(Sum (y (#) u2)) + (Sum (<*((y . u1) * u1)*> ^ (y (#) v2))) is Element of the carrier of V
Sum <*((y . u1) * u1)*> is Element of the carrier of V
Sum (y (#) v2) is Element of the carrier of V
(Sum <*((y . u1) * u1)*>) + (Sum (y (#) v2)) is Element of the carrier of V
(Sum (y (#) u2)) + ((Sum <*((y . u1) * u1)*>) + (Sum (y (#) v2))) is Element of the carrier of V
(Sum (y (#) v2)) + ((y . u1) * u1) is Element of the carrier of V
(Sum (y (#) u2)) + ((Sum (y (#) v2)) + ((y . u1) * u1)) is Element of the carrier of V
(Sum (y (#) u2)) + (Sum (y (#) v2)) is Element of the carrier of V
((Sum (y (#) u2)) + (Sum (y (#) v2))) + ((y . u1) * u1) is Element of the carrier of V
(y (#) u2) ^ (y (#) v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum ((y (#) u2) ^ (y (#) v2)) is Element of the carrier of V
(Sum ((y (#) u2) ^ (y (#) v2))) + ((y . u1) * u1) is Element of the carrier of V
Sum (y (#) (u2 ^ v2)) is Element of the carrier of V
(Sum (y (#) (u2 ^ v2))) + ((y . u1) * u1) is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of (M \/ N) \ {u1}
- A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
(- A9) + a is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier ((- A9) + a) is finite Element of K11( the carrier of V)
Carrier (- A9) is finite Element of K11( the carrier of V)
Carrier a is finite Element of K11( the carrier of V)
(Carrier (- A9)) \/ (Carrier a) is finite Element of K11( the carrier of V)
Carrier A9 is finite Element of K11( the carrier of V)
(Carrier A9) \/ (Carrier a) is finite Element of K11( the carrier of V)
((y . u1) ") * ((- A9) + a) is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of V
Carrier (((y . u1) ") * ((- A9) + a)) is finite Element of K11( the carrier of V)
A9 (#) (u2 ^ v2) is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (A9 (#) (u2 ^ v2)) is Element of the carrier of V
Sum A9 is Element of the carrier of V
((y . u1) ") * x is Element of the carrier of V
((y . u1) ") * (Sum A9) is Element of the carrier of V
((y . u1) ") * ((y . u1) * u1) is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + (((y . u1) ") * ((y . u1) * u1)) is Element of the carrier of V
((y . u1) ") * (y . u1) is ext-real V14() V15() Element of REAL
(((y . u1) ") * (y . u1)) * u1 is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + ((((y . u1) ") * (y . u1)) * u1) is Element of the carrier of V
1 * u1 is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + (1 * u1) is Element of the carrier of V
(((y . u1) ") * (Sum A9)) + u1 is Element of the carrier of V
(((y . u1) ") * x) - (((y . u1) ") * (Sum A9)) is Element of the carrier of V
x - (Sum A9) is Element of the carrier of V
((y . u1) ") * (x - (Sum A9)) is Element of the carrier of V
- (Sum A9) is Element of the carrier of V
(- (Sum A9)) + x is Element of the carrier of V
((y . u1) ") * ((- (Sum A9)) + x) is Element of the carrier of V
Sum (- A9) is Element of the carrier of V
(Sum (- A9)) + (Sum a) is Element of the carrier of V
((y . u1) ") * ((Sum (- A9)) + (Sum a)) is Element of the carrier of V
Sum ((- A9) + a) is Element of the carrier of V
((y . u1) ") * (Sum ((- A9) + a)) is Element of the carrier of V
Sum (((y . u1) ") * ((- A9) + a)) is Element of the carrier of V
V is set
M is set
{M} is non empty V5() finite 1 -element set
V \ {M} is Element of K11(V)
K11(V) is non empty set
(V \ {M}) \/ {M} is set
{M} \/ (V \ {M}) is set
{M} \/ V is set
V is set
M is set
{M} is non empty V5() finite 1 -element set
V \ {M} is Element of K11(V)
K11(V) is non empty set
V /\ {M} is finite set
N is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M + 1 is ext-real positive non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N - (M + 1) is ext-real V14() V15() set
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is finite Element of K11( the carrier of V)
card y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Lin x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
a is set
u1 is Element of the carrier of V
{u1} is non empty V5() finite 1 -element Element of K11( the carrier of V)
y \ {u1} is finite Element of K11( the carrier of V)
K11(y) is non empty finite V37() set
card (y \ {u1}) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {u1} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card y) - (card {u1}) is ext-real V14() V15() set
(M + 1) - 1 is ext-real V14() V15() Element of REAL
N - M is ext-real V14() V15() set
u2 is finite Element of K11( the carrier of V)
card u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(y \ {u1}) \/ u2 is finite Element of K11( the carrier of V)
Lin ((y \ {u1}) \/ u2) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
Lin (y \ {u1}) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
M - M is ext-real V14() V15() set
v2 is finite Element of K11( the carrier of V)
card v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(y \ {u1}) \/ v2 is finite Element of K11( the carrier of V)
Lin ((y \ {u1}) \/ v2) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
u2 \/ (y \ {u1}) is finite Element of K11( the carrier of V)
v2 is Element of the carrier of V
{v2} is non empty V5() finite 1 -element Element of K11( the carrier of V)
(u2 \/ (y \ {u1})) \ {v2} is finite Element of K11( the carrier of V)
((u2 \/ (y \ {u1})) \ {v2}) \/ {u1} is finite Element of K11( the carrier of V)
Lin (((u2 \/ (y \ {u1})) \ {v2}) \/ {u1}) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
u2 \ {v2} is finite Element of K11( the carrier of V)
(y \ {u1}) \ {v2} is finite Element of K11( the carrier of V)
((y \ {u1}) \ {v2}) \/ {u1} is finite Element of K11( the carrier of V)
(y \ {u1}) \/ {u1} is finite Element of K11( the carrier of V)
(u2 \ {v2}) \/ (((y \ {u1}) \ {v2}) \/ {u1}) is finite Element of K11( the carrier of V)
(u2 \ {v2}) \/ ((y \ {u1}) \/ {u1}) is finite Element of K11( the carrier of V)
y \/ (u2 \ {v2}) is finite Element of K11( the carrier of V)
K11(u2) is non empty finite V37() set
card (u2 \ {v2}) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card {v2} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card u2) - (card {v2}) is ext-real V14() V15() set
(N - M) - 1 is ext-real V14() V15() Element of REAL
N - (M + 1) is ext-real V14() V15() Element of REAL
(u2 \ {v2}) \/ ((y \ {u1}) \ {v2}) is finite Element of K11( the carrier of V)
((u2 \ {v2}) \/ ((y \ {u1}) \ {v2})) \/ {u1} is finite Element of K11( the carrier of V)
Lin (y \/ (u2 \ {v2})) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
(u2 \ {v2}) \/ {v2} is finite Element of K11( the carrier of V)
A is set
the carrier of (Lin (y \/ (u2 \ {v2}))) is non empty set
the carrier of (Lin ((y \ {u1}) \/ u2)) is non empty set
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M - 0 is ext-real V14() V15() set
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
x \/ N is finite Element of K11( the carrier of V)
M is finite Element of K11( the carrier of V)
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card M) - (card N) is ext-real V14() V15() set
the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
(0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is non empty set
K11( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) is non empty set
{} the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))
M is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of (0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
(0). ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of (0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the ZeroF of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is Element of the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )
the addF of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is V16() V19(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))) V20( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) Function-like quasi_total Element of K11(K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )))
K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) is non empty set
K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) is non empty set
K11(K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))) is non empty set
the Mult of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is V16() V19(K12(REAL, the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))) V20( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )))
K12(REAL, the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) is set
K12(K12(REAL, the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )) is set
K11(K12(K12(REAL, the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))) is non empty set
the scalar of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) is V16() V19(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ))) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )),REAL))
K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )),REAL) is set
K11(K12(K12( the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR )),REAL)) is non empty set
UNITSTR(# the carrier of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the ZeroF of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the addF of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the Mult of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ), the scalar of ((0). the non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR ) #) is strict UNITSTR
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is Basis of V
x is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
rng x is finite set
y is V16() V19( NAT ) V20( the carrier of V) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
dom y is finite Element of K11(NAT)
{ (Carrier b₁) where b₁ is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N : ex b₂ being ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT st
( b₂ in dom y & Sum b₁ = y . b₂ ) } is set
union { (Carrier b₁) where b₁ is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N : ex b₂ being ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT st
( b₂ in dom y & Sum b₁ = y . b₂ ) } is set
v1 is set
u2 is set
v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier v2 is finite Element of K11( the carrier of V)
I1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Sum v2 is Element of the carrier of V
y . I1 is set
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
v1 is Element of K11( the carrier of V)
Lin v1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
u2 is Element of the carrier of V
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M
Sum v2 is Element of the carrier of V
Carrier v2 is finite Element of K11( the carrier of V)
the carrier of (Lin v1) is non empty set
I1 is set
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
A is Element of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Sum A is Element of the carrier of V
Carrier A is finite Element of K11( the carrier of V)
A9 is set
y . A9 is set
A9 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of v1
Sum I1 is Element of the carrier of V
the carrier of UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is set
the carrier of ((Omega). V) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
N \ v1 is Element of K11( the carrier of V)
I1 is set
I1 is Element of K11( the carrier of V)
I1 \ v1 is Element of K11( the carrier of V)
v1 \/ (I1 \ v1) is Element of K11( the carrier of V)
v1 \/ I1 is Element of K11( the carrier of V)
v2 is non empty Element of K11( the carrier of V)
v1 \/ v2 is Element of K11( the carrier of V)
len y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Seg (len y) is finite len y -element Element of K11(NAT)
u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal set
y . u2 is set
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
v2 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Sum v2 is Element of the carrier of V
Carrier v2 is finite Element of K11( the carrier of V)
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
Sum I1 is Element of the carrier of V
u2 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom u2 is finite Element of K11(NAT)
u2 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
dom u2 is finite Element of K11(NAT)
v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal set
y . v2 is set
I1 is set
A is set
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A9 is finite Element of K11( the carrier of V)
Sum A9 is Element of the carrier of V
A9 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A9 is finite Element of K11( the carrier of V)
Sum A9 is Element of the carrier of V
v2 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
Sum I1 is Element of the carrier of V
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y . A is set
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y . A is set
u2 . A is set
A is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier A is finite Element of K11( the carrier of V)
Sum A is Element of the carrier of V
rng u2 is finite set
v2 is set
I1 is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of N
Carrier I1 is finite Element of K11( the carrier of V)
A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Sum I1 is Element of the carrier of V
y . A is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
N is Basis of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
M is Basis of V
card M is V7() V8() V9() cardinal set
N is Basis of V
card N is V7() V8() V9() cardinal set
the carrier of V is non empty set
K11( the carrier of V) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is finite Element of K11( the carrier of V)
card y is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like UNITSTR
the carrier of M is non empty set
K11( the carrier of M) is non empty set
{} the carrier of M is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of M)
the carrier of V is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{(0. V)} is non empty V5() finite 1 -element Element of K11( the carrier of V)
K11( the carrier of V) is non empty set
0. M is V64(M) Element of the carrier of M
the ZeroF of M is Element of the carrier of M
{(0. M)} is non empty V5() finite 1 -element Element of K11( the carrier of M)
(0). M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of M
the carrier of ((0). M) is non empty set
N is finite Element of K11( the carrier of M)
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of M
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of V
the Basis of M is Basis of M
x is Basis of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is Basis of V
card x is V7() V8() V9() cardinal set
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
x is finite Element of K11( the carrier of V)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the Basis of M is Basis of M
the carrier of M is non empty set
K11( the carrier of M) is non empty set
x is Element of K11( the carrier of M)
the carrier of V is non empty set
K11( the carrier of V) is non empty set
y is linearly-independent Element of K11( the carrier of V)
u1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the Basis of u1 is Basis of u1
Lin the Basis of u1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of u1
the carrier of u1 is non empty set
the ZeroF of u1 is Element of the carrier of u1
the addF of u1 is V16() V19(K12( the carrier of u1, the carrier of u1)) V20( the carrier of u1) Function-like quasi_total Element of K11(K12(K12( the carrier of u1, the carrier of u1), the carrier of u1))
K12( the carrier of u1, the carrier of u1) is non empty set
K12(K12( the carrier of u1, the carrier of u1), the carrier of u1) is non empty set
K11(K12(K12( the carrier of u1, the carrier of u1), the carrier of u1)) is non empty set
the Mult of u1 is V16() V19(K12(REAL, the carrier of u1)) V20( the carrier of u1) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of u1), the carrier of u1))
K12(REAL, the carrier of u1) is set
K12(K12(REAL, the carrier of u1), the carrier of u1) is set
K11(K12(K12(REAL, the carrier of u1), the carrier of u1)) is non empty set
the scalar of u1 is V16() V19(K12( the carrier of u1, the carrier of u1)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of u1, the carrier of u1),REAL))
K12(K12( the carrier of u1, the carrier of u1),REAL) is set
K11(K12(K12( the carrier of u1, the carrier of u1),REAL)) is non empty set
UNITSTR(# the carrier of u1, the ZeroF of u1, the addF of u1, the Mult of u1, the scalar of u1 #) is strict UNITSTR
u2 is finite Element of K11( the carrier of V)
card u2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is finite Element of K11( the carrier of V)
card a is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
card M is V7() V8() V9() cardinal set
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
((Lin M)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is set
the carrier of (Lin M) is non empty set
K11( the carrier of (Lin M)) is non empty set
x is linearly-independent Element of K11( the carrier of (Lin M))
Lin x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of Lin M
y is Basis of Lin M
card y is V7() V8() V9() cardinal set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(((Omega). V)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(Omega). M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M
the carrier of V is non empty set
K11( the carrier of V) is non empty set
N is finite Element of K11( the carrier of V)
the Basis of M is Basis of M
y is Basis of V
the carrier of M is non empty set
card the Basis of M is V7() V8() V9() cardinal set
card y is V7() V8() V9() cardinal set
u1 is finite Element of K11( the carrier of V)
card u1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is finite Element of K11( the carrier of V)
card a is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
K11( the carrier of M) is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
v1 is Element of K11( the carrier of V)
Lin v1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
u2 is Element of K11( the carrier of M)
Lin u2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M
the ZeroF of M is Element of the carrier of M
the addF of M is V16() V19(K12( the carrier of M, the carrier of M)) V20( the carrier of M) Function-like quasi_total Element of K11(K12(K12( the carrier of M, the carrier of M), the carrier of M))
K12( the carrier of M, the carrier of M) is non empty set
K12(K12( the carrier of M, the carrier of M), the carrier of M) is non empty set
K11(K12(K12( the carrier of M, the carrier of M), the carrier of M)) is non empty set
the Mult of M is V16() V19(K12(REAL, the carrier of M)) V20( the carrier of M) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of M), the carrier of M))
K12(REAL, the carrier of M) is set
K12(K12(REAL, the carrier of M), the carrier of M) is set
K11(K12(K12(REAL, the carrier of M), the carrier of M)) is non empty set
the scalar of M is V16() V19(K12( the carrier of M, the carrier of M)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of M, the carrier of M),REAL))
K12(K12( the carrier of M, the carrier of M),REAL) is set
K11(K12(K12( the carrier of M, the carrier of M),REAL)) is non empty set
UNITSTR(# the carrier of M, the ZeroF of M, the addF of M, the Mult of M, the scalar of M #) is strict UNITSTR
x is finite Element of K11( the carrier of M)
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
Lin x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M
a is Element of K11( the carrier of V)
card a is V7() V8() V9() cardinal set
y is Element of K11( the carrier of M)
Lin y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M
((Lin y)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card y is V7() V8() V9() cardinal set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
{} the carrier of V is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of V)
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
Lin N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
0. V is V64(V) Element of the carrier of V
{(0. V)} is non empty V5() finite 1 -element Element of K11( the carrier of V)
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is set
{N} is non empty V5() finite 1 -element set
x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)
Lin {x} is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is Element of the carrier of V
{M} is non empty V5() finite 1 -element Element of K11( the carrier of V)
Lin {M} is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card {M} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
K11( the carrier of V) is non empty set
M is finite Element of K11( the carrier of V)
card M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is set
x is Element of the carrier of V
{x} is non empty V5() finite 1 -element Element of K11( the carrier of V)
card {x} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is set
a is Element of the carrier of V
{x,a} is finite Element of K11( the carrier of V)
u1 is set
{x,a,u1} is non empty finite set
v1 is set
card {x,a,u1} is ext-real non negative non empty V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
u1 is set
Lin {x,a} is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M is Element of the carrier of V
N is Element of the carrier of V
{M,N} is finite Element of K11( the carrier of V)
Lin {M,N} is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card {M,N} is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
M + N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
((M + N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M /\ N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M + N)) + ((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) + (N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of x
a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of x
y /\ a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of x
the carrier of (y /\ a) is non empty set
K11( the carrier of (y /\ a)) is non empty set
u1 is finite Element of K11( the carrier of (y /\ a))
v1 is Basis of a
u2 is Basis of y
the carrier of a is non empty set
K11( the carrier of a) is non empty set
the carrier of y is non empty set
K11( the carrier of y) is non empty set
I1 is finite Element of K11( the carrier of y)
the carrier of x is non empty set
K11( the carrier of x) is non empty set
v2 is finite Element of K11( the carrier of a)
I1 /\ v2 is finite Element of K11( the carrier of a)
A9 is set
Lin I1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of y
the ZeroF of y is Element of the carrier of y
the addF of y is V16() V19(K12( the carrier of y, the carrier of y)) V20( the carrier of y) Function-like quasi_total Element of K11(K12(K12( the carrier of y, the carrier of y), the carrier of y))
K12( the carrier of y, the carrier of y) is non empty set
K12(K12( the carrier of y, the carrier of y), the carrier of y) is non empty set
K11(K12(K12( the carrier of y, the carrier of y), the carrier of y)) is non empty set
the Mult of y is V16() V19(K12(REAL, the carrier of y)) V20( the carrier of y) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of y), the carrier of y))
K12(REAL, the carrier of y) is set
K12(K12(REAL, the carrier of y), the carrier of y) is set
K11(K12(K12(REAL, the carrier of y), the carrier of y)) is non empty set
the scalar of y is V16() V19(K12( the carrier of y, the carrier of y)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of y, the carrier of y),REAL))
K12(K12( the carrier of y, the carrier of y),REAL) is set
K11(K12(K12( the carrier of y, the carrier of y),REAL)) is non empty set
UNITSTR(# the carrier of y, the ZeroF of y, the addF of y, the Mult of y, the scalar of y #) is strict UNITSTR
w1 is set
{A9} is non empty V5() finite 1 -element set
u1 \/ {A9} is finite set
w2 is set
A is linearly-independent Element of K11( the carrier of x)
w1 is Element of K11( the carrier of x)
x is Element of the carrier of x
Lin v2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of a
the ZeroF of a is Element of the carrier of a
the addF of a is V16() V19(K12( the carrier of a, the carrier of a)) V20( the carrier of a) Function-like quasi_total Element of K11(K12(K12( the carrier of a, the carrier of a), the carrier of a))
K12( the carrier of a, the carrier of a) is non empty set
K12(K12( the carrier of a, the carrier of a), the carrier of a) is non empty set
K11(K12(K12( the carrier of a, the carrier of a), the carrier of a)) is non empty set
the Mult of a is V16() V19(K12(REAL, the carrier of a)) V20( the carrier of a) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of a), the carrier of a))
K12(REAL, the carrier of a) is set
K12(K12(REAL, the carrier of a), the carrier of a) is set
K11(K12(K12(REAL, the carrier of a), the carrier of a)) is non empty set
the scalar of a is V16() V19(K12( the carrier of a, the carrier of a)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of a, the carrier of a),REAL))
K12(K12( the carrier of a, the carrier of a),REAL) is set
K11(K12(K12( the carrier of a, the carrier of a),REAL)) is non empty set
UNITSTR(# the carrier of a, the ZeroF of a, the addF of a, the Mult of a, the scalar of a #) is strict UNITSTR
the carrier of y /\ the carrier of a is set
the ZeroF of (y /\ a) is Element of the carrier of (y /\ a)
the addF of (y /\ a) is V16() V19(K12( the carrier of (y /\ a), the carrier of (y /\ a))) V20( the carrier of (y /\ a)) Function-like quasi_total Element of K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a)))
K12( the carrier of (y /\ a), the carrier of (y /\ a)) is non empty set
K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a)) is non empty set
K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)), the carrier of (y /\ a))) is non empty set
the Mult of (y /\ a) is V16() V19(K12(REAL, the carrier of (y /\ a))) V20( the carrier of (y /\ a)) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a)))
K12(REAL, the carrier of (y /\ a)) is set
K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a)) is set
K11(K12(K12(REAL, the carrier of (y /\ a)), the carrier of (y /\ a))) is non empty set
the scalar of (y /\ a) is V16() V19(K12( the carrier of (y /\ a), the carrier of (y /\ a))) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL))
K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL) is set
K11(K12(K12( the carrier of (y /\ a), the carrier of (y /\ a)),REAL)) is non empty set
UNITSTR(# the carrier of (y /\ a), the ZeroF of (y /\ a), the addF of (y /\ a), the Mult of (y /\ a), the scalar of (y /\ a) #) is strict UNITSTR
Lin u1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of y /\ a
w1 \ {A9} is Element of K11( the carrier of x)
u1 \ {A9} is finite Element of K11( the carrier of (y /\ a))
A is Element of K11( the carrier of x)
Lin A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of x
I1 \/ v2 is finite set
A is set
A9 is Element of the carrier of x
y + a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of x
the carrier of (y + a) is non empty set
K11( the carrier of (y + a)) is non empty set
A is finite Element of K11( the carrier of (y + a))
card A is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card I1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card v2 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(card I1) + (card v2) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
card u1 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((card I1) + (card v2)) - (card u1) is ext-real V14() V15() Element of REAL
0. (y + a) is V64(y + a) Element of the carrier of (y + a)
the ZeroF of (y + a) is Element of the carrier of (y + a)
w2 is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of A
Sum w2 is Element of the carrier of (y + a)
Carrier w2 is finite Element of K11( the carrier of (y + a))
(Carrier w2) \ I1 is finite Element of K11( the carrier of (y + a))
(Carrier w2) /\ I1 is finite Element of K11( the carrier of y)
K1 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
rng K1 is finite set
w2 (#) K1 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
Sum (w2 (#) K1) is Element of the carrier of (y + a)
K11((rng K1)) is non empty finite V37() set
w2 is finite Element of K11((rng K1))
w2 ` is finite Element of K11((rng K1))
K1 - (w2 `) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
K1 - w2 is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
K2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
rng K2 is finite set
(rng K2) /\ (Carrier w2) is finite Element of K11( the carrier of (y + a))
w2 (#) K2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
L1 is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of y + a
Carrier L1 is finite Element of K11( the carrier of (y + a))
L1 (#) K2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
Sum (w2 (#) K2) is Element of the carrier of (y + a)
Sum L1 is Element of the carrier of (y + a)
L2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
rng L2 is finite set
(rng L2) /\ (Carrier w2) is finite Element of K11( the carrier of (y + a))
w2 (#) L2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
L is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of y + a
Carrier L is finite Element of K11( the carrier of (y + a))
L (#) L2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
Sum (w2 (#) L2) is Element of the carrier of (y + a)
Sum L is Element of the carrier of (y + a)
L is finite Element of K11((rng K1))
L \ (w2 `) is finite Element of K11((rng K1))
(w2 `) ` is finite Element of K11((rng K1))
L /\ ((w2 `) `) is finite Element of K11((rng K1))
(Carrier w2) /\ (Carrier w2) is finite Element of K11( the carrier of (y + a))
I1 /\ ((Carrier w2) /\ (Carrier w2)) is finite Element of K11( the carrier of (y + a))
w1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of y + a
the carrier of w1 is non empty set
K1 is V16() V19( the carrier of w1) V20( REAL ) Function-like quasi_total Linear_Combination of w1
Carrier K1 is finite Element of K11( the carrier of w1)
K11( 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 K11( the carrier of (y + a))
(Carrier L1) /\ (Carrier L) is finite Element of K11( the carrier of (y + a))
I1 /\ ((Carrier w2) \ I1) is finite Element of K11( the carrier of (y + a))
(Carrier w2) /\ (I1 /\ ((Carrier w2) \ I1)) is finite Element of K11( the carrier of (y + a))
(Carrier w2) /\ {} is finite Element of K11( the carrier of (y + a))
x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of y + a
the carrier of x is non empty set
K2 is V16() V19( the carrier of x) V20( REAL ) Function-like quasi_total Linear_Combination of x
Carrier K2 is finite Element of K11( the carrier of x)
K11( the carrier of x) is non empty set
Sum K2 is Element of the carrier of x
dom K1 is finite Element of K11(NAT)
K12((dom K1),(dom K1)) is finite set
K11(K12((dom K1),(dom K1))) is non empty finite V37() set
(K1 - (w2 `)) ^ (K1 - w2) is V16() V19( NAT ) Function-like finite FinSequence-like FinSubsequence-like set
K2 ^ L2 is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
w2 (#) (K2 ^ L2) is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
Sum (w2 (#) (K2 ^ L2)) is Element of the carrier of (y + a)
(w2 (#) K2) ^ (w2 (#) L2) is V16() V19( NAT ) V20( the carrier of (y + a)) Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of (y + a)
Sum ((w2 (#) K2) ^ (w2 (#) L2)) is Element of the carrier of (y + a)
(Sum L1) + (Sum L) is Element of the carrier of (y + a)
KI is V16() V19( dom K1) V20( dom K1) Function-like quasi_total bijective finite Element of K11(K12((dom K1),(dom K1)))
K1 * KI is V16() finite set
- (Sum L) is Element of the carrier of (y + a)
- (Sum K2) is Element of the carrier of x
KI is V16() V19( the carrier of (y /\ a)) V20( REAL ) Function-like quasi_total Linear_Combination of u1
Sum KI is Element of the carrier of (y /\ a)
(Carrier L1) \/ (Carrier L) is finite Element of K11( the carrier of (y + a))
L1 + L is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of y + a
Carrier (L1 + L) is finite Element of K11( the carrier of (y + a))
LI is set
K is Element of the carrier of (y + a)
(L1 + L) . K is ext-real V14() V15() Element of REAL
L1 . K is ext-real V14() V15() Element of REAL
L . K is ext-real V14() V15() Element of REAL
(L1 . K) + (L . K) is ext-real V14() V15() Element of REAL
K is Element of the carrier of (y + a)
L1 . K is ext-real V14() V15() Element of REAL
K is Element of the carrier of (y + a)
L . K is ext-real V14() V15() Element of REAL
u1 \/ v2 is finite set
Carrier KI is finite Element of K11( the carrier of (y /\ a))
LI is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of y + a
Carrier LI is finite Element of K11( the carrier of (y + a))
Sum LI is Element of the carrier of (y + a)
A9 is linearly-independent Element of K11( the carrier of (y + a))
LI + L is V16() V19( the carrier of (y + a)) V20( REAL ) Function-like quasi_total Linear_Combination of y + a
Carrier (LI + L) is finite Element of K11( the carrier of (y + a))
(Carrier LI) \/ (Carrier L) is finite Element of K11( the carrier of (y + a))
Sum (LI + L) is Element of the carrier of (y + a)
K is V16() V19( the carrier of a) V20( REAL ) Function-like quasi_total Linear_Combination of a
Carrier K is finite Element of K11( the carrier of a)
Sum K is Element of the carrier of a
0. a is V64(a) Element of the carrier of a
(Sum LI) + (Sum L) is Element of the carrier of (y + a)
K is V16() V19( the carrier of a) V20( REAL ) Function-like quasi_total Linear_Combination of v2
Sum K is Element of the carrier of a
(a) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal 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 y
K1 is V16() V19( the carrier of y) V20( REAL ) Function-like quasi_total Linear_Combination of I1
Sum K1 is Element of the carrier of y
w2 is Element of the carrier of a
K2 is V16() V19( the carrier of a) V20( REAL ) Function-like quasi_total Linear_Combination of v2
Sum K2 is Element of the carrier of a
Carrier K2 is finite Element of K11( the carrier of a)
L2 is V16() V19( the carrier of x) V20( REAL ) Function-like quasi_total Linear_Combination of x
Carrier L2 is finite Element of K11( the carrier of x)
Sum L2 is Element of the carrier of x
Carrier K1 is finite Element of K11( the carrier of y)
L1 is V16() V19( the carrier of x) V20( REAL ) Function-like quasi_total Linear_Combination of x
Carrier L1 is finite Element of K11( the carrier of x)
Sum L1 is Element of the carrier of x
L1 + L2 is V16() V19( the carrier of x) V20( REAL ) Function-like quasi_total Linear_Combination of x
Carrier (L1 + L2) is finite Element of K11( the carrier of x)
(Carrier L1) \/ (Carrier L2) is finite Element of K11( the carrier of x)
A9 is Element of K11( the carrier of x)
L is V16() V19( the carrier of x) V20( REAL ) Function-like quasi_total Linear_Combination of A9
Sum L is Element of the carrier of x
Lin A9 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of x
the carrier of (Lin A9) is non empty set
Lin A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of y + a
((y /\ a)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((y + a)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((y + a)) + ((y /\ a)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
- (card u1) is ext-real non positive V14() V15() set
((card I1) + (card v2)) + (- (card u1)) is ext-real V14() V15() Element of REAL
(((card I1) + (card v2)) + (- (card u1))) + (card u1) is ext-real V14() V15() Element of REAL
(y) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(y) + (a) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) + (N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M) + (N)) - (V) is ext-real V14() V15() Element of REAL
M /\ N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M + N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
((M + N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M /\ N)) - (V) is ext-real V14() V15() set
(V) + (((M /\ N)) - (V)) is ext-real V14() V15() set
((M + N)) + ((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(((M + N)) + ((M /\ N))) - (V) is ext-real V14() V15() Element of REAL
((M + N)) + (((M /\ N)) - (V)) is ext-real V14() V15() set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
(M) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M) + (N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
the addF of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V), the carrier of V))
K12( the carrier of V, the carrier of V) is non empty set
K12(K12( the carrier of V, the carrier of V), the carrier of V) is non empty set
K11(K12(K12( the carrier of V, the carrier of V), the carrier of V)) is non empty set
the Mult of V is V16() V19(K12(REAL, the carrier of V)) V20( the carrier of V) Function-like quasi_total Element of K11(K12(K12(REAL, the carrier of V), the carrier of V))
K12(REAL, the carrier of V) is set
K12(K12(REAL, the carrier of V), the carrier of V) is set
K11(K12(K12(REAL, the carrier of V), the carrier of V)) is non empty set
the scalar of V is V16() V19(K12( the carrier of V, the carrier of V)) V20( REAL ) Function-like quasi_total Element of K11(K12(K12( the carrier of V, the carrier of V),REAL))
K12(K12( the carrier of V, the carrier of V),REAL) is set
K11(K12(K12( the carrier of V, the carrier of V),REAL)) is non empty set
UNITSTR(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, the scalar of V #) is strict UNITSTR
M + N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
M /\ N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(0). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(Omega). (M /\ N) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M /\ N
(0). (M /\ N) is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M /\ N
((M /\ N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M + N)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
((M + N)) + 0 is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(Omega). V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(((Omega). V)) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
N is finite Element of K11( the carrier of V)
card N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
K11(N) is non empty finite V37() set
x is finite Element of K11(N)
card x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is Element of K11( the carrier of V)
Lin y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(a) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of N
(y) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
x is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of V is non empty set
K11( the carrier of V) is non empty set
{ (Lin b₁) where b₁ is Element of K11( the carrier of V) : ( b₁ is linearly-independent & card b₁ = M ) } is set
x is set
a is Element of K11( the carrier of V)
Lin a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card a is V7() V8() V9() cardinal set
y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(y) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is Element of K11( the carrier of V)
Lin a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card a is V7() V8() V9() cardinal set
y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(y) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
the carrier of y is non empty set
K11( the carrier of y) is non empty set
a is finite Element of K11( the carrier of y)
u1 is Element of K11( the carrier of y)
Lin u1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of y
v1 is linearly-independent Element of K11( the carrier of V)
Lin v1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
card v1 is V7() V8() V9() cardinal set
x is set
a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
y is set
(a) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
N is set
x is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(V,M) is set
N is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(N) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
(V) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
M is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(V,M) is set
N is set
x is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
(x) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like () Subspace of V
N is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
(M,N) is set
(V,N) is set
x is set
y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of M
(y) is ext-real non negative V7() V8() V9() V13() V14() V15() finite cardinal Element of NAT
a is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like () Subspace of V
V is non empty RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
V is non empty RLSStruct
[#] V is non empty non proper Element of K11( the carrier of V)
the carrier of V is non empty set
K11( the carrier of V) is non empty set
{} V is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of V)
M is Element of the carrier of V
N is Element of the carrier of V
x is ext-real V14() V15() Element of REAL
1 - x is ext-real V14() V15() Element of REAL
(1 - x) * M is Element of the carrier of V
x * N is Element of the carrier of V
((1 - x) * M) + (x * N) is Element of the carrier of V
M is Element of the carrier of V
N is Element of the carrier of V
x is ext-real V14() V15() Element of REAL
1 - x is ext-real V14() V15() Element of REAL
(1 - x) * M is Element of the carrier of V
x * N is Element of the carrier of V
((1 - x) * M) + (x * N) is Element of the carrier of V
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
M is Element of the carrier of V
{M} is non empty V5() finite 1 -element Element of K11( the carrier of V)
K11( the carrier of V) is non empty set
N is Element of the carrier of V
x is Element of the carrier of V
y is ext-real V14() V15() Element of REAL
1 - y is ext-real V14() V15() Element of REAL
(1 - y) * N is Element of the carrier of V
y * x is Element of the carrier of V
((1 - y) * N) + (y * x) is Element of the carrier of V
(1 - y) + y is ext-real V14() V15() Element of REAL
((1 - y) + y) * M is Element of the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
[#] V is non empty non proper Element of K11( the carrier of V)
{} V is ext-real non negative empty proper V7() V8() V9() V11() V12() V13() V14() V15() functional finite V37() cardinal {} -element FinSequence-membered Element of K11( the carrier of V)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() Subspace of V
the carrier of M is non empty set
the carrier of V is non empty set
K11( the carrier of V) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of V
the carrier of M is non empty set
the carrier of V is non empty set
K11( the carrier of V) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
0. V is V64(V) Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() Subspace of V
(V,M) is non empty Element of K11( the carrier of V)
K11( the carrier of V) is non empty set
the carrier of M is non empty set
N is Element of the carrier of V
x is Element of the carrier of V
y is ext-real V14() V15() Element of REAL
1 - y is ext-real V14() V15() Element of REAL
(1 - y) * N is Element of the carrier of V
y * x is Element of the carrier of V
((1 - y) * N) + (y * x) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is (V) Element of K11( the carrier of V)
N is Element of the carrier of V
x is ext-real V14() V15() Element of REAL
x * N is Element of the carrier of V
1 - x is ext-real V14() V15() Element of REAL
(1 - x) * (0. V) is Element of the carrier of V
((1 - x) * (0. V)) + (x * N) is Element of the carrier of V
(0. V) + (x * N) is Element of the carrier of V
N is Element of the carrier of V
x is ext-real V14() V15() Element of REAL
x * N is Element of the carrier of V
V is non empty RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is non empty (V) Element of K11( the carrier of V)
Lin M is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() Subspace of V
the carrier of (Lin M) is non empty set
N is Element of the carrier of V
x is Element of the carrier of V
N + x is Element of the carrier of V
y is ext-real V14() V15() Element of REAL
y * N is Element of the carrier of V
a is Element of the carrier of V
1 / 2 is ext-real non negative V14() V15() Element of REAL
1 - (1 / 2) is ext-real V14() V15() Element of REAL
(1 - (1 / 2)) * a is Element of the carrier of V
u1 is Element of the carrier of V
(1 / 2) * u1 is Element of the carrier of V
((1 - (1 / 2)) * a) + ((1 / 2) * u1) is Element of the carrier of V
2 * (((1 - (1 / 2)) * a) + ((1 / 2) * u1)) is Element of the carrier of V
2 * ((1 - (1 / 2)) * a) is Element of the carrier of V
2 * ((1 / 2) * u1) is Element of the carrier of V
(2 * ((1 - (1 / 2)) * a)) + (2 * ((1 / 2) * u1)) is Element of the carrier of V
2 * (1 - (1 / 2)) is ext-real V14() V15() Element of REAL
(2 * (1 - (1 / 2))) * a is Element of the carrier of V
((2 * (1 - (1 / 2))) * a) + (2 * ((1 / 2) * u1)) is Element of the carrier of V
2 - 1 is ext-real V14() V15() Element of REAL
(2 - 1) * a is Element of the carrier of V
2 * (1 / 2) is ext-real non negative V14() V15() Element of REAL
(2 * (1 / 2)) * u1 is Element of the carrier of V
((2 - 1) * a) + ((2 * (1 / 2)) * u1) is Element of the carrier of V
1 * u1 is Element of the carrier of V
a + (1 * u1) is Element of the carrier of V
a + u1 is Element of the carrier of V
N is set
x is Element of the carrier of V
y is Element of the carrier of V
x + y is Element of the carrier of V
u1 is Element of the carrier of V
a is ext-real V14() V15() Element of REAL
a * u1 is Element of the carrier of V
x is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M
Sum x is Element of the carrier of V
N is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() Subspace of V
(V,M) is non empty Element of K11( the carrier of V)
the carrier of V is non empty set
K11( the carrier of V) is non empty set
the carrier of M is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
N is Element of the carrier of V
x is Element of the carrier of V
N + x is Element of the carrier of V
y is ext-real V14() V15() Element of REAL
y * N is Element of the carrier of V
a is Element of the carrier of V
y * a is Element of the carrier of V
u1 is Element of the carrier of V
a + u1 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
M is non empty (V) Element of K11( the carrier of V)
Lin M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
the carrier of (Lin M) is non empty set
N is set
x is Element of the carrier of V
y is Element of the carrier of V
x + y is Element of the carrier of V
u1 is Element of the carrier of V
a is ext-real V14() V15() Element of REAL
a * u1 is Element of the carrier of V
x is V16() V19( the carrier of V) V20( REAL ) Function-like quasi_total Linear_Combination of M
Sum x is Element of the carrier of V
N is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like Subspace of V
(V,M) is non empty Element of K11( the carrier of V)
the carrier of V is non empty set
K11( the carrier of V) is non empty set
the carrier of M is non empty set
0. V is V64(V) Element of the carrier of V
the ZeroF of V is Element of the carrier of V
N is Element of the carrier of V
x is Element of the carrier of V
N + x is Element of the carrier of V
y is ext-real V14() V15() Element of REAL
y * N is Element of the carrier of V
a is Element of the carrier of V
y * a is Element of the carrier of V
u1 is Element of the carrier of V
a + u1 is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K11( the carrier of V) is non empty set
N is Element of the carrier of V
M is Element of K11( the carrier of V)
{ (N + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
y is set
a is set
a is Element of K11( the carrier of V)
u1 is Element of K11( the carrier of V)
v1 is set
u2 is Element of the carrier of V
N + u2 is Element of the carrier of V
v1 is set
u2 is Element of the carrier of V
N + u2 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() Subspace of V
(V,M) is non empty Element of K11( the carrier of V)
the carrier of M is non empty set
N is Element of K11( the carrier of V)
x is Element of the carrier of V
x + M is Element of K11( the carrier of V)
(V,N,x) is Element of K11( the carrier of V)
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in N } is set
y is set
a is Element of the carrier of V
x + a is Element of the carrier of V
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
y is set
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
a is Element of the carrier of V
x + a is Element of the carrier of V
V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is (V) Element of K11( the carrier of V)
N is Element of the carrier of V
(V,M,N) is Element of K11( the carrier of V)
{ (N + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
x is Element of the carrier of V
y is Element of the carrier of V
a is ext-real V14() V15() Element of REAL
1 - a is ext-real V14() V15() Element of REAL
(1 - a) * x is Element of the carrier of V
a * y is Element of the carrier of V
((1 - a) * x) + (a * y) is Element of the carrier of V
u1 is Element of the carrier of V
N + u1 is Element of the carrier of V
v1 is Element of the carrier of V
N + v1 is Element of the carrier of V
(1 - a) * N is Element of the carrier of V
(1 - a) * u1 is Element of the carrier of V
((1 - a) * N) + ((1 - a) * u1) is Element of the carrier of V
a * (N + v1) is Element of the carrier of V
(((1 - a) * N) + ((1 - a) * u1)) + (a * (N + v1)) is Element of the carrier of V
a * N is Element of the carrier of V
a * v1 is Element of the carrier of V
(a * N) + (a * v1) is Element of the carrier of V
(((1 - a) * N) + ((1 - a) * u1)) + ((a * N) + (a * v1)) is Element of the carrier of V
(((1 - a) * N) + ((1 - a) * u1)) + (a * N) is Element of the carrier of V
((((1 - a) * N) + ((1 - a) * u1)) + (a * N)) + (a * v1) is Element of the carrier of V
((1 - a) * N) + (a * N) is Element of the carrier of V
((1 - a) * u1) + (((1 - a) * N) + (a * N)) is Element of the carrier of V
(((1 - a) * u1) + (((1 - a) * N) + (a * N))) + (a * v1) is Element of the carrier of V
(1 - a) + a is ext-real V14() V15() Element of REAL
((1 - a) + a) * N is Element of the carrier of V
((1 - a) * u1) + (((1 - a) + a) * N) is Element of the carrier of V
(((1 - a) * u1) + (((1 - a) + a) * N)) + (a * v1) is Element of the carrier of V
((1 - a) * u1) + N is Element of the carrier of V
(((1 - a) * u1) + N) + (a * v1) is Element of the carrier of V
((1 - a) * u1) + (a * v1) is Element of the carrier of V
N + (((1 - a) * u1) + (a * v1)) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() RealUnitarySpace-like UNITSTR
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V115() strict RealUnitarySpace-like Subspace of V
(V,M) is non empty Element of K11( the carrier of V)
the carrier of M is non empty set
N is Element of K11( the carrier of V)
x is Element of the carrier of V
x + M is Element of K11( the carrier of V)
(V,N,x) is Element of K11( the carrier of V)
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in N } is set
y is set
a is Element of the carrier of V
x + a is Element of the carrier of V
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
y is set
{ (x + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
a is Element of the carrier of V
x + a is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
N is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in N ) } is set
{ H₁(b₁,b₂) where b₁, b₂ is Element of the carrier of V : S₁[b₁,b₂] } is set
V is non empty Abelian addLoopStr
the carrier of V is non empty set
K11( the carrier of V) is non empty set
x is Element of K11( the carrier of V)
y is Element of K11( the carrier of V)
(V,x,y) is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in x & b₂ in y ) } is set
(V,y,x) is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in y & b₂ in x ) } is set
a is set
u1 is Element of the carrier of V
v1 is Element of the carrier of V
u1 + v1 is Element of the carrier of V
a is set
u1 is Element of the carrier of V
v1 is Element of the carrier of V
u1 + v1 is Element of the carrier of V
V is non empty addLoopStr
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is Element of K11( the carrier of V)
N is Element of the carrier of V
{N} is non empty V5() finite 1 -element Element of K11( the carrier of V)
(V,{N},M) is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in {N} & b₂ in M ) } is set
(V,M,N) is Element of K11( the carrier of V)
{ (N + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
x is set
y is Element of the carrier of V
N + y is Element of the carrier of V
x is set
y is Element of the carrier of V
a is Element of the carrier of V
y + a is Element of the carrier of V
V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is (V) Element of K11( the carrier of V)
N is Element of the carrier of V
{N} is non empty V5() finite 1 -element Element of K11( the carrier of V)
(V,{N},M) is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in {N} & b₂ in M ) } is set
(V,M,N) is Element of K11( the carrier of V)
{ (N + b₁) where b₁ is Element of the carrier of V : b₁ in M } is set
V is non empty RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is (V) Element of K11( the carrier of V)
N is (V) Element of K11( the carrier of V)
M /\ N is Element of K11( the carrier of V)
x is Element of the carrier of V
y is Element of the carrier of V
a is ext-real V14() V15() Element of REAL
1 - a is ext-real V14() V15() Element of REAL
(1 - a) * x is Element of the carrier of V
a * y is Element of the carrier of V
((1 - a) * x) + (a * y) is Element of the carrier of V
V is non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
K11( the carrier of V) is non empty set
M is (V) Element of K11( the carrier of V)
N is (V) Element of K11( the carrier of V)
(V,M,N) is Element of K11( the carrier of V)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in N ) } is set
x is Element of the carrier of V
y is Element of the carrier of V
a is ext-real V14() V15() Element of REAL
1 - a is ext-real V14() V15() Element of REAL
(1 - a) * x is Element of the carrier of V
a * y is Element of the carrier of V
((1 - a) * x) + (a * y) is Element of the carrier of V
u1 is Element of the carrier of V
v1 is Element of the carrier of V
u1 + v1 is Element of the carrier of V
u2 is Element of the carrier of V
v2 is Element of the carrier of V
u2 + v2 is Element of the carrier of V
(1 - a) * u1 is Element of the carrier of V
(1 - a) * v1 is Element of the carrier of V
((1 - a) * u1) + ((1 - a) * v1) is Element of the carrier of V
a * (u2 + v2) is Element of the carrier of V
(((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2)) is Element of the carrier of V
a * u2 is Element of the carrier of V
a * v2 is Element of the carrier of V
(a * u2) + (a * v2) is Element of the carrier of V
(((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2)) is Element of the carrier of V
(((1 - a) * u1) + ((1 - a) * v1)) + (a * u2) is Element of the carrier of V
((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2) is Element of the carrier of V
((1 - a) * u1) + (a * u2) is Element of the carrier of V
((1 - a) * v1) + (((1 - a) * u1) + (a * u2)) is Element of the carrier of V
(((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2) is Element of the carrier of V
((1 - a) * v1) + (a * v2) is Element of the carrier of V
(((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2)) is Element of the carrier of V