:: LMOD_7 semantic presentation

K149() is Element of bool K145()

K145() is set

bool K145() is non empty set

K144() is set

bool K144() is non empty set

bool K149() is non empty set

K118(K149()) is V27() set

{} is empty set

the empty set is empty set

1 is non empty set

F

K is Element of F

V is Element of F

W is set

F

[:F

bool [:F

K is V6() V18(F

V is V6() V18(F

W is Element of F

K . W is Element of F

F

V . W is Element of F

F

[:F

[:[:F

bool [:[:F

K is V6() V18([:F

V is V6() V18([:F

W is Element of F

x is Element of F

y is Element of F

K . (W,x,y) is Element of F

F

V . (W,x,y) is Element of F

F

[:F

[:[:F

bool [:[:F

K is V6() V18([:F

V is V6() V18([:F

W is Element of F

x is Element of F

y is Element of F

v is Element of F

K . (W,x,y,v) is Element of F

F

V . (W,x,y,v) is Element of F

F

bool F

F

{ F

K is Element of bool F

F

F

{ b

K is Element of F

F

F

{ b

F

F

F

F

{ b

F

F

{ b

F

K is Element of F

F

F

F

{ b

F

F

{ b

K is Element of F

V is Element of F

K is Element of F

K is non empty right_complementable Abelian add-associative right_zeroed addLoopStr

the carrier of K is non empty set

V is right_complementable Element of the carrier of K

W is right_complementable Element of the carrier of K

V - W is right_complementable Element of the carrier of K

- W is right_complementable Element of the carrier of K

V + (- W) is right_complementable Element of the carrier of K

the addF of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

the addF of K . (V,(- W)) is right_complementable Element of the carrier of K

- (V - W) is right_complementable Element of the carrier of K

- V is right_complementable Element of the carrier of K

(- V) - (- W) is right_complementable Element of the carrier of K

- (- W) is right_complementable Element of the carrier of K

(- V) + (- (- W)) is right_complementable Element of the carrier of K

the addF of K . ((- V),(- (- W))) is right_complementable Element of the carrier of K

x is right_complementable Element of the carrier of K

(V - W) + x is right_complementable Element of the carrier of K

the addF of K . ((V - W),x) is right_complementable Element of the carrier of K

V + x is right_complementable Element of the carrier of K

the addF of K . (V,x) is right_complementable Element of the carrier of K

(V + x) - W is right_complementable Element of the carrier of K

(V + x) + (- W) is right_complementable Element of the carrier of K

the addF of K . ((V + x),(- W)) is right_complementable Element of the carrier of K

(- V) + W is right_complementable Element of the carrier of K

the addF of K . ((- V),W) is right_complementable Element of the carrier of K

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

W is Element of bool the carrier of V

0. K is V55(K) right_complementable Element of the carrier of K

the carrier of K is non empty set

the ZeroF of K is right_complementable Element of the carrier of K

1_ K is right_complementable Element of the carrier of K

K184(K) is right_complementable Element of the carrier of K

the OneF of K is right_complementable Element of the carrier of K

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty set

0. K is V55(K) right_complementable Element of the carrier of K

the ZeroF of K is right_complementable Element of the carrier of K

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is right_complementable Element of the carrier of V

x is Element of bool the carrier of V

y is V6() V18( the carrier of V, the carrier of K) Linear_Combination of x

y . W is right_complementable Element of the carrier of K

Carrier y is V36() Element of bool the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

the carrier of K is non empty set

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

Lin W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

x is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W

Carrier x is V36() Element of bool the carrier of V

the Element of Carrier x is Element of Carrier x

0. K is V55(K) right_complementable Element of the carrier of K

the ZeroF of K is right_complementable Element of the carrier of K

v is right_complementable Element of the carrier of V

x . v is right_complementable Element of the carrier of K

the carrier of (Lin W) is non empty set

x is right_complementable Element of the carrier of (Lin W)

y is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W

Sum y is right_complementable Element of the carrier of V

Carrier y is V36() Element of bool the carrier of V

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

0. (Lin W) is V55( Lin W) right_complementable Element of the carrier of (Lin W)

the ZeroF of (Lin W) is right_complementable Element of the carrier of (Lin W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

{} the carrier of V is empty proper Element of bool the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 right_complementable Element of the carrier of V

the lmult of V is V6() V18([: the carrier of K, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]

the carrier of K is non empty set

[: the carrier of K, the carrier of V:] is non empty set

[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K

Lin W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W is Element of bool the carrier of V

Lin W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

x is Element of bool the carrier of V

W \/ x is Element of bool the carrier of V

Lin x is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(Lin W) /\ (Lin x) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W /\ x is Element of bool the carrier of V

y is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of y is non empty set

the carrier of (Lin W) is non empty set

the carrier of (Lin x) is non empty set

the carrier of (Lin W) /\ the carrier of (Lin x) is set

w is set

the carrier of K is non empty set

a is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W

Sum a is right_complementable Element of the carrier of V

b is V6() V18( the carrier of V, the carrier of K) Linear_Combination of x

Sum b is right_complementable Element of the carrier of V

Carrier a is V36() Element of bool the carrier of V

Carrier b is V36() Element of bool the carrier of V

(Carrier a) \/ (Carrier b) is Element of bool the carrier of V

a - b is V6() V18( the carrier of V, the carrier of K) Linear_Combination of V

Carrier (a - b) is V36() Element of bool the carrier of V

c is V6() V18( the carrier of V, the carrier of K) Linear_Combination of W \/ x

Sum c is right_complementable Element of the carrier of V

(Sum a) - (Sum b) is right_complementable Element of the carrier of V

- (Sum b) is right_complementable Element of the carrier of V

(Sum a) + (- (Sum b)) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . ((Sum a),(- (Sum b))) is right_complementable Element of the carrier of V

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

Carrier c is V36() Element of bool the carrier of V

the Element of Carrier a is Element of Carrier a

0. K is V55(K) right_complementable Element of the carrier of K

the ZeroF of K is right_complementable Element of the carrier of K

b is right_complementable Element of the carrier of V

a . b is right_complementable Element of the carrier of K

c . b is right_complementable Element of the carrier of K

b . b is right_complementable Element of the carrier of K

(a . b) - (b . b) is right_complementable Element of the carrier of K

- (b . b) is right_complementable Element of the carrier of K

(a . b) + (- (b . b)) is right_complementable Element of the carrier of K

the addF of K is V6() V18([: the carrier of K, the carrier of K:], the carrier of K) Element of bool [:[: the carrier of K, the carrier of K:], the carrier of K:]

[: the carrier of K, the carrier of K:] is non empty set

[:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

bool [:[: the carrier of K, the carrier of K:], the carrier of K:] is non empty set

the addF of K . ((a . b),(- (b . b))) is right_complementable Element of the carrier of K

w is set

a is set

{(0. V)} is non empty Element of bool the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is Element of bool the carrier of V

Lin x is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

y is Element of bool the carrier of V

x \/ y is Element of bool the carrier of V

Lin y is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 right_complementable Element of the carrier of V

the lmult of V is V6() V18([: the carrier of K, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of K, the carrier of V:], the carrier of V:]

the carrier of K is non empty set

[: the carrier of K, the carrier of V:] is non empty set

[:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set

bool [:[: the carrier of K, the carrier of V:], the carrier of V:] is non empty set

VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over K

Lin W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(Lin x) + (Lin y) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(Lin x) /\ (Lin y) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

{ the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V} is non empty set

y is set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

Subspaces V is non empty set

W is set

x is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty (K,V)

x is Element of W

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty (K,V)

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,W) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

W is right_complementable Element of the carrier of V

<:W:> is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)

{ the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)} is non empty set

y is set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

(K,V) is non empty (K,V)

{ b

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)

y is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

w is set

v is non empty set

a is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

w is non empty (K,V)

a is set

b is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

a is set

b is set

W is non empty (K,V)

x is non empty (K,V)

y is set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty (K,V)

x is Element of W

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is Element of bool the carrier of V

the Element of x is Element of x

v is right_complementable Element of the carrier of V

{v} is non empty Element of bool the carrier of V

w is Element of bool the carrier of V

x \ w is Element of bool the carrier of V

Lin (x \ w) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

w \/ (x \ w) is Element of bool the carrier of V

Lin w is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

<:v:> is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

c is right_complementable Element of the carrier of V

<:c:> is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)

{ the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)} is non empty set

y is set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

(K,V) is non empty (K,V)

{ b

the non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)

y is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

w is set

v is non empty set

a is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

w is non empty (K,V)

a is set

b is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V)

c is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

a is set

b is set

W is non empty (K,V)

x is non empty (K,V)

y is set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty (K,V)

x is Element of W

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

Subspaces V is non empty set

W is V6() FinSequence-like FinSequence of Subspaces V

SubJoin V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

[:(Subspaces V),(Subspaces V):] is non empty set

[:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

(SubJoin V) $$ W is Element of Subspaces V

(K,V) is non empty (K,V)

SubMeet V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

(SubMeet V) $$ W is Element of Subspaces V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

Subspaces V is non empty set

SubJoin V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

[:(Subspaces V),(Subspaces V):] is non empty set

[:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the_unity_wrt (SubJoin V) is Element of Subspaces V

(K,V) is non empty (K,V)

SubMeet V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

LattStr(# (K,V),(SubJoin V),(SubMeet V) #) is non empty strict LattStr

y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of y is non empty set

[: the carrier of y, the carrier of y:] is non empty set

the L_join of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) commutative associative idempotent Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]

[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set

bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set

@ ((0). V) is Element of Subspaces V

w is Element of (K,V)

a is Element of (K,V)

b is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

(SubJoin V) . (w,a) is Element of (K,V)

c is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

((0). V) + c is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(SubJoin V) . (a,w) is Element of (K,V)

c + ((0). V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

Subspaces V is non empty set

SubMeet V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

[:(Subspaces V),(Subspaces V):] is non empty set

[:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):] is non empty set

(Omega). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the_unity_wrt (SubMeet V) is Element of Subspaces V

(K,V) is non empty (K,V)

SubJoin V is V6() V18([:(Subspaces V),(Subspaces V):], Subspaces V) Element of bool [:[:(Subspaces V),(Subspaces V):],(Subspaces V):]

LattStr(# (K,V),(SubJoin V),(SubMeet V) #) is non empty strict LattStr

y is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr

the carrier of y is non empty set

[: the carrier of y, the carrier of y:] is non empty set

the L_meet of y is V6() V18([: the carrier of y, the carrier of y:], the carrier of y) commutative associative idempotent Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]

[:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set

bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is non empty set

@ ((Omega). V) is Element of Subspaces V

w is Element of (K,V)

a is Element of (K,V)

b is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V))

(SubMeet V) . (w,a) is Element of (K,V)

c is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

((Omega). V) /\ c is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(SubMeet V) . (a,w) is Element of (K,V)

c /\ ((Omega). V) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is Element of bool the carrier of V

{ (b

v is set

w is right_complementable Element of the carrier of V

a is right_complementable Element of the carrier of V

w + a is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (w,a) is right_complementable Element of the carrier of V

v is set

w is right_complementable Element of the carrier of V

a is right_complementable Element of the carrier of V

w + a is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (w,a) is right_complementable Element of the carrier of V

v is Element of bool the carrier of V

w is set

b is right_complementable Element of the carrier of V

c is right_complementable Element of the carrier of V

a is set

b + c is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (b,c) is right_complementable Element of the carrier of V

y is Element of bool the carrier of V

v is Element of bool the carrier of V

w is set

a is right_complementable Element of the carrier of V

b is right_complementable Element of the carrier of V

a + b is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (a,b) is right_complementable Element of the carrier of V

a is right_complementable Element of the carrier of V

b is right_complementable Element of the carrier of V

a + b is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (a,b) is right_complementable Element of the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is right_complementable Element of the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

bool the carrier of V is non empty set

W is Element of bool the carrier of V

x is Element of bool the carrier of V

y is set

v is right_complementable (K,V,W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is right_complementable Element of the carrier of V

x is right_complementable Element of the carrier of V

x - W is right_complementable Element of the carrier of V

- W is right_complementable Element of the carrier of V

x + (- W) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (x,(- W)) is right_complementable Element of the carrier of V

y is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

x + y is Element of bool the carrier of V

bool the carrier of V is non empty set

x - (x - W) is right_complementable Element of the carrier of V

- (x - W) is right_complementable Element of the carrier of V

x + (- (x - W)) is right_complementable Element of the carrier of V

the addF of V . (x,(- (x - W))) is right_complementable Element of the carrier of V

x - x is right_complementable Element of the carrier of V

- x is right_complementable Element of the carrier of V

x + (- x) is right_complementable Element of the carrier of V

the addF of V . (x,(- x)) is right_complementable Element of the carrier of V

(x - x) + W is right_complementable Element of the carrier of V

the addF of V . ((x - x),W) is right_complementable Element of the carrier of V

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

(0. V) + W is right_complementable Element of the carrier of V

the addF of V . ((0. V),W) is right_complementable Element of the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is right_complementable Element of the carrier of V

x is right_complementable Element of the carrier of V

W - x is right_complementable Element of the carrier of V

- x is right_complementable Element of the carrier of V

W + (- x) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (W,(- x)) is right_complementable Element of the carrier of V

y is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W + y is Element of bool the carrier of V

bool the carrier of V is non empty set

x + y is Element of bool the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

{ (b

x is set

y is set

v is right_complementable Element of the carrier of V

v + W is Element of bool the carrier of V

bool the carrier of V is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is set

the carrier of V is non empty set

x is right_complementable Element of the carrier of V

x + W is Element of bool the carrier of V

bool the carrier of V is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

x is right_complementable Element of the carrier of V

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

x + W is Element of bool the carrier of V

bool the carrier of V is non empty set

(K,V,W) is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty set

x is Element of (K,V,W)

y is right_complementable Element of the carrier of V

y + W is Element of bool the carrier of V

bool the carrier of V is non empty set

(K,V,W,y) is Element of (K,V,W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

v is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

w is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over v

the carrier of w is non empty set

y is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W is right_complementable Element of the carrier of V

(K,V,y,W) is Element of (K,V,y)

(K,V,y) is non empty set

W + y is Element of bool the carrier of V

bool the carrier of V is non empty set

x is right_complementable Element of the carrier of V

(K,V,y,x) is Element of (K,V,y)

x + y is Element of bool the carrier of V

W - x is right_complementable Element of the carrier of V

- x is right_complementable Element of the carrier of V

W + (- x) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (W,(- x)) is right_complementable Element of the carrier of V

c is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of w

a is right_complementable Element of the carrier of w

b is right_complementable Element of the carrier of w

a - b is right_complementable Element of the carrier of w

- b is right_complementable Element of the carrier of w

a + (- b) is right_complementable Element of the carrier of w

the addF of w is V6() V18([: the carrier of w, the carrier of w:], the carrier of w) Element of bool [:[: the carrier of w, the carrier of w:], the carrier of w:]

[: the carrier of w, the carrier of w:] is non empty set

[:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set

bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set

the addF of w . (a,(- b)) is right_complementable Element of the carrier of w

(v,w,c,a) is Element of (v,w,c)

(v,w,c) is non empty set

a + c is Element of bool the carrier of w

bool the carrier of w is non empty set

(v,w,c,b) is Element of (v,w,c)

b + c is Element of bool the carrier of w

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty set

the carrier of V is non empty set

x is Element of (K,V,W)

y is right_complementable Element of the carrier of V

(K,V,W,y) is Element of (K,V,W)

y + W is Element of bool the carrier of V

bool the carrier of V is non empty set

v is right_complementable Element of the carrier of V

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

y - v is right_complementable Element of the carrier of V

- v is right_complementable Element of the carrier of V

y + (- v) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (y,(- v)) is right_complementable Element of the carrier of V

- (y - v) is right_complementable Element of the carrier of V

- y is right_complementable Element of the carrier of V

(- y) - (- v) is right_complementable Element of the carrier of V

- (- v) is right_complementable Element of the carrier of V

(- y) + (- (- v)) is right_complementable Element of the carrier of V

the addF of V . ((- y),(- (- v))) is right_complementable Element of the carrier of V

(K,V,W,(- y)) is Element of (K,V,W)

(- y) + W is Element of bool the carrier of V

(K,V,W,(- v)) is Element of (K,V,W)

(- v) + W is Element of bool the carrier of V

v is right_complementable Element of the carrier of V

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

- v is right_complementable Element of the carrier of V

(K,V,W,(- v)) is Element of (K,V,W)

(- v) + W is Element of bool the carrier of V

y is Element of (K,V,W)

v is Element of (K,V,W)

w is right_complementable Element of the carrier of V

(K,V,W,w) is Element of (K,V,W)

w + W is Element of bool the carrier of V

bool the carrier of V is non empty set

- w is right_complementable Element of the carrier of V

(K,V,W,(- w)) is Element of (K,V,W)

(- w) + W is Element of bool the carrier of V

y is Element of (K,V,W)

v is right_complementable Element of the carrier of V

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

bool the carrier of V is non empty set

w is right_complementable Element of the carrier of V

(K,V,W,w) is Element of (K,V,W)

w + W is Element of bool the carrier of V

a is right_complementable Element of the carrier of V

(K,V,W,a) is Element of (K,V,W)

a + W is Element of bool the carrier of V

b is right_complementable Element of the carrier of V

(K,V,W,b) is Element of (K,V,W)

b + W is Element of bool the carrier of V

v - a is right_complementable Element of the carrier of V

- a is right_complementable Element of the carrier of V

v + (- a) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (v,(- a)) is right_complementable Element of the carrier of V

w - b is right_complementable Element of the carrier of V

- b is right_complementable Element of the carrier of V

w + (- b) is right_complementable Element of the carrier of V

the addF of V . (w,(- b)) is right_complementable Element of the carrier of V

(v - a) + (w - b) is right_complementable Element of the carrier of V

the addF of V . ((v - a),(w - b)) is right_complementable Element of the carrier of V

(v - a) + w is right_complementable Element of the carrier of V

the addF of V . ((v - a),w) is right_complementable Element of the carrier of V

((v - a) + w) - b is right_complementable Element of the carrier of V

((v - a) + w) + (- b) is right_complementable Element of the carrier of V

the addF of V . (((v - a) + w),(- b)) is right_complementable Element of the carrier of V

v + w is right_complementable Element of the carrier of V

the addF of V . (v,w) is right_complementable Element of the carrier of V

(v + w) - a is right_complementable Element of the carrier of V

(v + w) + (- a) is right_complementable Element of the carrier of V

the addF of V . ((v + w),(- a)) is right_complementable Element of the carrier of V

((v + w) - a) - b is right_complementable Element of the carrier of V

((v + w) - a) + (- b) is right_complementable Element of the carrier of V

the addF of V . (((v + w) - a),(- b)) is right_complementable Element of the carrier of V

a + b is right_complementable Element of the carrier of V

the addF of V . (a,b) is right_complementable Element of the carrier of V

(v + w) - (a + b) is right_complementable Element of the carrier of V

- (a + b) is right_complementable Element of the carrier of V

(v + w) + (- (a + b)) is right_complementable Element of the carrier of V

the addF of V . ((v + w),(- (a + b))) is right_complementable Element of the carrier of V

(K,V,W,(v + w)) is Element of (K,V,W)

(v + w) + W is Element of bool the carrier of V

(K,V,W,(a + b)) is Element of (K,V,W)

(a + b) + W is Element of bool the carrier of V

a is right_complementable Element of the carrier of V

(K,V,W,a) is Element of (K,V,W)

a + W is Element of bool the carrier of V

b is right_complementable Element of the carrier of V

(K,V,W,b) is Element of (K,V,W)

b + W is Element of bool the carrier of V

a + b is right_complementable Element of the carrier of V

the addF of V . (a,b) is right_complementable Element of the carrier of V

(K,V,W,(a + b)) is Element of (K,V,W)

(a + b) + W is Element of bool the carrier of V

v is Element of (K,V,W)

w is Element of (K,V,W)

a is right_complementable Element of the carrier of V

(K,V,W,a) is Element of (K,V,W)

a + W is Element of bool the carrier of V

bool the carrier of V is non empty set

b is right_complementable Element of the carrier of V

(K,V,W,b) is Element of (K,V,W)

b + W is Element of bool the carrier of V

a + b is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (a,b) is right_complementable Element of the carrier of V

(K,V,W,(a + b)) is Element of (K,V,W)

(a + b) + W is Element of bool the carrier of V

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty set

[:(K,V,W),(K,V,W):] is non empty set

bool [:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty set

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the carrier of V is non empty set

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is strict addLoopStr

(K,V,W) is non empty set

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the carrier of V is non empty set

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

x is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W is right_complementable Element of the carrier of V

(K,V,x,W) is Element of (K,V,x)

(K,V,x) is non empty set

W + x is Element of bool the carrier of V

bool the carrier of V is non empty set

(K,V,x) is non empty strict addLoopStr

(K,V,x) is V6() V18([:(K,V,x),(K,V,x):],(K,V,x)) Element of bool [:[:(K,V,x),(K,V,x):],(K,V,x):]

[:(K,V,x),(K,V,x):] is non empty set

[:[:(K,V,x),(K,V,x):],(K,V,x):] is non empty set

bool [:[:(K,V,x),(K,V,x):],(K,V,x):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,x,(0. V)) is Element of (K,V,x)

(0. V) + x is Element of bool the carrier of V

addLoopStr(# (K,V,x),(K,V,x),(K,V,x,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,x) is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

x is right_complementable Element of the carrier of V

(K,V,W,x) is Element of (K,V,W)

(K,V,W) is non empty set

x + W is Element of bool the carrier of V

bool the carrier of V is non empty set

(K,V,W) is non empty strict addLoopStr

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,W) is non empty set

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty strict addLoopStr

(K,V,W) is non empty set

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,W) is non empty set

x is Element of the carrier of (K,V,W)

y is right_complementable Element of the carrier of V

(K,V,W,y) is Element of (K,V,W)

y + W is Element of bool the carrier of V

(K,V,W,y) is Element of the carrier of (K,V,W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

v is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

w is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over v

the carrier of w is non empty set

y is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

W is right_complementable Element of the carrier of V

(K,V,y,W) is Element of the carrier of (K,V,y)

(K,V,y) is non empty strict addLoopStr

(K,V,y) is non empty set

(K,V,y) is V6() V18([:(K,V,y),(K,V,y):],(K,V,y)) Element of bool [:[:(K,V,y),(K,V,y):],(K,V,y):]

[:(K,V,y),(K,V,y):] is non empty set

[:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set

bool [:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,y,(0. V)) is Element of (K,V,y)

(0. V) + y is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,y),(K,V,y),(K,V,y,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,y) is non empty set

(K,V,y,W) is Element of (K,V,y)

W + y is Element of bool the carrier of V

x is right_complementable Element of the carrier of V

(K,V,y,x) is Element of the carrier of (K,V,y)

(K,V,y,x) is Element of (K,V,y)

x + y is Element of bool the carrier of V

W - x is right_complementable Element of the carrier of V

- x is right_complementable Element of the carrier of V

W + (- x) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (W,(- x)) is right_complementable Element of the carrier of V

c is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of w

a is right_complementable Element of the carrier of w

b is right_complementable Element of the carrier of w

a - b is right_complementable Element of the carrier of w

- b is right_complementable Element of the carrier of w

a + (- b) is right_complementable Element of the carrier of w

the addF of w is V6() V18([: the carrier of w, the carrier of w:], the carrier of w) Element of bool [:[: the carrier of w, the carrier of w:], the carrier of w:]

[: the carrier of w, the carrier of w:] is non empty set

[:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set

bool [:[: the carrier of w, the carrier of w:], the carrier of w:] is non empty set

the addF of w . (a,(- b)) is right_complementable Element of the carrier of w

(v,w,c,a) is Element of the carrier of (v,w,c)

(v,w,c) is non empty strict addLoopStr

(v,w,c) is non empty set

(v,w,c) is V6() V18([:(v,w,c),(v,w,c):],(v,w,c)) Element of bool [:[:(v,w,c),(v,w,c):],(v,w,c):]

[:(v,w,c),(v,w,c):] is non empty set

[:[:(v,w,c),(v,w,c):],(v,w,c):] is non empty set

bool [:[:(v,w,c),(v,w,c):],(v,w,c):] is non empty set

0. w is V55(w) right_complementable Element of the carrier of w

the ZeroF of w is right_complementable Element of the carrier of w

(v,w,c,(0. w)) is Element of (v,w,c)

(0. w) + c is Element of bool the carrier of w

bool the carrier of w is non empty set

addLoopStr(# (v,w,c),(v,w,c),(v,w,c,(0. w)) #) is non empty strict addLoopStr

the carrier of (v,w,c) is non empty set

(v,w,c,a) is Element of (v,w,c)

a + c is Element of bool the carrier of w

(v,w,c,b) is Element of the carrier of (v,w,c)

(v,w,c,b) is Element of (v,w,c)

b + c is Element of bool the carrier of w

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of V is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the ZeroF of V is right_complementable Element of the carrier of V

W is right_complementable Element of the carrier of V

x is right_complementable Element of the carrier of V

W + x is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (W,x) is right_complementable Element of the carrier of V

y is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,y) is non empty strict addLoopStr

(K,V,y) is non empty set

(K,V,y) is V6() V18([:(K,V,y),(K,V,y):],(K,V,y)) Element of bool [:[:(K,V,y),(K,V,y):],(K,V,y):]

[:(K,V,y),(K,V,y):] is non empty set

[:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set

bool [:[:(K,V,y),(K,V,y):],(K,V,y):] is non empty set

(K,V,y,(0. V)) is Element of (K,V,y)

(0. V) + y is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,y),(K,V,y),(K,V,y,(0. V)) #) is non empty strict addLoopStr

(K,V,y,W) is Element of the carrier of (K,V,y)

the carrier of (K,V,y) is non empty set

(K,V,y,W) is Element of (K,V,y)

W + y is Element of bool the carrier of V

(K,V,y,x) is Element of the carrier of (K,V,y)

(K,V,y,x) is Element of (K,V,y)

x + y is Element of bool the carrier of V

(K,V,y,W) + (K,V,y,x) is Element of the carrier of (K,V,y)

the addF of (K,V,y) is V6() V18([: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y)) Element of bool [:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):]

[: the carrier of (K,V,y), the carrier of (K,V,y):] is non empty set

[:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set

bool [:[: the carrier of (K,V,y), the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set

the addF of (K,V,y) . ((K,V,y,W),(K,V,y,x)) is Element of the carrier of (K,V,y)

(K,V,y,(W + x)) is Element of the carrier of (K,V,y)

(K,V,y,(W + x)) is Element of (K,V,y)

(W + x) + y is Element of bool the carrier of V

0. (K,V,y) is V55((K,V,y)) Element of the carrier of (K,V,y)

the ZeroF of (K,V,y) is Element of the carrier of (K,V,y)

(K,V,y,(0. V)) is Element of the carrier of (K,V,y)

(K,V,y,(K,V,y,W),(K,V,y,x)) is Element of (K,V,y)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty strict addLoopStr

(K,V,W) is non empty set

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the carrier of V is non empty set

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,W) is non empty set

y is Element of the carrier of (K,V,W)

w is right_complementable Element of the carrier of V

(K,V,W,w) is Element of the carrier of (K,V,W)

(K,V,W,w) is Element of (K,V,W)

w + W is Element of bool the carrier of V

v is Element of the carrier of (K,V,W)

a is right_complementable Element of the carrier of V

(K,V,W,a) is Element of the carrier of (K,V,W)

(K,V,W,a) is Element of (K,V,W)

a + W is Element of bool the carrier of V

y + v is Element of the carrier of (K,V,W)

the addF of (K,V,W) is V6() V18([: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):]

[: the carrier of (K,V,W), the carrier of (K,V,W):] is non empty set

[:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set

bool [:[: the carrier of (K,V,W), the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set

the addF of (K,V,W) . (y,v) is Element of the carrier of (K,V,W)

w + a is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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 addF of V . (w,a) is right_complementable Element of the carrier of V

(K,V,W,(w + a)) is Element of the carrier of (K,V,W)

(K,V,W,(w + a)) is Element of (K,V,W)

(w + a) + W is Element of bool the carrier of V

v + y is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (v,y) is Element of the carrier of (K,V,W)

y is Element of the carrier of (K,V,W)

a is right_complementable Element of the carrier of V

(K,V,W,a) is Element of the carrier of (K,V,W)

(K,V,W,a) is Element of (K,V,W)

a + W is Element of bool the carrier of V

v is Element of the carrier of (K,V,W)

b is right_complementable Element of the carrier of V

(K,V,W,b) is Element of the carrier of (K,V,W)

(K,V,W,b) is Element of (K,V,W)

b + W is Element of bool the carrier of V

w is Element of the carrier of (K,V,W)

c is right_complementable Element of the carrier of V

(K,V,W,c) is Element of the carrier of (K,V,W)

(K,V,W,c) is Element of (K,V,W)

c + W is Element of bool the carrier of V

y + v is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (y,v) is Element of the carrier of (K,V,W)

a + b is right_complementable Element of the carrier of V

the addF of V . (a,b) is right_complementable Element of the carrier of V

(K,V,W,(a + b)) is Element of the carrier of (K,V,W)

(K,V,W,(a + b)) is Element of (K,V,W)

(a + b) + W is Element of bool the carrier of V

v + w is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (v,w) is Element of the carrier of (K,V,W)

b + c is right_complementable Element of the carrier of V

the addF of V . (b,c) is right_complementable Element of the carrier of V

(K,V,W,(b + c)) is Element of the carrier of (K,V,W)

(K,V,W,(b + c)) is Element of (K,V,W)

(b + c) + W is Element of bool the carrier of V

(y + v) + w is Element of the carrier of (K,V,W)

the addF of (K,V,W) . ((y + v),w) is Element of the carrier of (K,V,W)

(a + b) + c is right_complementable Element of the carrier of V

the addF of V . ((a + b),c) is right_complementable Element of the carrier of V

(K,V,W,((a + b) + c)) is Element of the carrier of (K,V,W)

(K,V,W,((a + b) + c)) is Element of (K,V,W)

((a + b) + c) + W is Element of bool the carrier of V

a + (b + c) is right_complementable Element of the carrier of V

the addF of V . (a,(b + c)) is right_complementable Element of the carrier of V

(K,V,W,(a + (b + c))) is Element of the carrier of (K,V,W)

(K,V,W,(a + (b + c))) is Element of (K,V,W)

(a + (b + c)) + W is Element of bool the carrier of V

y + (v + w) is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (y,(v + w)) is Element of the carrier of (K,V,W)

y is Element of the carrier of (K,V,W)

v is right_complementable Element of the carrier of V

(K,V,W,v) is Element of the carrier of (K,V,W)

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

0. (K,V,W) is V55((K,V,W)) Element of the carrier of (K,V,W)

the ZeroF of (K,V,W) is Element of the carrier of (K,V,W)

(K,V,W,(0. V)) is Element of the carrier of (K,V,W)

y + (0. (K,V,W)) is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (y,(0. (K,V,W))) is Element of the carrier of (K,V,W)

v + (0. V) is right_complementable Element of the carrier of V

the addF of V . (v,(0. V)) is right_complementable Element of the carrier of V

(K,V,W,(v + (0. V))) is Element of the carrier of (K,V,W)

(K,V,W,(v + (0. V))) is Element of (K,V,W)

(v + (0. V)) + W is Element of bool the carrier of V

y is Element of the carrier of (K,V,W)

v is right_complementable Element of the carrier of V

(K,V,W,v) is Element of the carrier of (K,V,W)

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

w is right_complementable Element of the carrier of V

v + w is right_complementable Element of the carrier of V

the addF of V . (v,w) is right_complementable Element of the carrier of V

(K,V,W,w) is Element of the carrier of (K,V,W)

(K,V,W,w) is Element of (K,V,W)

w + W is Element of bool the carrier of V

a is Element of the carrier of (K,V,W)

y + a is Element of the carrier of (K,V,W)

the addF of (K,V,W) . (y,a) is Element of the carrier of (K,V,W)

K is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr

V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K

the carrier of K is non empty set

W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(K,V,W) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr

(K,V,W) is non empty set

(K,V,W) is V6() V18([:(K,V,W),(K,V,W):],(K,V,W)) Element of bool [:[:(K,V,W),(K,V,W):],(K,V,W):]

[:(K,V,W),(K,V,W):] is non empty set

[:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

bool [:[:(K,V,W),(K,V,W):],(K,V,W):] is non empty set

0. V is V55(V) right_complementable Element of the carrier of V

the carrier of V is non empty set

the ZeroF of V is right_complementable Element of the carrier of V

(K,V,W,(0. V)) is Element of (K,V,W)

(0. V) + W is Element of bool the carrier of V

bool the carrier of V is non empty set

addLoopStr(# (K,V,W),(K,V,W),(K,V,W,(0. V)) #) is non empty strict addLoopStr

the carrier of (K,V,W) is non empty set

y is right_complementable Element of the carrier of (K,V,W)

x is right_complementable Element of the carrier of K

v is right_complementable Element of the carrier of V

(K,V,W,v) is right_complementable Element of the carrier of (K,V,W)

(K,V,W,v) is Element of (K,V,W)

v + W is Element of bool the carrier of V

w is right_complementable Element of the carrier of V

(K,V,W,w) is right_complementable Element of the carrier of (K,V,W)

(K,V,W,w) is Element of (K,V,W)

w + W is Element of bool the carrier of V

w - v is right_complementable Element of the carrier of V

- v is right_complementable Element of the carrier of V

w + (- v) is right_complementable Element of the carrier of V

the addF of V is V6() V18([: the carrier of V, the carrier of V:], the carrier of V) 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