:: 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₁() is set
K is Element of F₁()
V is Element of F₁()
W is set
F₁() is non empty set
[:F₁(),F₁():] is non empty set
bool [:F₁(),F₁():] is non empty set
K is V6() V18(F₁(),F₁()) Element of bool [:F₁(),F₁():]
V is V6() V18(F₁(),F₁()) Element of bool [:F₁(),F₁():]
W is Element of F₁()
K . W is Element of F₁()
F₂(W) is set
V . W is Element of F₁()
F₁() is non empty set
[:F₁(),F₁(),F₁():] is non empty set
[:[:F₁(),F₁(),F₁():],F₁():] is non empty set
bool [:[:F₁(),F₁(),F₁():],F₁():] is non empty set
K is V6() V18([:F₁(),F₁(),F₁():],F₁()) Element of bool [:[:F₁(),F₁(),F₁():],F₁():]
V is V6() V18([:F₁(),F₁(),F₁():],F₁()) Element of bool [:[:F₁(),F₁(),F₁():],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₂(W,x,y) is set
V . (W,x,y) is Element of F₁()
F₁() is non empty set
[:F₁(),F₁(),F₁(),F₁():] is non empty set
[:[:F₁(),F₁(),F₁(),F₁():],F₁():] is non empty set
bool [:[:F₁(),F₁(),F₁(),F₁():],F₁():] is non empty set
K is V6() V18([:F₁(),F₁(),F₁(),F₁():],F₁()) Element of bool [:[:F₁(),F₁(),F₁(),F₁():],F₁():]
V is V6() V18([:F₁(),F₁(),F₁(),F₁():],F₁()) Element of bool [:[:F₁(),F₁(),F₁(),F₁():],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₂(W,x,y,v) is set
V . (W,x,y,v) is Element of F₁()
F₂() is non empty set
bool F₂() is non empty set
F₁() is non empty set
{ F₃(b₁) where b₁ is Element of F₁() : P₁[b₁] } is set
K is Element of bool F₂()
F₁() is non empty set
F₂() is Element of F₁()
{ b₁ where b₁ is Element of F₁() : P₁[b₁] } is set
K is Element of F₁()
F₂() is non empty set
F₁() is set
{ b₁ where b₁ is Element of F₂() : P₁[b₁] } is set
F₃() is Element of F₂()
F₂() is non empty set
F₃() is Element of F₂()
F₁() is set
{ b₁ where b₁ is Element of F₂() : P₁[b₁] } is set
F₂() is set
F₃() is non empty set
{ b₁ where b₁ is Element of F₃() : P₁[b₁] } is set
F₁() is set
K is Element of F₃()
F₁() is non empty set
F₃() is set
F₅(F₃()) is set
{ b₁ where b₁ is Element of F₁() : P₂[b₁,F₃()] } is set
F₄() is Element of F₁()
F₂() is non empty set
{ b₁ where b₁ is Element of F₁() : S₁[b₁] } is set
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₁ where b₁ is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V)) : b₁ is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) } is set
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₁ where b₁ is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V,(K,V)) : b₁ is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (K,V) } is set
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₁ + b₂) where b₁, b₂ is right_complementable Element of the carrier of V : ( b₁ in W & b₂ in x ) } is set
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₁ + W) where b₁ is right_complementable Element of the carrier of V : verum } is set
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 addF of V . (w,(- v)) is right_complementable Element of the carrier of V
x * (w - v) is right_complementable Element of the carrier of V
x * w is right_complementable Element of the carrier of V
x * v is right_complementable Element of the carrier of V
(x * w) - (x * v) is right_complementable Element of the carrier of V
- (x * v) is right_complementable Element of the carrier of V
(x * w) + (- (x * v)) is right_complementable Element of the carrier of V
the addF of V . ((x * w),(- (x * v))) is right_complementable Element of the carrier of V
(K,V,W,(x * w)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * w)) is Element of (K,V,W)
(x * w) + W is Element of bool the carrier of V
(K,V,W,(x * v)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * v)) is Element of (K,V,W)
(x * 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
x * w is right_complementable Element of the carrier of V
(K,V,W,(x * w)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * w)) is Element of (K,V,W)
(x * w) + W is Element of bool the carrier of V
v is right_complementable Element of the carrier of (K,V,W)
w is right_complementable Element of the carrier of (K,V,W)
a is right_complementable Element of the carrier of V
(K,V,W,a) is right_complementable 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
x * a is right_complementable Element of the carrier of V
(K,V,W,(x * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * a)) is Element of (K,V,W)
(x * a) + 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
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
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
x is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
y is right_complementable Element of the carrier of K
v is right_complementable Element of the carrier of (K,V,W)
x . (y,v) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,y,v) is right_complementable Element of the carrier of (K,V,W)
x is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
y is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
v is right_complementable Element of the carrier of K
w is right_complementable Element of the carrier of (K,V,W)
x . (v,w) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,v,w) is right_complementable Element of the carrier of (K,V,W)
y . (v,w) is right_complementable 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
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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over 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
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 VectSpStr over K
(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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over 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
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 right_complementable Element of the carrier of (K,V,x)
(K,V,x) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
(K,V,x) is non empty set
(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
bool the carrier of V is non empty set
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,V,x,W) is Element of (K,V,x)
W + x is Element of bool the carrier of V
(K,V,x) is non empty strict VectSpStr over K
the addF of (K,V,x) is V6() V18([: the carrier of (K,V,x), the carrier of (K,V,x):], the carrier of (K,V,x)) Element of bool [:[: the carrier of (K,V,x), the carrier of (K,V,x):], the carrier of (K,V,x):]
[: the carrier of (K,V,x), the carrier of (K,V,x):] is non empty set
[:[: the carrier of (K,V,x), the carrier of (K,V,x):], the carrier of (K,V,x):] is non empty set
bool [:[: the carrier of (K,V,x), the carrier of (K,V,x):], the carrier of (K,V,x):] is non empty set
(K,V,x,(0. V)) is right_complementable Element of the carrier of (K,V,x)
(K,V,x) is V6() V18([: the carrier of K, the carrier of (K,V,x):], the carrier of (K,V,x)) Element of bool [:[: the carrier of K, the carrier of (K,V,x):], the carrier of (K,V,x):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,x):] is non empty set
[:[: the carrier of K, the carrier of (K,V,x):], the carrier of (K,V,x):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,x):], the carrier of (K,V,x):] is non empty set
VectSpStr(# the carrier of (K,V,x), the addF of (K,V,x),(K,V,x,(0. V)),(K,V,x) #) is non empty strict VectSpStr over K
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
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 VectSpStr over K
(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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K
the carrier of (K,V,W) is non empty set
x 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
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 right_complementable Element of the carrier of (K,V,W)
(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 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
(K,V,W,x) is Element of (K,V,W)
x + W is Element of bool the carrier of V
(K,V,W) is non empty strict VectSpStr over K
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K
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 VectSpStr over K
(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 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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K
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 right_complementable Element of the carrier of (K,V,W)
(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 VectSpStr over K
(K,V,y) is non empty strict right_complementable Abelian add-associative right_zeroed 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
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
(K,V,y,(0. V)) is right_complementable Element of the carrier of (K,V,y)
(K,V,y) is V6() V18([: the carrier of K, the carrier of (K,V,y):], the carrier of (K,V,y)) Element of bool [:[: the carrier of K, the carrier of (K,V,y):], the carrier of (K,V,y):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,y):] is non empty set
[:[: the carrier of K, the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,y):], the carrier of (K,V,y):] is non empty set
VectSpStr(# the carrier of (K,V,y), the addF of (K,V,y),(K,V,y,(0. V)),(K,V,y) #) is non empty strict VectSpStr over K
the carrier of (K,V,y) is non empty set
(K,V,y,W) is right_complementable Element of the carrier of (K,V,y)
(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 right_complementable 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 VectSpStr over v
(v,w,c) is non empty strict right_complementable Abelian add-associative right_zeroed 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
the addF of (v,w,c) is V6() V18([: the carrier of (v,w,c), the carrier of (v,w,c):], the carrier of (v,w,c)) Element of bool [:[: the carrier of (v,w,c), the carrier of (v,w,c):], the carrier of (v,w,c):]
[: the carrier of (v,w,c), the carrier of (v,w,c):] is non empty set
[:[: the carrier of (v,w,c), the carrier of (v,w,c):], the carrier of (v,w,c):] is non empty set
bool [:[: the carrier of (v,w,c), the carrier of (v,w,c):], the carrier of (v,w,c):] is non empty set
(v,w,c,(0. w)) is right_complementable Element of the carrier of (v,w,c)
(v,w,c) is V6() V18([: the carrier of v, the carrier of (v,w,c):], the carrier of (v,w,c)) Element of bool [:[: the carrier of v, the carrier of (v,w,c):], the carrier of (v,w,c):]
the carrier of v is non empty set
[: the carrier of v, the carrier of (v,w,c):] is non empty set
[:[: the carrier of v, the carrier of (v,w,c):], the carrier of (v,w,c):] is non empty set
bool [:[: the carrier of v, the carrier of (v,w,c):], the carrier of (v,w,c):] is non empty set
VectSpStr(# the carrier of (v,w,c), the addF of (v,w,c),(v,w,c,(0. w)),(v,w,c) #) is non empty strict VectSpStr over v
the carrier of (v,w,c) is non empty set
(v,w,c,a) is right_complementable Element of the carrier of (v,w,c)
(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 right_complementable 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
the carrier of K is non empty set
V is right_complementable Element of the carrier of K
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over K
the carrier of W is non empty set
x is right_complementable Element of the carrier of W
V * x is right_complementable Element of the carrier of W
y is right_complementable Element of the carrier of W
x + y 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 . (x,y) is right_complementable Element of the carrier of W
v is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of W
(K,W,v) is non empty strict VectSpStr over K
(K,W,v) is non empty strict right_complementable Abelian add-associative right_zeroed addLoopStr
(K,W,v) is non empty set
(K,W,v) is V6() V18([:(K,W,v),(K,W,v):],(K,W,v)) Element of bool [:[:(K,W,v),(K,W,v):],(K,W,v):]
[:(K,W,v),(K,W,v):] is non empty set
[:[:(K,W,v),(K,W,v):],(K,W,v):] is non empty set
bool [:[:(K,W,v),(K,W,v):],(K,W,v):] 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
(K,W,v,(0. W)) is Element of (K,W,v)
(0. W) + v is Element of bool the carrier of W
bool the carrier of W is non empty set
addLoopStr(# (K,W,v),(K,W,v),(K,W,v,(0. W)) #) is non empty strict addLoopStr
the carrier of (K,W,v) is non empty set
the addF of (K,W,v) is V6() V18([: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v)) Element of bool [:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):]
[: the carrier of (K,W,v), the carrier of (K,W,v):] is non empty set
[:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
bool [:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
(K,W,v,(0. W)) is right_complementable Element of the carrier of (K,W,v)
(K,W,v) is V6() V18([: the carrier of K, the carrier of (K,W,v):], the carrier of (K,W,v)) Element of bool [:[: the carrier of K, the carrier of (K,W,v):], the carrier of (K,W,v):]
[: the carrier of K, the carrier of (K,W,v):] is non empty set
[:[: the carrier of K, the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
bool [:[: the carrier of K, the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
VectSpStr(# the carrier of (K,W,v), the addF of (K,W,v),(K,W,v,(0. W)),(K,W,v) #) is non empty strict VectSpStr over K
(K,W,v,x) is Element of the carrier of (K,W,v)
the carrier of (K,W,v) is non empty set
(K,W,v,x) is right_complementable Element of the carrier of (K,W,v)
(K,W,v,x) is Element of (K,W,v)
x + v is Element of bool the carrier of W
(K,W,v,y) is Element of the carrier of (K,W,v)
(K,W,v,y) is right_complementable Element of the carrier of (K,W,v)
(K,W,v,y) is Element of (K,W,v)
y + v is Element of bool the carrier of W
(K,W,v,x) + (K,W,v,y) is Element of the carrier of (K,W,v)
the addF of (K,W,v) is V6() V18([: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v)) Element of bool [:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):]
[: the carrier of (K,W,v), the carrier of (K,W,v):] is non empty set
[:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
bool [:[: the carrier of (K,W,v), the carrier of (K,W,v):], the carrier of (K,W,v):] is non empty set
the addF of (K,W,v) . ((K,W,v,x),(K,W,v,y)) is Element of the carrier of (K,W,v)
(K,W,v,(x + y)) is Element of the carrier of (K,W,v)
(K,W,v,(x + y)) is right_complementable Element of the carrier of (K,W,v)
(K,W,v,(x + y)) is Element of (K,W,v)
(x + y) + v is Element of bool the carrier of W
V * (K,W,v,x) is Element of the carrier of (K,W,v)
(K,W,v,(V * x)) is Element of the carrier of (K,W,v)
(K,W,v,(V * x)) is right_complementable Element of the carrier of (K,W,v)
(K,W,v,(V * x)) is Element of (K,W,v)
(V * x) + v is Element of bool the carrier of W
(K,W,v,x) + (K,W,v,y) is right_complementable Element of the carrier of (K,W,v)
the addF of (K,W,v) . ((K,W,v,x),(K,W,v,y)) is right_complementable Element of the carrier of (K,W,v)
(K,W,v) . (V,(K,W,v,x)) is right_complementable Element of the carrier of (K,W,v)
(K,W,v,V,(K,W,v,x)) is right_complementable Element of the carrier of (K,W,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 strict VectSpStr over K
(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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K
the carrier of (K,V,W) is non empty set
x is right_complementable Element of the carrier of (K,V,W)
w is Element of the carrier of (K,V,W)
y is right_complementable Element of the carrier of (K,V,W)
a is Element of the carrier of (K,V,W)
v is right_complementable Element of the carrier of (K,V,W)
b is Element of the carrier of (K,V,W)
x + y is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (x,y) is right_complementable Element of the carrier of (K,V,W)
w + a 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) . (w,a) is Element of the carrier of (K,V,W)
x is Element of the carrier of (K,V,W)
y is Element of the carrier of (K,V,W)
x + y 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) . (x,y) is Element of the carrier of (K,V,W)
y + x is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,x) is Element of the carrier of (K,V,W)
v is right_complementable Element of the carrier of (K,V,W)
w is right_complementable Element of the carrier of (K,V,W)
v + w is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (v,w) is right_complementable Element of the carrier of (K,V,W)
x is Element of the carrier of (K,V,W)
y is Element of the carrier of (K,V,W)
v is Element of the carrier of (K,V,W)
x + y 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) . (x,y) is Element of the carrier of (K,V,W)
(x + y) + v is Element of the carrier of (K,V,W)
the addF of (K,V,W) . ((x + y),v) is Element of the carrier of (K,V,W)
w is right_complementable Element of the carrier of (K,V,W)
a is right_complementable Element of the carrier of (K,V,W)
w + a is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (w,a) is right_complementable Element of the carrier of (K,V,W)
b is right_complementable Element of the carrier of (K,V,W)
(w + a) + b is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . ((w + a),b) is right_complementable Element of the carrier of (K,V,W)
a + b is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (a,b) is right_complementable Element of the carrier of (K,V,W)
w + (a + b) is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (w,(a + b)) is right_complementable Element of the carrier of (K,V,W)
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)
x + (y + v) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (x,(y + v)) is Element of the carrier of (K,V,W)
x is Element of the carrier of (K,V,W)
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)
x + (0. (K,V,W)) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (x,(0. (K,V,W))) is Element of the carrier of (K,V,W)
y is right_complementable Element of the carrier of (K,V,W)
0. (K,V,W) is V55((K,V,W)) right_complementable Element of the carrier of (K,V,W)
the ZeroF of (K,V,W) is right_complementable Element of the carrier of (K,V,W)
y + (0. (K,V,W)) is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,(0. (K,V,W))) is right_complementable Element of the carrier of (K,V,W)
x is Element of the carrier of (K,V,W)
y is right_complementable Element of the carrier of (K,V,W)
v is right_complementable Element of the carrier of (K,V,W)
y + v is right_complementable Element of the carrier of (K,V,W)
the addF of (K,V,W) . (y,v) is right_complementable Element of the carrier of (K,V,W)
w is Element of the carrier of (K,V,W)
x + w is Element of the carrier of (K,V,W)
the addF of (K,V,W) . (x,w) 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
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 VectSpStr over K
(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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K
the carrier of (K,V,W) is non empty set
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 right_complementable 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
w 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 right_complementable 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
x is right_complementable Element of the carrier of K
x * a is right_complementable Element of the carrier of V
(K,V,W,(x * a)) is Element of the carrier of (K,V,W)
(K,V,W,(x * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * a)) is Element of (K,V,W)
(x * a) + W is Element of bool the carrier of V
x * v is Element of the carrier of (K,V,W)
x * b is right_complementable Element of the carrier of V
(K,V,W,(x * b)) is Element of the carrier of (K,V,W)
(K,V,W,(x * b)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * b)) is Element of (K,V,W)
(x * b) + W is Element of bool the carrier of V
x * w is Element of the carrier of (K,V,W)
y is right_complementable Element of the carrier of K
y * a is right_complementable Element of the carrier of V
(K,V,W,(y * a)) is Element of the carrier of (K,V,W)
(K,V,W,(y * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(y * a)) is Element of (K,V,W)
(y * a) + W is Element of bool the carrier of V
y * v is Element of the carrier of (K,V,W)
v + w 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) . (v,w) is Element of the carrier of (K,V,W)
x * (v + w) is Element of the carrier of (K,V,W)
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 the carrier of (K,V,W)
(K,V,W,(a + b)) is right_complementable 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
x * (K,V,W,(a + b)) is Element of the carrier of (K,V,W)
x * (a + b) is right_complementable Element of the carrier of V
(K,V,W,(x * (a + b))) is Element of the carrier of (K,V,W)
(K,V,W,(x * (a + b))) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * (a + b))) is Element of (K,V,W)
(x * (a + b)) + W is Element of bool the carrier of V
(x * a) + (x * b) is right_complementable Element of the carrier of V
the addF of V . ((x * a),(x * b)) is right_complementable Element of the carrier of V
(K,V,W,((x * a) + (x * b))) is Element of the carrier of (K,V,W)
(K,V,W,((x * a) + (x * b))) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,((x * a) + (x * b))) is Element of (K,V,W)
((x * a) + (x * b)) + W is Element of bool the carrier of V
(x * v) + (x * w) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . ((x * v),(x * w)) is Element of the carrier of (K,V,W)
x + y 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 . (x,y) is right_complementable Element of the carrier of K
(x + y) * v is Element of the carrier of (K,V,W)
(x + y) * a is right_complementable Element of the carrier of V
(K,V,W,((x + y) * a)) is Element of the carrier of (K,V,W)
(K,V,W,((x + y) * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,((x + y) * a)) is Element of (K,V,W)
((x + y) * a) + W is Element of bool the carrier of V
(x * a) + (y * a) is right_complementable Element of the carrier of V
the addF of V . ((x * a),(y * a)) is right_complementable Element of the carrier of V
(K,V,W,((x * a) + (y * a))) is Element of the carrier of (K,V,W)
(K,V,W,((x * a) + (y * a))) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,((x * a) + (y * a))) is Element of (K,V,W)
((x * a) + (y * a)) + W is Element of bool the carrier of V
(x * v) + (y * v) is Element of the carrier of (K,V,W)
the addF of (K,V,W) . ((x * v),(y * v)) is Element of the carrier of (K,V,W)
x * y is right_complementable Element of the carrier of K
the multF 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 multF of K . (x,y) is right_complementable Element of the carrier of K
(x * y) * v is Element of the carrier of (K,V,W)
(x * y) * a is right_complementable Element of the carrier of V
(K,V,W,((x * y) * a)) is Element of the carrier of (K,V,W)
(K,V,W,((x * y) * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,((x * y) * a)) is Element of (K,V,W)
((x * y) * a) + W is Element of bool the carrier of V
x * (y * a) is right_complementable Element of the carrier of V
(K,V,W,(x * (y * a))) is Element of the carrier of (K,V,W)
(K,V,W,(x * (y * a))) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,(x * (y * a))) is Element of (K,V,W)
(x * (y * a)) + W is Element of bool the carrier of V
x * (K,V,W,(y * a)) is Element of the carrier of (K,V,W)
x * (y * v) is Element of the carrier of (K,V,W)
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
(1_ K) * v is Element of the carrier of (K,V,W)
(1_ K) * a is right_complementable Element of the carrier of V
(K,V,W,((1_ K) * a)) is Element of the carrier of (K,V,W)
(K,V,W,((1_ K) * a)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W,((1_ K) * a)) is Element of (K,V,W)
((1_ K) * a) + 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 strict VectSpStr over K
(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
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
(K,V,W,(0. V)) is right_complementable Element of the carrier of (K,V,W)
(K,V,W) is V6() V18([: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W)) Element of bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):]
the carrier of K is non empty set
[: the carrier of K, the carrier of (K,V,W):] is non empty set
[:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
bool [:[: the carrier of K, the carrier of (K,V,W):], the carrier of (K,V,W):] is non empty set
VectSpStr(# the carrier of (K,V,W), the addF of (K,V,W),(K,V,W,(0. V)),(K,V,W) #) is non empty strict VectSpStr over K