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

c

Carrier c

{ b

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

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

Carrier c

{ b

{(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

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

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

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

c

c

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

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

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

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

c

(B * A) + (c

B " is Element of the carrier of GF

(B ") * ((B * A) + (c

(B ") * (B * A) is Element of the carrier of V

(B ") * (c

((B ") * (B * A)) + ((B ") * (c

(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 ") * c

((B ") * c

(((B ") * B) * A) + (((B ") * c

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

A + (((B ") * c

- (((B ") * c

- (1_ GF) is Element of the carrier of GF

(- (1_ GF)) * (((B ") * c

(- (1_ GF)) * ((B ") * c

((- (1_ GF)) * ((B ") * c

c

(c

(c

(c

((c

(c

((c

(((c

(c

((c

(((c

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

(((c

- (((c

- (1_ GF) is Element of the carrier of GF

(- (1_ GF)) * (((c

(- (1_ GF)) * ((c

((- (1_ GF)) * ((c

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

B is set

c

Sum c

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

Sum c

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

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

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

c

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

{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

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

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

Sum c

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

Sum c

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

Sum c

Carrier c

{ b

(Carrier c

(Carrier c

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

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

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

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

(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

(c

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

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

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

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

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

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

(GF,V,c

(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

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c

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

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

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

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

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

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

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

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

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

(GF,V,c

the carrier of (GF,V,c

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

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

l is Relation-like the carrier of V -defined the carrier of GF -valued Function-like quasi_total Linear_Combination of c

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

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

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

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)