:: VECTSP_7 semantic presentation

K137() is Element of bool K133()
K133() is set
bool K133() is non empty set
omega is set
bool omega is non empty set
bool K137() is non empty set
{} is empty finite V35() set
the empty finite V35() set is empty finite V35() set
1 is non empty set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
B is Element of bool the carrier of V
the carrier of GF is non empty non trivial set
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum B is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. GF } is set
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of B
Carrier c₆ is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not c₆ . b₁ = 0. GF } is set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
the carrier of GF is non empty non trivial set
[: the carrier of V, the carrier of GF:] is non empty set
bool [: the carrier of V, the carrier of GF:] is non empty set
1_ GF is Element of the carrier of GF
1. GF is V47(GF) Element of the carrier of GF
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
B . (0. V) is Element of the carrier of GF
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
{(0. V)} is non empty finite Element of bool the carrier of V
c₆ is non empty finite Element of bool the carrier of V
v is Element of the carrier of V
B . v is Element of the carrier of GF
v is finite Element of bool the carrier of V
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier c₆ is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not c₆ . b₁ = 0. GF } is set
{(0. V)} is non empty finite Element of bool the carrier of V
v is set
l is Element of the carrier of V
c₆ . l is Element of the carrier of GF
v is set
v is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum v is Element of the carrier of V
v . (0. V) is Element of the carrier of GF
(v . (0. V)) * (0. V) is Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
the carrier of GF is non empty non trivial set
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum B is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. GF } is set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
{} V is empty proper finite V35() (GF,V) Element of bool the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
{A} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
the carrier of GF is non empty non trivial set
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {A}
Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. GF } is set
B . A is Element of the carrier of GF
(B . A) * A is Element of the carrier of V
B is Element of the carrier of V
B . B is Element of the carrier of GF
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
the carrier of GF is non empty non trivial set
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
0. GF is V47(GF) Element of the carrier of GF
B is Element of the carrier of GF
B * B is Element of the carrier of V
[: the carrier of V, the carrier of GF:] is non empty set
bool [: the carrier of V, the carrier of GF:] is non empty set
1_ GF is Element of the carrier of GF
1. GF is V47(GF) Element of the carrier of GF
- (1_ GF) is Element of the carrier of GF
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
c₆ . A is Element of the carrier of GF
c₆ . B is Element of the carrier of GF
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
l is Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
v . l is Element of the carrier of GF
l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier l is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. GF } is set
x is set
f is Element of the carrier of V
l . f is Element of the carrier of GF
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {A,B}
Carrier x is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not x . b₁ = 0. GF } is set
Sum x is Element of the carrier of V
(- (1_ GF)) * (B * B) is Element of the carrier of V
((- (1_ GF)) * (B * B)) + (B * B) is Element of the carrier of V
- (B * B) is Element of the carrier of V
(- (B * B)) + (B * B) is Element of the carrier of V
(B * B) - (B * B) is Element of the carrier of V
- ((B * B) - (B * B)) is Element of the carrier of V
- (0. V) is Element of the carrier of V
1_ GF is Element of the carrier of GF
1. GF is V47(GF) Element of the carrier of GF
(1_ GF) * B is Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {A,B}
Sum B is Element of the carrier of V
Carrier B is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not B . b₁ = 0. GF } is set
B . A is Element of the carrier of GF
(B . A) * A is Element of the carrier of V
B . B is Element of the carrier of GF
(B . B) * B is Element of the carrier of V
((B . A) * A) + ((B . B) * B) is Element of the carrier of V
the Element of Carrier B is Element of Carrier B
(B . A) " is Element of the carrier of GF
((B . A) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . A) ") * ((B . A) * A) is Element of the carrier of V
((B . A) ") * ((B . B) * B) is Element of the carrier of V
(((B . A) ") * ((B . A) * A)) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . A) is Element of the carrier of GF
(((B . A) ") * (B . A)) * A is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + (((B . A) ") * ((B . B) * B)) is Element of the carrier of V
((B . A) ") * (B . B) is Element of the carrier of GF
(((B . A) ") * (B . B)) * B is Element of the carrier of V
((((B . A) ") * (B . A)) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(1_ GF) * A is Element of the carrier of V
((1_ GF) * A) + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
A + ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
- ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
- (1_ GF) is Element of the carrier of GF
(- (1_ GF)) * ((((B . A) ") * (B . B)) * B) is Element of the carrier of V
(- (1_ GF)) * (((B . A) ") * (B . B)) is Element of the carrier of GF
((- (1_ GF)) * (((B . A) ") * (B . B))) * B is Element of the carrier of V
(B . B) " is Element of the carrier of GF
((B . B) ") * (((B . A) * A) + ((B . B) * B)) is Element of the carrier of V
((B . B) ") * ((B . A) * A) is Element of the carrier of V
((B . B) ") * ((B . B) * B) is Element of the carrier of V
(((B . B) ") * ((B . A) * A)) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((B . B) ") * (B . A) is Element of the carrier of GF
(((B . B) ") * (B . A)) * A is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + (((B . B) ") * ((B . B) * B)) is Element of the carrier of V
((B . B) ") * (B . B) is Element of the carrier of GF
(((B . B) ") * (B . B)) * B is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + ((((B . B) ") * (B . B)) * B) is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + ((1_ GF) * B) is Element of the carrier of V
((((B . B) ") * (B . A)) * A) + B is Element of the carrier of V
(0. GF) * A is Element of the carrier of V
((0. GF) * A) + B is Element of the carrier of V
(0. V) + B is Element of the carrier of V
v is Element of the carrier of V
B . v is Element of the carrier of GF
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
the carrier of GF is non empty non trivial set
0. GF is V47(GF) Element of the carrier of GF
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
A is Element of the carrier of V
B is Element of the carrier of V
{A,B} is non empty finite Element of bool the carrier of V
bool the carrier of V is non empty set
B is Element of the carrier of GF
B * A is Element of the carrier of V
c₆ is Element of the carrier of GF
c₆ * B is Element of the carrier of V
(B * A) + (c₆ * B) is Element of the carrier of V
B " is Element of the carrier of GF
(B ") * ((B * A) + (c₆ * B)) is Element of the carrier of V
(B ") * (B * A) is Element of the carrier of V
(B ") * (c₆ * B) is Element of the carrier of V
((B ") * (B * A)) + ((B ") * (c₆ * B)) is Element of the carrier of V
(B ") * B is Element of the carrier of GF
((B ") * B) * A is Element of the carrier of V
(((B ") * B) * A) + ((B ") * (c₆ * B)) is Element of the carrier of V
(B ") * c₆ is Element of the carrier of GF
((B ") * c₆) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c₆) * B) is Element of the carrier of V
1_ GF is Element of the carrier of GF
1. GF is V47(GF) Element of the carrier of GF
(1_ GF) * A is Element of the carrier of V
((1_ GF) * A) + (((B ") * c₆) * B) is Element of the carrier of V
A + (((B ") * c₆) * B) is Element of the carrier of V
- (((B ") * c₆) * B) is Element of the carrier of V
- (1_ GF) is Element of the carrier of GF
(- (1_ GF)) * (((B ") * c₆) * B) is Element of the carrier of V
(- (1_ GF)) * ((B ") * c₆) is Element of the carrier of GF
((- (1_ GF)) * ((B ") * c₆)) * B is Element of the carrier of V
c₆ " is Element of the carrier of GF
(c₆ ") * ((B * A) + (c₆ * B)) is Element of the carrier of V
(c₆ ") * (B * A) is Element of the carrier of V
(c₆ ") * (c₆ * B) is Element of the carrier of V
((c₆ ") * (B * A)) + ((c₆ ") * (c₆ * B)) is Element of the carrier of V
(c₆ ") * B is Element of the carrier of GF
((c₆ ") * B) * A is Element of the carrier of V
(((c₆ ") * B) * A) + ((c₆ ") * (c₆ * B)) is Element of the carrier of V
(c₆ ") * c₆ is Element of the carrier of GF
((c₆ ") * c₆) * B is Element of the carrier of V
(((c₆ ") * B) * A) + (((c₆ ") * c₆) * B) is Element of the carrier of V
1_ GF is Element of the carrier of GF
1. GF is V47(GF) Element of the carrier of GF
(1_ GF) * B is Element of the carrier of V
(((c₆ ") * B) * A) + ((1_ GF) * B) is Element of the carrier of V
(((c₆ ") * B) * A) + B is Element of the carrier of V
- (((c₆ ") * B) * A) is Element of the carrier of V
- (1_ GF) is Element of the carrier of GF
(- (1_ GF)) * (((c₆ ") * B) * A) is Element of the carrier of V
(- (1_ GF)) * ((c₆ ") * B) is Element of the carrier of GF
((- (1_ GF)) * ((c₆ ") * B)) * A is Element of the carrier of V
B is Element of the carrier of GF
B * B is Element of the carrier of V
(0. V) + (B * B) is Element of the carrier of V
A - (B * B) is Element of the carrier of V
- B is Element of the carrier of GF
(- B) * B is Element of the carrier of V
A + ((- B) * B) is Element of the carrier of V
1. GF is V47(GF) Element of the carrier of GF
(1. GF) * A is Element of the carrier of V
((1. GF) * A) + ((- B) * B) is Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
(0. GF) * A is Element of the carrier of V
((0. GF) * A) + (0. V) is Element of the carrier of V
(1. GF) * B is Element of the carrier of V
((0. GF) * A) + ((1. GF) * B) is Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
the carrier of GF is non empty non trivial set
A is Element of bool the carrier of V
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A : verum } is set
B is set
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
ZeroLC V is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
B is Element of bool the carrier of V
v is Element of the carrier of V
l is Element of the carrier of V
v + l is Element of the carrier of V
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum x is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
x + f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
v is Element of the carrier of GF
l is Element of the carrier of V
v * l is Element of the carrier of V
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum x is Element of the carrier of V
v * x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum f is Element of the carrier of V
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
B is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the carrier of B is non empty set
B is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the carrier of B is non empty set
GF is set
V is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
the carrier of V is non empty non trivial set
A is non empty V68() V105(V) V106(V) V107(V) V108(V) V115() V116() V117() VectSpStr over V
the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A
(V,A,B) is non empty V68() strict V105(V) V106(V) V107(V) V108(V) V115() V116() V117() Subspace of A
the carrier of (V,A,B) is non empty set
{ (Sum b₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set
B is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B
Sum B is Element of the carrier of A
{ (Sum b₁) where b₁ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set
the carrier of (V,A,B) is non empty set
GF is set
V is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
A is non empty V68() V105(V) V106(V) V107(V) V108(V) V115() V116() V117() VectSpStr over V
the carrier of A is non empty set
bool the carrier of A is non empty set
B is Element of bool the carrier of A
(V,A,B) is non empty V68() strict V105(V) V106(V) V107(V) V108(V) V115() V116() V117() Subspace of A
0. V is V47(V) Element of the carrier of V
the carrier of V is non empty non trivial set
[: the carrier of A, the carrier of V:] is non empty set
bool [: the carrier of A, the carrier of V:] is non empty set
B is Element of the carrier of A
1_ V is Element of the carrier of V
1. V is V47(V) Element of the carrier of V
c₆ is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of bool [: the carrier of A, the carrier of V:]
c₆ . B is Element of the carrier of V
Funcs ( the carrier of A, the carrier of V) is non empty FUNCTION_DOMAIN of the carrier of A, the carrier of V
v is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Element of Funcs ( the carrier of A, the carrier of V)
{B} is non empty finite Element of bool the carrier of A
l is non empty finite Element of bool the carrier of A
x is Element of the carrier of A
v . x is Element of the carrier of V
x is finite Element of bool the carrier of A
l is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of A
Carrier l is finite Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not l . b₁ = 0. V } is set
{B} is non empty finite Element of bool the carrier of A
x is set
f is Element of the carrier of A
l . f is Element of the carrier of V
x is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of {B}
Sum x is Element of the carrier of A
(1_ V) * B is Element of the carrier of A
Carrier x is finite Element of bool the carrier of A
{ b₁ where b₁ is Element of the carrier of A : not x . b₁ = 0. V } is set
f is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B
Sum f is Element of the carrier of A
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
{} the carrier of V is empty proper finite V35() (GF,V) Element of bool the carrier of V
bool the carrier of V is non empty set
(GF,V,({} the carrier of V)) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(0). V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of the carrier of V
the carrier of (GF,V,({} the carrier of V)) is non empty set
the carrier of GF is non empty non trivial set
{ (Sum b₁) where b₁ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {} the carrier of V : verum } is set
0. V is V47(V) Element of the carrier of V
B is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {} the carrier of V
Sum B is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
(0). V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
0. V is V47(V) Element of the carrier of V
{(0. V)} is non empty finite Element of bool the carrier of V
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is set
the Element of A is Element of A
B is set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the carrier of B is non empty set
0. GF is V47(GF) Element of the carrier of GF
the carrier of GF is non empty non trivial set
1. GF is V47(GF) Element of the carrier of GF
B is Element of the carrier of V
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(Omega). V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of GF, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty non trivial set
[: the carrier of GF, the carrier of V:] is non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over GF
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of bool the carrier of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of the carrier of V
the carrier of GF is non empty non trivial set
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum c₆ is Element of the carrier of V
v is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of B
Sum v is Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of bool the carrier of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of bool the carrier of V
A \/ B is Element of bool the carrier of V
(GF,V,(A \/ B)) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(GF,V,A) + (GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
0. GF is V47(GF) Element of the carrier of GF
the carrier of GF is non empty non trivial set
B is Element of the carrier of V
c₆ is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A \/ B
Sum c₆ is Element of the carrier of V
Carrier c₆ is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not c₆ . b₁ = 0. GF } is set
(Carrier c₆) \ A is finite Element of bool the carrier of V
(Carrier c₆) /\ A is finite Element of bool the carrier of V
x is set
[: the carrier of V, the carrier of GF:] is non empty set
bool [: the carrier of V, the carrier of GF:] is non empty set
f is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
f . f is Element of the carrier of GF
c₆ . x is set
f is finite Element of bool the carrier of V
f is set
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
x is finite Element of bool the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
g is Element of the carrier of V
f . g is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier g is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. GF } is set
g is set
g is Element of the carrier of V
g . g is Element of the carrier of GF
g is set
g is Element of the carrier of V
u is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
u . g is Element of the carrier of GF
c₆ . g is set
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
u is Element of the carrier of V
g . u is Element of the carrier of GF
u is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier u is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not u . b₁ = 0. GF } is set
g is set
v is Element of the carrier of V
u . v is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of B
g + g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
v is Element of the carrier of V
c₆ . v is Element of the carrier of GF
(g + g) . v is Element of the carrier of GF
g . v is Element of the carrier of GF
g . v is Element of the carrier of GF
(g . v) + (g . v) is Element of the carrier of GF
(c₆ . v) + (g . v) is Element of the carrier of GF
(c₆ . v) + (0. GF) is Element of the carrier of GF
g . v is Element of the carrier of GF
g . v is Element of the carrier of GF
(g . v) + (g . v) is Element of the carrier of GF
(g . v) + (0. GF) is Element of the carrier of GF
g . v is Element of the carrier of GF
g . v is Element of the carrier of GF
(g . v) + (g . v) is Element of the carrier of GF
(0. GF) + (g . v) is Element of the carrier of GF
(0. GF) + (0. GF) is Element of the carrier of GF
Sum g is Element of the carrier of V
Sum g is Element of the carrier of V
(Sum g) + (Sum g) is Element of the carrier of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of bool the carrier of V
A /\ B is Element of bool the carrier of V
(GF,V,(A /\ B)) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(GF,V,A) /\ (GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of GF, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty non trivial set
[: the carrier of GF, the carrier of V:] is non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over GF
A is Element of bool the carrier of V
B is set
B is set
union B is set
v is set
l is set
v is Element of bool the carrier of V
{ b₁ where b₁ is Element of bool the carrier of V : ( a₁ in b₁ & b₁ in B ) } is set
l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of v
Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. GF } is set
x is Relation-like Function-like set
dom x is set
rng x is set
f is non empty set
union f is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f
rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set
g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
dom the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set
g is set
g is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . g is set
g is set
x . g is set
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union (rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f) is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . (x . g) is set
g is Element of bool the carrier of V
the Element of B is Element of B
x is Element of bool the carrier of V
B is set
c₆ is Element of bool the carrier of V
(GF,V,c₆) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
(Omega). V is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
v is Element of the carrier of V
{v} is non empty finite Element of bool the carrier of V
c₆ \/ {v} is non empty Element of bool the carrier of V
l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c₆ \/ {v}
Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. GF } is set
l . v is Element of the carrier of GF
- (l . v) is Element of the carrier of GF
[: the carrier of V, the carrier of GF:] is non empty set
bool [: the carrier of V, the carrier of GF:] is non empty set
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
x . v is Element of the carrier of GF
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
f is Element of the carrier of V
(Carrier l) \ {v} is finite Element of bool the carrier of V
l . f is Element of the carrier of GF
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
f . f is Element of the carrier of GF
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier f is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. GF } is set
f is set
g is Element of the carrier of V
f . g is Element of the carrier of GF
l . g is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
g . v is Element of the carrier of GF
g is Element of the carrier of V
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
g . g is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier g is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. GF } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {v}
Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c₆
f - g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
- g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
1. GF is V47(GF) Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(- (1. GF)) * g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is Element of the carrier of GF
l . u is Element of the carrier of GF
f . u is Element of the carrier of GF
g . u is Element of the carrier of GF
(f . u) - (g . u) is Element of the carrier of GF
- (- (l . v)) is Element of the carrier of GF
(0. GF) + (- (- (l . v))) is Element of the carrier of GF
(l . v) + (0. GF) is Element of the carrier of GF
f . u is Element of the carrier of GF
g . u is Element of the carrier of GF
(f . u) - (g . u) is Element of the carrier of GF
(l . u) - (g . u) is Element of the carrier of GF
(l . u) - (0. GF) is Element of the carrier of GF
Sum f is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
(0. V) + (Sum g) is Element of the carrier of V
(- (l . v)) " is Element of the carrier of GF
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
((- (l . v)) ") * (- (l . v)) is Element of the carrier of GF
(((- (l . v)) ") * (- (l . v))) * v is Element of the carrier of V
1_ GF is Element of the carrier of GF
(1_ GF) * v is Element of the carrier of V
x is set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is set
B is set
union B is set
v is set
l is set
v is Element of bool the carrier of V
{ b₁ where b₁ is Element of bool the carrier of V : ( a₁ in b₁ & b₁ in B ) } is set
the carrier of GF is non empty non trivial set
l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of v
Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. GF } is set
x is Relation-like Function-like set
dom x is set
rng x is set
f is non empty set
union f is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f
rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set
g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
dom the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f is set
g is set
g is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . g is set
g is set
x . g is set
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union (rng the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f) is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b₁ where b₁ is Element of bool the carrier of V : ( g in b₁ & b₁ in B ) } is set
the Relation-like f -defined union f -valued Function-like quasi_total Choice_Function of f . (x . g) is set
g is Element of bool the carrier of V
l is set
x is set
f is Element of bool the carrier of V
{} the carrier of V is empty proper finite V35() (GF,V) Element of bool the carrier of V
B is set
c₆ is Element of bool the carrier of V
(GF,V,c₆) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the carrier of (GF,V,c₆) is non empty set
l is Element of the carrier of V
the carrier of GF is non empty non trivial set
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of A
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
0. GF is V47(GF) Element of the carrier of GF
{ b₁ where b₁ is Element of the carrier of V : not x . b₁ = 0. GF } is set
f is set
f is Element of the carrier of V
v is Element of bool the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of v
Sum f is Element of the carrier of V
(GF,V,v) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
v is Element of the carrier of V
v is Element of the carrier of V
{v} is non empty finite Element of bool the carrier of V
c₆ \/ {v} is non empty Element of bool the carrier of V
l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c₆ \/ {v}
Sum l is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
Carrier l is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not l . b₁ = 0. GF } is set
l . v is Element of the carrier of GF
- (l . v) is Element of the carrier of GF
[: the carrier of V, the carrier of GF:] is non empty set
bool [: the carrier of V, the carrier of GF:] is non empty set
x is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
x . v is Element of the carrier of GF
Funcs ( the carrier of V, the carrier of GF) is non empty FUNCTION_DOMAIN of the carrier of V, the carrier of GF
f is Element of the carrier of V
(Carrier l) \ {v} is finite Element of bool the carrier of V
l . f is Element of the carrier of GF
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
f . f is Element of the carrier of GF
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier f is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not f . b₁ = 0. GF } is set
f is set
g is Element of the carrier of V
f . g is Element of the carrier of GF
l . g is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of bool [: the carrier of V, the carrier of GF:]
g . v is Element of the carrier of GF
g is Element of the carrier of V
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Element of Funcs ( the carrier of V, the carrier of GF)
g . g is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
Carrier g is finite Element of bool the carrier of V
{ b₁ where b₁ is Element of the carrier of V : not g . b₁ = 0. GF } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of GF
g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of {v}
Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier of V
f is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c₆
f - g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
- g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
1. GF is V47(GF) Element of the carrier of GF
- (1. GF) is Element of the carrier of GF
(- (1. GF)) * g is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
f + (- g) is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of V
u is Element of the carrier of V
(f - g) . u is Element of the carrier of GF
l . u is Element of the carrier of GF
f . u is Element of the carrier of GF
g . u is Element of the carrier of GF
(f . u) - (g . u) is Element of the carrier of GF
- (- (l . v)) is Element of the carrier of GF
(0. GF) + (- (- (l . v))) is Element of the carrier of GF
(l . v) + (0. GF) is Element of the carrier of GF
f . u is Element of the carrier of GF
g . u is Element of the carrier of GF
(f . u) - (g . u) is Element of the carrier of GF
(l . u) - (g . u) is Element of the carrier of GF
(l . u) - (0. GF) is Element of the carrier of GF
Sum f is Element of the carrier of V
(Sum f) - (Sum g) is Element of the carrier of V
(0. V) + (Sum g) is Element of the carrier of V
(- (l . v)) " is Element of the carrier of GF
((- (l . v)) ") * ((- (l . v)) * v) is Element of the carrier of V
((- (l . v)) ") * (- (l . v)) is Element of the carrier of GF
(((- (l . v)) ") * (- (l . v))) * v is Element of the carrier of V
1_ GF is Element of the carrier of GF
(1_ GF) * v is Element of the carrier of V
x is set
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of GF, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty non trivial set
[: the carrier of GF, the carrier of V:] is non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over GF
{} the carrier of V is empty proper finite V35() (GF,V) Element of bool the carrier of V
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
the U5 of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of GF, the carrier of V:] -defined the carrier of V -valued Function-like quasi_total Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty non trivial set
[: the carrier of GF, the carrier of V:] is non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over GF
B is Element of bool the carrier of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is (GF,V)
GF is non empty non degenerated non trivial V68() V88() unital V94() V96() right-distributive left-distributive right_unital well-unital V102() left_unital V115() V116() V117() L11()
V is non empty V68() V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set
A is Element of bool the carrier of V
(GF,V,A) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is Element of bool the carrier of V
(GF,V,B) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
B is (GF,V)