K148() is Element of bool K144()
K144() is set
bool K144() is non empty set
K121() is set
bool K121() is non empty set
bool K148() is non empty set
{} is Relation-like non-empty empty-yielding empty set
the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set
1 is non empty set
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
bool the carrier of V is non empty set
the carrier of S is non empty set
the carrier of S0 is non empty set
I1 is set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
I1 is Element of bool the carrier of V
S1 is Element of bool the carrier of V
W9 is Element of bool the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in W9 ) } is set
Z is set
Z0 is Element of the carrier of V
A is Element of the carrier of V
Z0 + A is Element of the carrier of V
Z is set
Z0 is Element of the carrier of V
A is Element of the carrier of V
Z0 + A is Element of the carrier of V
S1 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 S1 is non empty set
W9 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 W9 is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) 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 V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S ) } is set
I is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
I is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S0 is non empty set
the carrier of S /\ the carrier of S0 is set
the carrier of V is non empty set
0. V is V47(V) Element of the carrier of V
the carrier of V /\ the carrier of V is set
bool the carrier of V is non empty set
I1 is Element of bool the carrier of V
Z is Element of bool the carrier of V
Z0 is Element of bool the carrier of V
S1 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 S1 is non empty set
W9 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 W9 is non empty set
S1 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 S1 is non empty set
W9 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of W9 is non empty set
I is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of I is non empty set
the carrier of W9 /\ the carrier of I is set
the carrier of I /\ the carrier of W9 is set
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is set
the carrier of (F,V,S,S0) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
the carrier of (F,V,S,S0) is non empty set
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
S1 + (0. V) is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(0. V) + S1 is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is set
the carrier of (F,V,S,S0) is non empty set
the carrier of S is non empty set
the carrier of S0 is non empty set
the carrier of S /\ the carrier of S0 is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
I is Element of the carrier of S
I1 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
I1 + (0. V) is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 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 S0 is non empty set
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),S1) 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 V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S1 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in S1 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in (F,V,S0,S1) ) } is set
the carrier of (F,V,S,(F,V,S0,S1)) is non empty set
Z0 is set
A is Element of the carrier of V
W is Element of the carrier of V
A + W is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
L is Element of the carrier of V
W99 is Element of the carrier of V
L + W99 is Element of the carrier of V
W99 + W is Element of the carrier of V
the carrier of (F,V,S0,S1) is non empty set
L + (W99 + W) is Element of the carrier of V
Z0 is set
A is Element of the carrier of V
W is Element of the carrier of V
A + W is Element of the carrier of V
the carrier of (F,V,S0,S1) is non empty set
L is Element of the carrier of V
W99 is Element of the carrier of V
L + W99 is Element of the carrier of V
A + L is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
(A + L) + W99 is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 S is non empty set
the carrier of (F,V,S,S0) is non empty set
the carrier of S0 is non empty set
(F,V,S0,S) 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 (F,V,S0,S) is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 S is non empty set
the carrier of S0 is non empty set
F 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((0). V),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,((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 carrier of ((0). V) is non empty set
the carrier of S is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
(F,V,S,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 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 S0 is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S0 is non empty set
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) 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 V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in S ) } is set
W9 is Element of the carrier of V
the carrier of (F,V,S1,S) is non empty set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
the carrier of (F,V,S1,S0) is non empty set
the carrier of (F,V,S1,S0) is non empty set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
the carrier of (F,V,S1,S) is non empty set
F 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 F
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
the carrier of ((Omega). V) is non empty set
0. S is V47(S) Element of the carrier of S
0. ((Omega). V) is V47( (Omega). V) Element of the carrier of ((Omega). V)
the addF of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]
[: the carrier of S, the carrier of S:] is Relation-like non empty set
[:[: the carrier of S, the carrier of S:], the carrier of S:] is Relation-like non empty set
bool [:[: the carrier of S, the carrier of S:], the carrier of S:] is non empty set
the addF of ((Omega). V) is Relation-like [: the carrier of ((Omega). V), the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V)) Element of bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):]
[: the carrier of ((Omega). V), the carrier of ((Omega). V):] is Relation-like non empty set
[:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is Relation-like non empty set
bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is non empty set
K114( the addF of ((Omega). V), the carrier of S) is set
the lmult of S is Relation-like [: the carrier of F, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of F, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of F, the carrier of S:], the carrier of S:]
[: the carrier of F, the carrier of S:] is Relation-like non empty set
[:[: the carrier of F, the carrier of S:], the carrier of S:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of S:], the carrier of S:] is non empty set
the lmult of ((Omega). V) is Relation-like [: the carrier of F, the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V)) Element of bool [:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):]
[: the carrier of F, the carrier of ((Omega). V):] is Relation-like non empty set
[:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):] is non empty set
the lmult of ((Omega). V) | [: the carrier of F, the carrier of S:] is Relation-like [: the carrier of F, the carrier of S:] -defined [: the carrier of F, the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued set
0. V is V47(V) Element of the carrier of V
F is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
S 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,((0). V),((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over S
(Omega). S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of S0
the carrier of S0 is non empty set
the addF of S0 is Relation-like [: the carrier of S0, the carrier of S0:] -defined the carrier of S0 -valued Function-like V18([: the carrier of S0, the carrier of S0:], the carrier of S0) Element of bool [:[: the carrier of S0, the carrier of S0:], the carrier of S0:]
[: the carrier of S0, the carrier of S0:] is Relation-like non empty set
[:[: the carrier of S0, the carrier of S0:], the carrier of S0:] is Relation-like non empty set
bool [:[: the carrier of S0, the carrier of S0:], the carrier of S0:] is non empty set
the ZeroF of S0 is Element of the carrier of S0
the lmult of S0 is Relation-like [: the carrier of S, the carrier of S0:] -defined the carrier of S0 -valued Function-like V18([: the carrier of S, the carrier of S0:], the carrier of S0) Element of bool [:[: the carrier of S, the carrier of S0:], the carrier of S0:]
the carrier of S is non empty set
[: the carrier of S, the carrier of S0:] is Relation-like non empty set
[:[: the carrier of S, the carrier of S0:], the carrier of S0:] is Relation-like non empty set
bool [:[: the carrier of S, the carrier of S0:], the carrier of S0:] is non empty set
VectSpStr(# the carrier of S0, the addF of S0, the ZeroF of S0, the lmult of S0 #) is non empty strict VectSpStr over S
(0). S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of S0
(S,S0,((Omega). S0),((0). S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of S0
F 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 F
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((Omega). V),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,((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 carrier of ((Omega). V) is non empty set
S0 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 S0 is non empty set
the carrier of S is non empty set
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over F
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,((Omega). V),((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S) 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 S is non empty set
the carrier of S /\ the carrier of S is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),S1) 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 S is non empty set
the carrier of S0 is non empty set
the carrier of S1 is non empty set
the carrier of (F,V,S,(F,V,S0,S1)) is non empty set
the carrier of (F,V,S0,S1) is non empty set
the carrier of S /\ the carrier of (F,V,S0,S1) is set
the carrier of S0 /\ the carrier of S1 is set
the carrier of S /\ ( the carrier of S0 /\ the carrier of S1) is set
the carrier of S /\ the carrier of S0 is set
( the carrier of S /\ the carrier of S0) /\ the carrier of S1 is set
the carrier of (F,V,S,S0) is non empty set
the carrier of (F,V,S,S0) /\ the carrier of S1 is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
the carrier of S0 is non empty set
the carrier of S /\ the carrier of S0 is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
the carrier of S is non empty set
(F,V,S0,S) 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 (F,V,S0,S) is non empty set
the carrier of S0 is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S0 is non empty set
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) 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 (F,V,S1,S) is non empty set
the carrier of S1 is non empty set
the carrier of S1 /\ the carrier of S0 is set
the carrier of (F,V,S1,S0) is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) 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 S0 is non empty set
the carrier of S is non empty set
the carrier of (F,V,S0,S) is non empty set
the carrier of S0 /\ the carrier of S is set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) 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 S is non empty set
the carrier of S0 is non empty set
the carrier of S1 is non empty set
the carrier of (F,V,S,S1) is non empty set
the carrier of S /\ the carrier of S1 is set
the carrier of S0 /\ the carrier of S1 is set
the carrier of (F,V,S0,S1) is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) 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 V is non empty set
W9 is Element of the carrier of V
F 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((0). V),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,((0). V)) 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 V47(V) Element of the carrier of V
the carrier of V is non empty set
the carrier of S is non empty set
{(0. V)} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
{(0. V)} /\ the carrier of S is Element of bool the carrier of V
the carrier of (F,V,((0). V),S) is non empty set
the carrier of ((0). V) is non empty set
the carrier of ((0). V) /\ the carrier of S is set
F 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 F
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
S is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((Omega). V),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,((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 carrier of (F,V,((Omega). V),S) is non empty set
the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty set
the carrier of S is non empty set
the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) /\ the carrier of S is set
F 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over F
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,((Omega). V),((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
the carrier of S is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),S0) 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 (F,V,(F,V,S,S0),S0) is non empty set
the carrier of S0 is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
S1 is set
(F,V,S0,(F,V,S,S0)) 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 (F,V,S0,(F,V,S,S0)) is non empty set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S,S0)) 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 (F,V,S,(F,V,S,S0)) is non empty set
S1 is set
the carrier of (F,V,S,S0) is non empty set
the carrier of S /\ the carrier of (F,V,S,S0) is set
S1 is set
the carrier of V is non empty set
W9 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
W9 + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
the carrier of (F,V,S,S0) is non empty set
the carrier of S /\ the carrier of (F,V,S,S0) is set
F 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 F
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S0,S)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) 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 (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) 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 (F,V,S0,(F,V,S,S1)) is non empty set
W9 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in (F,V,S0,S1) ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) 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 (F,V,S0,(F,V,S,S1)) is non empty set
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) 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 (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set
W9 is set
the carrier of S0 is non empty set
the carrier of (F,V,S,S1) is non empty set
the carrier of S0 /\ the carrier of (F,V,S,S1) is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S1 ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
I1 + I is Element of the carrier of V
(I1 + I) - I is Element of the carrier of V
- I is Element of the carrier of V
(I1 + I) + (- I) is Element of the carrier of V
I - I is Element of the carrier of V
I + (- I) is Element of the carrier of V
I1 + (I - I) is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
I1 + (0. V) is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S0,S1)) 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 (F,V,S,(F,V,S0,S1)) is non empty set
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S0,S),(F,V,S,S1)) 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 (F,V,(F,V,S0,S),(F,V,S,S1)) is non empty set
W9 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in (F,V,S0,S1) ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S1 ) } is set
the carrier of (F,V,S,S1) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S ) } is set
the carrier of (F,V,S0,S) is non empty set
the carrier of (F,V,S0,S) /\ the carrier of (F,V,S,S1) is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S0,S),(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) 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 (F,V,S0,(F,V,S,S1)) is non empty set
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) 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 (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
the carrier of S0 is non empty set
W9 is Element of bool the carrier of V
the carrier of S is non empty set
I is set
the carrier of (F,V,S,S0) is non empty set
the carrier of (F,V,S0,S1) is non empty set
the carrier of (F,V,S,S0) /\ the carrier of (F,V,S0,S1) is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(I1 + Z) + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in (F,V,S,S1) ) } is set
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,(F,V,S0,S)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S1,S0),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S1,S),(F,V,S,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S1),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S1),(F,V,S1,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S1),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,(F,V,S,S1),S1),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S1,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,(F,V,S1,S1)),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S1),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S1,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,S,S0),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S1) 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 V is non empty set
W9 is Element of the carrier of V
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S0 is non empty set
the carrier of S \/ the carrier of S0 is non empty set
I is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of I is non empty set
Z is set
the carrier of V is non empty set
Z0 is Element of the carrier of S0
bool the carrier of V is non empty set
W is Element of bool the carrier of V
L is set
W99 is Element of the carrier of S
B is Element of bool the carrier of V
B9 is Element of the carrier of V
A is Element of the carrier of V
B9 + A is Element of the carrier of V
(B9 + A) - A is Element of the carrier of V
- A is Element of the carrier of V
(B9 + A) + (- A) is Element of the carrier of V
A - A is Element of the carrier of V
A + (- A) is Element of the carrier of V
B9 + (A - A) is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
B9 + (0. V) is Element of the carrier of V
B is Element of bool the carrier of V
A + B9 is Element of the carrier of V
(A + B9) - B9 is Element of the carrier of V
- B9 is Element of the carrier of V
(A + B9) + (- B9) is Element of the carrier of V
B9 - B9 is Element of the carrier of V
B9 + (- B9) is Element of the carrier of V
A + (B9 - B9) is Element of the carrier of V
A + (0. V) is Element of the carrier of V
I is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of I is non empty set
I1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of I1 is non empty set
F 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 F
the carrier of V is non empty set
bool the carrier of V is non empty set
S is set
S1 is set
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is set
the carrier of I is non empty set
W9 is set
I1 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 I1 is non empty set
S0 is Relation-like Function-like set
S1 is set
W9 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 W9 is non empty set
I is set
[S1,I] is set
{S1,I} is non empty set
{S1} is non empty set
{{S1,I},{S1}} is non empty set
W9 is set
[S1,W9] is set
{S1,W9} is non empty set
{S1} is non empty set
{{S1,W9},{S1}} is non empty set
dom S0 is set
rng S0 is set
S1 is set
W9 is set
S0 . W9 is set
[W9,S1] is set
{W9,S1} is non empty set
{W9} is non empty set
{{W9,S1},{W9}} is non empty set
I 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 I is non empty set
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of I is non empty set
I1 is set
[I1,S1] is set
{I1,S1} is non empty set
{I1} is non empty set
{{I1,S1},{I1}} is non empty set
S0 . I1 is set
S is set
S0 is set
S1 is set
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
(F,V) is set
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
F 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over F
(F,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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
the carrier of ((Omega). V) is non empty set
S 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 S is non empty set
F 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 F
F 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 F
the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
(Omega). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(Omega). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
S is non empty right_complementable 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
(F,V) is non empty set
S0 is set
(F,V,S,((0). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty set
[:S1,S1:] is Relation-like non empty set
bool [:S1,S1:] is non empty set
W9 is Relation-like S1 -defined S1 -valued Element of bool [:S1,S1:]
I is Element of S1
I1 is Element of S1
[I,I1] is set
{I,I1} is non empty set
{I} is non empty set
{{I,I1},{I}} is non empty set
[I1,I] is set
{I1,I} is non empty set
{I1} is non empty set
{{I1,I},{I1}} is non empty set
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
A is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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
I is set
the Element of S1 is Element of S1
Z0 is Element of S1
Z is Element of S1
[Z0,Z] is Element of [:S1,S1:]
{Z0,Z} is non empty set
{Z0} is non empty set
{{Z0,Z},{Z0}} is non empty set
I1 is set
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,Z) 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 Z is non empty set
Z0 is set
I1 is Relation-like Function-like set
dom I1 is set
rng I1 is set
union (rng I1) is set
Z0 is set
A is set
W is set
I1 . W is set
L 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 L is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
Z0 is Element of bool the carrier of V
A is Element of the carrier of V
W is Element of the carrier of V
A + W is Element of the carrier of V
L is set
W99 is set
I1 . W99 is set
B9 is set
B is set
I1 . B is set
C 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 C is non empty set
u 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 u is non empty set
y1 is Element of S1
y2 is Element of S1
[y1,y2] is Element of [:S1,S1:]
{y1,y2} is non empty set
{y1} is non empty set
{{y1,y2},{y1}} is non empty set
c21 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
c22 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 . y2 is set
y2 is Element of S1
y1 is Element of S1
[y2,y1] is Element of [:S1,S1:]
{y2,y1} is non empty set
{y2} is non empty set
{{y2,y1},{y2}} is non empty set
c21 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
c22 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 . y1 is set
y1 is Element of S1
y2 is Element of S1
[y1,y2] is Element of [:S1,S1:]
{y1,y2} is non empty set
{y1} is non empty set
{{y1,y2},{y1}} is non empty set
[y2,y1] is Element of [:S1,S1:]
{y2,y1} is non empty set
{y2} is non empty set
{{y2,y1},{y2}} is non empty set
the carrier of F is non empty non trivial set
A is Element of the carrier of F
W is Element of the carrier of V
A * W is Element of the carrier of V
L is set
W99 is set
I1 . W99 is set
B9 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 B9 is non empty set
the Element of rng I1 is Element of rng I1
W is set
I1 . W is set
L 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 L is non empty set
L 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 L is non empty set
(F,V,S,L) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
W99 is Element of the carrier of V
B9 is set
B is set
I1 . B is set
C 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 C is non empty set
u is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,u) 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 ((0). V) is non empty set
0. V is V47(V) Element of the carrier of V
{(0. V)} is non empty Element of bool the carrier of V
W99 is Element of S1
B is Element of S1
I1 . B is set
C 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 C is non empty set
u is Element of the carrier of V
B9 is Element of S1
[B,B9] is Element of [:S1,S1:]
{B,B9} is non empty set
{B} is non empty set
{{B,B9},{B}} is non empty set
I1 is Element of S1
I is Element of S1
I1 is Element of S1
[I,I1] is set
{I,I1} is non empty set
{I} is non empty set
{{I,I1},{I}} is non empty set
Z is Element of S1
[I1,Z] is set
{I1,Z} is non empty set
{I1} is non empty set
{{I1,Z},{I1}} is non empty set
Z0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
A is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace 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
L is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
[I,Z] is set
{I,Z} is non empty set
{{I,Z},{I}} is non empty set
I is Element of S1
I1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
[I,I] is set
{I,I} is non empty set
{I} is non empty set
{{I,I},{I}} is non empty set
I is Element of S1
I1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,I1) 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 V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty non trivial set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,I1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(0. V) + Z is Element of the carrier of V
{ (b1 * Z) where b1 is Element of the carrier of F : verum } is set
1_ F is Element of the carrier of F
K133(F) is V47(F) Element of the carrier of F
(1_ F) * Z is Element of the carrier of V
A is set
W is Element of the carrier of F
W * Z is Element of the carrier of V
bool the carrier of V is non empty set
A is Element of bool the carrier of V
W is Element of the carrier of V
L is Element of the carrier of V
W + L is Element of the carrier of V
W99 is Element of the carrier of F
W99 * Z is Element of the carrier of V
B9 is Element of the carrier of F
B9 * Z is Element of the carrier of V
W99 + B9 is Element of the carrier of F
(W99 + B9) * Z is Element of the carrier of V
W is Element of the carrier of F
L is Element of the carrier of V
W * L is Element of the carrier of V
W99 is Element of the carrier of F
W99 * Z is Element of the carrier of V
W * W99 is Element of the carrier of F
(W * W99) * Z is 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
the carrier of W is non empty set
(F,V,S,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,W,(F,V,S,I1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
L is Element of the carrier of V
W99 is Element of the carrier of F
W99 * Z is Element of the carrier of V
W99 " is Element of the carrier of F
(W99 ") * (W99 * Z) is Element of the carrier of V
(W99 ") * W99 is Element of the carrier of F
((W99 ") * W99) * Z is Element of the carrier of V
0. F is V47(F) Element of the carrier of F
the carrier of ((0). V) is non empty set
{(0. V)} is non empty Element of bool the carrier of V
(F,V,W,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,W,I1),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
L is Element of the carrier of V
W99 is Element of the carrier of V
B9 is Element of the carrier of V
W99 + B9 is Element of the carrier of V
L - B9 is Element of the carrier of V
- B9 is Element of the carrier of V
L + (- B9) is Element of the carrier of V
(F,V,S,(F,V,W,I1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
L is Element of S1
[I,L] is Element of [:S1,S1:]
{I,L} is non empty set
{I} is non empty set
{{I,L},{I}} is non empty set
(F,V,I1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) 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
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty non trivial set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
(F,V,((0). V),((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((0). V),((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty non trivial set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Coset of S
W9 is Coset of S0
S1 /\ W9 is Element of bool the carrier of V
bool the carrier of V is non empty set
the Element of S1 /\ W9 is Element of S1 /\ W9
Z is Element of the carrier of V
Z + S0 is Element of bool the carrier of V
{ (Z + b1) where b1 is Element of the carrier of V : b1 in S0 } is set
Z + S is Element of bool the carrier of V
{ (Z + b1) where b1 is Element of the carrier of V : b1 in S } is set
Z + (F,V,S,S0) is Element of bool the carrier of V
{ (Z + b1) where b1 is Element of the carrier of V : b1 in (F,V,S,S0) } is set
Z0 is set
A is Element of the carrier of V
Z + A is Element of the carrier of V
W is Element of the carrier of V
Z + W is Element of the carrier of V
Z0 is set
A is Element of the carrier of V
Z + A is Element of the carrier of V
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of S is non empty set
the carrier of S0 is non empty set
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(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 addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
I is Coset of S
I1 is Coset of S0
I /\ I1 is Element of bool the carrier of V
bool the carrier of V is non empty set
Z is Element of the carrier of V
Z + S is Element of bool the carrier of V
{ (Z + b1) where b1 is Element of the carrier of V : b1 in S } is set
Z0 is Element of the carrier of V
A is Element of the carrier of V
Z0 + A is Element of the carrier of V
W is Element of the carrier of V
W + S0 is Element of bool the carrier of V
{ (W + b1) where b1 is Element of the carrier of V : b1 in S0 } is set
L is Element of the carrier of V
W99 is Element of the carrier of V
L + W99 is Element of the carrier of V
A + L is Element of the carrier of V
B9 is Element of the carrier of V
{B9} is non empty Element of bool the carrier of V
B is set
W - W99 is Element of the carrier of V
- W99 is Element of the carrier of V
W + (- W99) is Element of the carrier of V
L + S0 is Element of bool the carrier of V
{ (L + b1) where b1 is Element of the carrier of V : b1 in S0 } is set
Z - Z0 is Element of the carrier of V
- Z0 is Element of the carrier of V
Z + (- Z0) is Element of the carrier of V
A + S is Element of bool the carrier of V
{ (A + b1) where b1 is Element of the carrier of V : b1 in S } is set
B is set
(F,V,S,S0) 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
C is Coset of (F,V,S,S0)
u is Element of the carrier of V
{u} is non empty Element of bool the carrier of V
the carrier of (F,V,S,S0) is non empty set
I is set
I1 is Element of the carrier of V
Z is Coset of S
Z /\ the carrier of S0 is Element of bool the carrier of V
bool the carrier of V is non empty set
Z0 is Element of the carrier of V
{Z0} is non empty Element of bool the carrier of V
A is Element of the carrier of V
I1 - A is Element of the carrier of V
- A is Element of the carrier of V
I1 + (- A) is Element of the carrier of V
A + Z0 is Element of the carrier of V
the carrier of S /\ the carrier of S0 is set
I is Element of the carrier of V
{I} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
(F,V,S,S0) 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
0. V is V47(V) Element of the carrier of V
the carrier of ((0). V) is non empty set
{(0. V)} is non empty Element of bool the carrier of V
the carrier of (F,V,S,S0) is non empty set
F 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 strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over F
the carrier of V is non empty set
W9 is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over W9
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
the carrier of I is non empty set
I1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of I
Z is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of I
(W9,I,I1,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of I
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
W9 + S0 is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W9 + b1) where b1 is Element of the carrier of V : b1 in S0 } is set
the carrier of S is non empty set
Z0 is Coset of S0
A is Coset of S
A /\ Z0 is Element of bool the carrier of V
W is Element of the carrier of V
{W} is non empty Element of bool the carrier of V
I - Z is Element of the carrier of V
- Z is Element of the carrier of V
I + (- Z) is Element of the carrier of V
(W9 + I) - Z is Element of the carrier of V
(W9 + I) + (- Z) is Element of the carrier of V
W9 + (I - Z) is Element of the carrier of V
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S,S0) 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
the carrier of ((0). V) is non empty set
0. V is V47(V) Element of the carrier of V
{(0. V)} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
(F,V,S,S0) 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 (F,V,S,S0) is non empty set
S1 is Element of the carrier of V
W9 is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
(I1 + Z) + (0. V) is Element of the carrier of V
I is Element of the carrier of V
I - I is Element of the carrier of V
- I is Element of the carrier of V
I + (- I) is Element of the carrier of V
(I1 + Z) + (I - I) is Element of the carrier of V
(I1 + Z) + I is Element of the carrier of V
((I1 + Z) + I) - I is Element of the carrier of V
((I1 + Z) + I) + (- I) is Element of the carrier of V
I1 + I is Element of the carrier of V
(I1 + I) + Z is Element of the carrier of V
((I1 + I) + Z) - I is Element of the carrier of V
((I1 + I) + Z) + (- I) is Element of the carrier of V
Z - I is Element of the carrier of V
Z + (- I) is Element of the carrier of V
(I1 + I) + (Z - I) is Element of the carrier of V
Z + (- I) is Element of the carrier of V
Z + (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
F 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 F
the carrier of V is non empty set
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
[: the carrier of V, the carrier of V:] is Relation-like non empty set
S is Element of the carrier of V
(F,V,S0,S1) 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 Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
[W9,I] is Element of [: the carrier of V, the carrier of V:]
{W9,I} is non empty set
{W9} is non empty set
{{W9,I},{W9}} is non empty set
[W9,I] `1 is Element of the carrier of V
[W9,I] `2 is Element of the carrier of V
([W9,I] `1) + ([W9,I] `2) is Element of the carrier of V
W9 is Element of [: the carrier of V, the carrier of V:]
W9 `1 is Element of the carrier of V
W9 `2 is Element of the carrier of V
(W9 `1) + (W9 `2) is Element of the carrier of V
I is Element of [: the carrier of V, the carrier of V:]
I `1 is Element of the carrier of V
I `2 is Element of the carrier of V
(I `1) + (I `2) is Element of the carrier of V
[(W9 `1),(W9 `2)] is Element of [: the carrier of V, the carrier of V:]
{(W9 `1),(W9 `2)} is non empty set
{(W9 `1)} is non empty set
{{(W9 `1),(W9 `2)},{(W9 `1)}} is non empty set
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `1 is Element of the carrier of V
(F,V,S1,S0,S) is Element of [: the carrier of V, the carrier of V:]
(F,V,S1,S0,S) `2 is Element of the carrier of V
(F,V,S1,S,S0) `2 is Element of the carrier of V
(F,V,S1,S0,S) `1 is Element of the carrier of V
((F,V,S1,S0,S) `2) + ((F,V,S1,S0,S) `1) is Element of the carrier of V
((F,V,S1,S,S0) `1) + ((F,V,S1,S,S0) `2) is Element of the carrier of V
F 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `2 is Element of the carrier of V
(F,V,S1,S0,S) is Element of [: the carrier of V, the carrier of V:]
(F,V,S1,S0,S) `1 is Element of the carrier of V
(F,V,S1,S0,S) `2 is Element of the carrier of V
((F,V,S1,S0,S) `2) + ((F,V,S1,S0,S) `1) is Element of the carrier of V
(F,V,S1,S,S0) `1 is Element of the carrier of V
((F,V,S1,S,S0) `1) + ((F,V,S1,S,S0) `2) is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is Relation-like non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
W9 is Element of [: the carrier of V, the carrier of V:]
W9 `1 is Element of the carrier of V
W9 `2 is Element of the carrier of V
(W9 `1) + (W9 `2) is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `1 is Element of the carrier of V
(F,V,S1,S,S0) `2 is Element of the carrier of V
((F,V,S1,S,S0) `1) + ((F,V,S1,S,S0) `2) is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `1 is Element of the carrier of V
(F,V,S1,S,S0) `2 is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `1 is Element of the carrier of V
(F,V,S1,S0,S) is Element of [: the carrier of V, the carrier of V:]
(F,V,S1,S0,S) `2 is Element of the carrier of V
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
the carrier of V is non empty set
S is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,S)
S1 is Element of the carrier of V
(F,V,S1,S,S0) is Element of [: the carrier of V, the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
(F,V,S1,S,S0) `2 is Element of the carrier of V
(F,V,S1,S0,S) is Element of [: the carrier of V, the carrier of V:]
(F,V,S1,S0,S) `1 is Element of the carrier of V
F 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 F
(F,V) is non empty set
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
S is Element of (F,V)
S0 is Element of (F,V)
S1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,W9) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is Element of (F,V)
I1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I1,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
S0 is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
S1 is set
W9 is set
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is Element of (F,V)
I1 is Element of (F,V)
S . (I,I1) is Element of (F,V)
(F,V,Z,Z0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S . (S1,W9) is set
S0 . (S1,W9) is set
F 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 F
(F,V) is non empty set
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
S is Element of (F,V)
S0 is Element of (F,V)
S1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,S1,W9) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is Element of (F,V)
I1 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I1,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
S0 is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
S1 is set
W9 is set
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is Element of (F,V)
I1 is Element of (F,V)
S . (I,I1) is Element of (F,V)
(F,V,Z,Z0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S . (S1,W9) is set
S0 . (S1,W9) is set
F 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
the carrier of LattStr(# (F,V),(F,V),(F,V) #) is non empty set
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "/\" S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,S1) is set
(F,V,W9,I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S1,S0) is set
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(S0 "/\" S1) "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,W9,I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . ((S0 "/\" S1),S1) is set
(F,V) . (S0,S1) is set
(F,V) . (((F,V) . (S0,S1)),S1) is set
I1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (I1,S1) is set
(F,V,(F,V,W9,I),I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "/\" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" (S1 "/\" W9) is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(S0 "/\" S1) "/\" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I1,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,(S1 "/\" W9)) is set
(F,V) . (S1,W9) is set
(F,V) . (S0,((F,V) . (S1,W9))) is set
A is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (S0,A) is set
(F,V,I,(F,V,I1,Z)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,I,I1),Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (Z0,W9) is set
(F,V) . (S0,S1) is set
(F,V) . (((F,V) . (S0,S1)),W9) is set
(F,V) . ((S0 "/\" S1),W9) is set
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "\/" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" (S1 "\/" W9) is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(S0 "\/" S1) "\/" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I1,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,(S1 "\/" W9)) is set
(F,V) . (S1,W9) is set
(F,V) . (S0,((F,V) . (S1,W9))) is set
A is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (S0,A) is set
(F,V,I,(F,V,I1,Z)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,I,I1),Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (Z0,W9) is set
(F,V) . (S0,S1) is set
(F,V) . (((F,V) . (S0,S1)),W9) is set
(F,V) . ((S0 "\/" S1),W9) is set
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" (S0 "\/" S1) is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,W9,I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,(S0 "\/" S1)) is set
(F,V) . (S0,S1) is set
(F,V) . (S0,((F,V) . (S0,S1))) is set
I1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (S0,I1) is set
(F,V,W9,(F,V,W9,I)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "\/" S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,S1) is set
(F,V,W9,I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,W9) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S1,S0) is set
F 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
the carrier of LattStr(# (F,V),(F,V),(F,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
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "/\" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "/\" S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,S1) is set
(F,V,((0). V),W9) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S1,S0) is set
(F,V,W9,((0). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
F 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
the carrier of LattStr(# (F,V),(F,V),(F,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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
the carrier of ((Omega). V) is non empty set
S0 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 S0 is non empty set
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "\/" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S1,W9) is set
(F,V,S0,I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,((Omega). V),I) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (W9,S1) is set
(F,V,I,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
F 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
F 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
the carrier of LattStr(# (F,V),(F,V),(F,V) #) is non empty set
S0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S1 "/\" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" (S1 "/\" W9) is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
S0 "\/" S1 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(S0 "\/" S1) "/\" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
I is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,W9) is set
S0 "\/" W9 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
Z is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,I,Z) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,Z,I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V) . (S0,(S1 "/\" W9)) is set
(F,V) . (S1,W9) is set
(F,V) . (S0,((F,V) . (S1,W9))) is set
A is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (S0,A) is set
(F,V,I,(F,V,Z,I1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,(F,V,I,Z),I1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is Element of the carrier of LattStr(# (F,V),(F,V),(F,V) #)
(F,V) . (Z0,W9) is set
(F,V) . (S0,S1) is set
(F,V) . (((F,V) . (S0,S1)),W9) is set
(F,V) . ((S0 "\/" S1),W9) is set
F is non empty non degenerated non trivial right_complementable almost_left_invertible unital associative commutative 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 F
(F,V) is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
[:(F,V),(F,V):] is Relation-like non empty set
[:[:(F,V),(F,V):],(F,V):] is Relation-like non empty set
bool [:[:(F,V),(F,V):],(F,V):] is non empty set
(F,V) is Relation-like [:(F,V),(F,V):] -defined (F,V) -valued Function-like V18([:(F,V),(F,V):],(F,V)) Element of bool [:[:(F,V),(F,V):],(F,V):]
LattStr(# (F,V),(F,V),(F,V) #) is non empty strict LattStr
S is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V68() LattStr
(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 carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like 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 Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty non trivial set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, 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 F
the carrier of ((Omega). V) is non empty set
W9 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 W9 is non empty set
the carrier of S is non empty set
S1 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of S1 is non empty set
I is Element of the carrier of S
(0). V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
S0 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of S0 is non empty set
Z is Element of the carrier of S
A is Element of the carrier of S0
W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Z0 is Element of the carrier of S0
A "/\" Z0 is Element of the carrier of S0
(F,V) . (A,Z0) is set
(F,V,W,((0). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Bottom S is Element of the carrier of S
A is Element of the carrier of S1
W is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
I1 is Element of the carrier of S1
A "\/" I1 is Element of the carrier of S1
(F,V) . (A,I1) is set
(F,V,W,W9) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V,W,((Omega). V)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
Top S is Element of the carrier of S
A is Element of the carrier of S
W 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 vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,W) is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,W)
the carrier of the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,W) is non empty set
W99 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 W99 is non empty set
B9 is Element of the carrier of S
B is Element of the carrier of S
B "/\" A is Element of the carrier of S
(F,V) . (B,A) is set
(F,V,W99,W) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V, the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,W),W) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
B "\/" A is Element of the carrier of S
(F,V) . (B,A) is set
(F,V,W99,W) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
(F,V, the non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (F,V,W),W) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V