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

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

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 0. GF } is set

Carrier c6 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c6 . b1 = 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
c6 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

Carrier c6 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c6 . b1 = 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
c6 . l is Element of the carrier of GF
v is set

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

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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
c6 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:]
c6 . A is Element of the carrier of GF
c6 . 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

Carrier l is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set
x is set
f is Element of the carrier of V
l . f is Element of the carrier of GF

Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 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

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
{ b1 where b1 is Element of the carrier of V : not B . b1 = 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
c6 is Element of the carrier of GF
c6 * B is Element of the carrier of V
(B * A) + (c6 * B) is Element of the carrier of V
B " is Element of the carrier of GF
(B ") * ((B * A) + (c6 * B)) is Element of the carrier of V
(B ") * (B * A) is Element of the carrier of V
(B ") * (c6 * B) is Element of the carrier of V
((B ") * (B * A)) + ((B ") * (c6 * 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 ") * (c6 * B)) is Element of the carrier of V
(B ") * c6 is Element of the carrier of GF
((B ") * c6) * B is Element of the carrier of V
(((B ") * B) * A) + (((B ") * c6) * 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 ") * c6) * B) is Element of the carrier of V
A + (((B ") * c6) * B) is Element of the carrier of V
- (((B ") * c6) * B) is Element of the carrier of V
- (1_ GF) is Element of the carrier of GF
(- (1_ GF)) * (((B ") * c6) * B) is Element of the carrier of V
(- (1_ GF)) * ((B ") * c6) is Element of the carrier of GF
((- (1_ GF)) * ((B ") * c6)) * B is Element of the carrier of V
c6 " is Element of the carrier of GF
(c6 ") * ((B * A) + (c6 * B)) is Element of the carrier of V
(c6 ") * (B * A) is Element of the carrier of V
(c6 ") * (c6 * B) is Element of the carrier of V
((c6 ") * (B * A)) + ((c6 ") * (c6 * B)) is Element of the carrier of V
(c6 ") * B is Element of the carrier of GF
((c6 ") * B) * A is Element of the carrier of V
(((c6 ") * B) * A) + ((c6 ") * (c6 * B)) is Element of the carrier of V
(c6 ") * c6 is Element of the carrier of GF
((c6 ") * c6) * B is Element of the carrier of V
(((c6 ") * B) * A) + (((c6 ") * c6) * 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
(((c6 ") * B) * A) + ((1_ GF) * B) is Element of the carrier of V
(((c6 ") * B) * A) + B is Element of the carrier of V
- (((c6 ") * B) * A) is Element of the carrier of V
- (1_ GF) is Element of the carrier of GF
(- (1_ GF)) * (((c6 ") * B) * A) is Element of the carrier of V
(- (1_ GF)) * ((c6 ") * B) is Element of the carrier of GF
((- (1_ GF)) * ((c6 ") * 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 b1) where b1 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

Sum c6 is Element of the carrier 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

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

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

Sum x is Element of the carrier of V

Sum f is Element of the carrier of V

Sum c6 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 b1) where b1 is Relation-like the carrier of A -defined the carrier of V -valued Function-like quasi_total Linear_Combination of B : verum } is set

Sum B is Element of the carrier of A
{ (Sum b1) where b1 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
c6 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:]
c6 . 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

Carrier l is finite Element of bool the carrier of A
{ b1 where b1 is Element of the carrier of A : not l . b1 = 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

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
{ b1 where b1 is Element of the carrier of A : not x . b1 = 0. V } is set

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 b1) where b1 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

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

Sum c6 is Element of the carrier of V

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

Sum c6 is Element of the carrier of V
Carrier c6 is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not c6 . b1 = 0. GF } is set
(Carrier c6) \ A is finite Element of bool the carrier of V
(Carrier c6) /\ 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
c6 . 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

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 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
c6 . 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

Carrier u is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not u . b1 = 0. GF } is set
g is set
v is Element of the carrier of V
u . v is Element of the carrier of GF

v is Element of the carrier of V
c6 . 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
(c6 . v) + (g . v) is Element of the carrier of GF
(c6 . 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
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in B ) } is set

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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set

dom x is set
rng x is set
f is non empty set
union f is set

g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is set
g is set

g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union () is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } 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
c6 is Element of bool the carrier of V
(GF,V,c6) 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
c6 \/ {v} is non empty Element of bool the carrier 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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 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
() \ {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

Carrier f is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not f . b1 = 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

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. GF } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of GF

Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier 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
{ b1 where b1 is Element of bool the carrier of V : ( a1 in b1 & b1 in B ) } is set
the carrier of GF is non empty non trivial set

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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 0. GF } is set

dom x is set
rng x is set
f is non empty set
union f is set

g is set
x . g is set
g is set
g is Element of bool the carrier of V
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set

g is set
g is set

g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } is set
g is Element of bool the carrier of V
g is set
g is set
union () is set
g is Element of bool the carrier of V
g is set
x . g is set
{ b1 where b1 is Element of bool the carrier of V : ( g in b1 & b1 in B ) } 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
c6 is Element of bool the carrier of V
(GF,V,c6) is non empty V68() strict V105(GF) V106(GF) V107(GF) V108(GF) V115() V116() V117() Subspace of V
the carrier of (GF,V,c6) is non empty set
l is Element of the carrier of V
the carrier of GF is non empty non trivial set

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
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0. GF } is set
f is set
f is Element of the carrier of V
v is Element of bool the carrier 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
c6 \/ {v} is non empty Element of bool the carrier 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
{ b1 where b1 is Element of the carrier of V : not l . b1 = 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
() \ {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

Carrier f is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not f . b1 = 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

Carrier g is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not g . b1 = 0. GF } is set
g is set
u is Element of the carrier of V
g . u is Element of the carrier of GF

Sum g is Element of the carrier of V
(- (l . v)) * v is Element of the carrier 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)