K93() is V33() V34() V35() V39() set
K97() is V33() V34() V35() V36() V37() V38() V39() Element of bool K93()
bool K93() is non empty set
K92() is V33() V34() V35() V36() V37() V38() V39() set
bool K92() is non empty set
bool K97() is non empty set
{} is set
the Relation-like non-empty empty-yielding empty V33() V34() V35() V36() V37() V38() V39() set is Relation-like non-empty empty-yielding empty V33() V34() V35() V36() V37() V38() V39() set
1 is non empty V30() V31() V32() V33() V34() V35() V36() V37() V38() Element of K97()
0 is V30() V31() V32() V33() V34() V35() V36() V37() V38() Element of K97()
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
bool the carrier of V is non empty set
the carrier of W1 is non empty set
the carrier of W2 is non empty set
B is set
C is Element of the carrier of V
AC is Element of the carrier of V
C + AC is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
B is Element of bool the carrier of V
W3 is Element of bool the carrier of V
S is Element of bool the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W3 & b2 in S ) } is set
C is set
AC is Element of the carrier of V
BC is Element of the carrier of V
AC + BC is Element of the carrier of V
C is set
AC is Element of the carrier of V
BC is Element of the carrier of V
AC + BC is Element of the carrier of V
W3 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W3 is non empty set
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of S is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W2 is non empty set
the carrier of W1 /\ the carrier of W2 is set
the carrier of V is non empty set
0. V is V56(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
B is Element of bool the carrier of V
C is Element of bool the carrier of V
AC is Element of bool the carrier of V
W3 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W3 is non empty set
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of S is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is set
the carrier of (V,W1,W2) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
the carrier of (V,W1,W2) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
W3 + (0. V) is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
(0. V) + W3 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is set
the carrier of (V,W1,W2) is non empty set
the carrier of W1 is non empty set
the carrier of W2 is non empty set
the carrier of W1 /\ the carrier of W2 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() 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 W1 & b2 in W2 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W2 & b2 in W1 ) } is set
A is set
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
the carrier of (V,W1,W2) is non empty set
A is set
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
W3 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
A is Element of the carrier of W1
B is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
B + (0. V) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W2 is non empty set
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
W3 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() 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 W1 & b2 in W2 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W2 & b2 in W3 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,W1,W2) & b2 in W3 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in (V,W2,W3) ) } is set
the carrier of (V,W1,(V,W2,W3)) is non empty set
AC is set
BC is Element of the carrier of V
L is Element of the carrier of V
BC + L is Element of the carrier of V
the carrier of (V,W1,W2) is non empty set
B9 is Element of the carrier of V
B is Element of the carrier of V
B9 + B is Element of the carrier of V
B + L is Element of the carrier of V
the carrier of (V,W2,W3) is non empty set
B9 + (B + L) is Element of the carrier of V
AC is set
BC is Element of the carrier of V
L is Element of the carrier of V
BC + L is Element of the carrier of V
the carrier of (V,W2,W3) is non empty set
B9 is Element of the carrier of V
B is Element of the carrier of V
B9 + B is Element of the carrier of V
BC + B9 is Element of the carrier of V
the carrier of (V,W1,W2) is non empty set
(BC + B9) + B is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
the carrier of (V,W1,W2) is non empty set
the carrier of W2 is non empty set
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,W1) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
the carrier of W2 is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((0). V),W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,((0). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of ((0). V) is non empty set
the carrier of W1 is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,((0). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
the carrier of W1 is non empty set
the ZeroF of W1 is Element of the carrier of W1
the addF of W1 is Relation-like [: the carrier of W1, the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([: the carrier of W1, the carrier of W1:], the carrier of W1) Element of bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:]
[: the carrier of W1, the carrier of W1:] is Relation-like non empty set
[:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is Relation-like non empty set
bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is non empty set
the Mult of W1 is Relation-like [:K93(), the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([:K93(), the carrier of W1:], the carrier of W1) Element of bool [:[:K93(), the carrier of W1:], the carrier of W1:]
[:K93(), the carrier of W1:] is Relation-like set
[:[:K93(), the carrier of W1:], the carrier of W1:] is Relation-like set
bool [:[:K93(), the carrier of W1:], the carrier of W1:] is non empty set
RLSStruct(# the carrier of W1, the ZeroF of W1, the addF of W1, the Mult of W1 #) is non empty strict RLSStruct
(0). W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
(W1,((Omega). W1),((0). W1)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((Omega). V),W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,((Omega). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
the carrier of W1 /\ the carrier of W1 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
the carrier of W2 is non empty set
the carrier of W1 is non empty set
the carrier of W2 /\ the carrier of W1 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
the carrier of W2 is non empty set
the carrier of W3 is non empty set
the carrier of (V,W1,(V,W2,W3)) is non empty set
the carrier of (V,W2,W3) is non empty set
the carrier of W1 /\ the carrier of (V,W2,W3) is set
the carrier of W2 /\ the carrier of W3 is set
the carrier of W1 /\ ( the carrier of W2 /\ the carrier of W3) is set
the carrier of W1 /\ the carrier of W2 is set
( the carrier of W1 /\ the carrier of W2) /\ the carrier of W3 is set
the carrier of (V,W1,W2) is non empty set
the carrier of (V,W1,W2) /\ the carrier of W3 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
the carrier of W2 is non empty set
the carrier of W1 /\ the carrier of W2 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
the carrier of W1 is non empty set
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,W1) is non empty set
the carrier of W2 is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W2 is non empty set
the carrier of W1 is non empty set
the carrier of (V,W2,W1) is non empty set
the carrier of W2 /\ the carrier of W1 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((0). V),W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,((0). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
0. V is V56(V) Element of the carrier of V
the carrier of V is non empty set
the carrier of W1 is non empty set
{(0. V)} is Element of bool the carrier of V
bool the carrier of V is non empty set
{(0. V)} /\ the carrier of W1 is Element of bool the carrier of V
the carrier of (V,((0). V),W1) is non empty set
the carrier of ((0). V) is non empty set
the carrier of ((0). V) /\ the carrier of W1 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,((0). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
the carrier of W1 is non empty set
the ZeroF of W1 is Element of the carrier of W1
the addF of W1 is Relation-like [: the carrier of W1, the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([: the carrier of W1, the carrier of W1:], the carrier of W1) Element of bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:]
[: the carrier of W1, the carrier of W1:] is Relation-like non empty set
[:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is Relation-like non empty set
bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is non empty set
the Mult of W1 is Relation-like [:K93(), the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([:K93(), the carrier of W1:], the carrier of W1) Element of bool [:[:K93(), the carrier of W1:], the carrier of W1:]
[:K93(), the carrier of W1:] is Relation-like set
[:[:K93(), the carrier of W1:], the carrier of W1:] is Relation-like set
bool [:[:K93(), the carrier of W1:], the carrier of W1:] is non empty set
RLSStruct(# the carrier of W1, the ZeroF of W1, the addF of W1, the Mult of W1 #) is non empty strict RLSStruct
(0). W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
(W1,((Omega). W1),((0). W1)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of W1
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((Omega). V),W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,((Omega). V),W1) is non empty set
the carrier of W1 is non empty set
the carrier of V /\ the carrier of W1 is set
V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,((Omega). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
the carrier of W1 is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,(V,W1,W2),W2) is non empty set
the carrier of W2 is non empty set
W3 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,W1,W2) & b2 in W2 ) } is set
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
W3 is set
(V,W2,(V,W1,W2)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,(V,W1,W2)) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W1,W2)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,(V,W1,W2)) is non empty set
W3 is set
the carrier of (V,W1,W2) is non empty set
the carrier of W1 /\ the carrier of (V,W1,W2) is set
W3 is set
the carrier of V is non empty set
S is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
S + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
the carrier of (V,W1,W2) is non empty set
the carrier of W1 /\ the carrier of (V,W1,W2) is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W2,W1)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,(V,W1,W3)) is non empty set
S is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (V,W1,W2) & b2 in (V,W2,W3) ) } is set
A is Element of the carrier of V
B is Element of the carrier of V
A + B is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,(V,W1,W3)) is non empty set
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set
S is set
the carrier of W2 is non empty set
the carrier of (V,W1,W3) is non empty set
the carrier of W2 /\ the carrier of (V,W1,W3) is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W3 ) } is set
A is Element of the carrier of V
B is Element of the carrier of V
A + B is Element of the carrier of V
B + A is Element of the carrier of V
(B + A) - A is Element of the carrier of V
- A is Element of the carrier of V
(B + 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
B + (A - A) is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
B + (0. V) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,(V,W2,W3)) is non empty set
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W2,W1),(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,(V,W2,W1),(V,W1,W3)) is non empty set
S is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in (V,W2,W3) ) } is set
A is Element of the carrier of V
B is Element of the carrier of V
A + B is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W3 ) } is set
the carrier of (V,W1,W3) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W2 & b2 in W1 ) } is set
the carrier of (V,W2,W1) is non empty set
the carrier of (V,W2,W1) /\ the carrier of (V,W1,W3) is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W2,W1),(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W2,(V,W1,W3)) is non empty set
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,(V,W1,W2),(V,W2,W3)) is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
the carrier of W2 is non empty set
S is Element of bool the carrier of V
the carrier of W1 is non empty set
A is set
the carrier of (V,W1,W2) is non empty set
the carrier of (V,W2,W3) is non empty set
the carrier of (V,W1,W2) /\ the carrier of (V,W2,W3) is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W1 & b2 in W2 ) } is set
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
(B + C) + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in W2 & b2 in (V,W1,W3) ) } is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W3,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W3,W2)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W3),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,(V,W1,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W3),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W3,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W3),(V,W3,W2)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W3),W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,(V,W1,W3),W3),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W3,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W3,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,(V,W3,W3)),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W3),W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W3,W2)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,W1,W2),W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W2 is non empty set
the carrier of W1 \/ the carrier of W2 is set
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of A is non empty set
C is set
the carrier of V is non empty set
AC is Element of the carrier of W2
bool the carrier of V is non empty set
L is Element of bool the carrier of V
B9 is set
B is Element of the carrier of W1
x is Element of bool the carrier of V
v is Element of the carrier of V
BC is Element of the carrier of V
v + BC is Element of the carrier of V
(v + BC) - BC is Element of the carrier of V
- BC is Element of the carrier of V
(v + BC) + (- BC) is Element of the carrier of V
BC - BC is Element of the carrier of V
BC + (- BC) is Element of the carrier of V
v + (BC - BC) is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
v + (0. V) is Element of the carrier of V
x is Element of bool the carrier of V
BC + v is Element of the carrier of V
(BC + v) - v is Element of the carrier of V
- v is Element of the carrier of V
(BC + v) + (- v) is Element of the carrier of V
v - v is Element of the carrier of V
v + (- v) is Element of the carrier of V
BC + (v - v) is Element of the carrier of V
BC + (0. V) is Element of the carrier of V
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of A is non empty set
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of B is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty set
W1 is set
W3 is set
A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is set
the carrier of A is non empty set
S is set
B is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of B is non empty set
W2 is Relation-like Function-like set
W3 is set
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of S is non empty set
A is set
[W3,A] is set
{W3,A} is set
{W3} is set
{{W3,A},{W3}} is set
S is set
[W3,S] is set
{W3,S} is set
{W3} is set
{{W3,S},{W3}} is set
dom W2 is set
rng W2 is set
W3 is set
S is set
W2 . S is set
[S,W3] is set
{S,W3} is set
{S} is set
{{S,W3},{S}} is set
A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of A is non empty set
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of S is non empty set
A is set
[A,W3] is set
{A,W3} is set
{A} is set
{{A,W3},{A}} is set
W2 . A is set
W1 is set
W2 is set
W3 is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is set
the non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of V
W3 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Element of the carrier of V
W3 is Element of the carrier of V
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
W3 is Element of the carrier of V
W2 + W3 is Element of the carrier of V
W1 - W3 is Element of the carrier of V
- W3 is Element of the carrier of V
W1 + (- W3) is Element of the carrier of V
W3 - W3 is Element of the carrier of V
W3 + (- W3) is Element of the carrier of V
W2 + (W3 - W3) is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
W2 + (0. V) is Element of the carrier of V
(- W3) + W3 is Element of the carrier of V
W1 + ((- W3) + W3) is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
W1 + (0. V) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V) is non empty set
W2 is set
(V,W1,((0). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty set
[:W3,W3:] is Relation-like non empty set
bool [:W3,W3:] is non empty set
S is Relation-like W3 -defined W3 -valued Element of bool [:W3,W3:]
A is Element of W3
B is Element of W3
[A,B] is Element of [:W3,W3:]
{A,B} is set
{A} is set
{{A,B},{A}} is set
C is Element of W3
[B,C] is Element of [:W3,W3:]
{B,C} is set
{B} is set
{{B,C},{B}} is set
AC is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
BC is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
L is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B9 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
[A,C] is Element of [:W3,W3:]
{A,C} is set
{{A,C},{A}} is set
A is Element of W3
B is Element of W3
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
C is Element of W3
[B,C] is set
{B,C} is set
{B} is set
{{B,C},{B}} is set
[A,C] is set
{A,C} is set
{{A,C},{A}} is set
A is Element of W3
A is Element of W3
B is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
[A,A] is Element of [:W3,W3:]
{A,A} is set
{A} is set
{{A,A},{A}} is set
A is Element of W3
[A,A] is set
{A,A} is set
{A} is set
{{A,A},{A}} is set
A is set
the Element of W3 is Element of W3
AC is Element of W3
C is Element of W3
[AC,C] is Element of [:W3,W3:]
{AC,C} is set
{AC} is set
{{AC,C},{AC}} is set
B is set
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of C is non empty set
AC is set
B is Relation-like Function-like set
dom B is set
rng B is set
union (rng B) is set
AC is set
BC is set
L is set
B . L is set
B9 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of B9 is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
AC is Element of bool the carrier of V
BC is Element of the carrier of V
L is Element of the carrier of V
BC + L is Element of the carrier of V
B9 is set
B is set
B . B is set
v is set
x is set
B . x is set
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of C is non empty set
u is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of u is non empty set
y1 is Element of W3
y2 is Element of W3
[y1,y2] is Element of [:W3,W3:]
{y1,y2} is set
{y1} is set
{{y1,y2},{y1}} is set
c20 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
c21 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B . y2 is set
y2 is Element of W3
y1 is Element of W3
[y2,y1] is Element of [:W3,W3:]
{y2,y1} is set
{y2} is set
{{y2,y1},{y2}} is set
c20 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
c21 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B . y1 is set
y1 is Element of W3
y2 is Element of W3
[y1,y2] is Element of [:W3,W3:]
{y1,y2} is set
{y1} is set
{{y1,y2},{y1}} is set
[y2,y1] is Element of [:W3,W3:]
{y2,y1} is set
{y2} is set
{{y2,y1},{y2}} is set
BC is V31() V32() Element of K93()
L is Element of the carrier of V
BC * L is Element of the carrier of V
the Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (BC,L) is set
B9 is set
B is set
B . B is set
v is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of v is non empty set
the Element of rng B is Element of rng B
L is set
B . L is set
B9 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of B9 is non empty set
B9 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of B9 is non empty set
(V,W1,B9) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is Element of the carrier of V
v is set
x is set
B . x is set
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of C is non empty set
u is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,u) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of ((0). V) is non empty set
0. V is V56(V) Element of the carrier of V
{(0. V)} is Element of bool the carrier of V
B is Element of W3
x is Element of W3
B . x is set
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of C is non empty set
u is Element of the carrier of V
v is Element of W3
[x,v] is Element of [:W3,W3:]
{x,v} is set
{x} is set
{{x,v},{x}} is set
B is Element of W3
A is set
A is Element of W3
B is Element of W3
[A,B] is Element of [:W3,W3:]
{A,B} is set
{A} is set
{{A,B},{A}} is set
[B,A] is Element of [:W3,W3:]
{B,A} is set
{B} is set
{{B,A},{B}} is set
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
BC is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
L is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is Element of W3
B is Element of W3
[A,B] is set
{A,B} is set
{A} is set
{{A,B},{A}} is set
[B,A] is set
{B,A} is set
{B} is set
{{B,A},{B}} is set
A is Element of W3
B is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,B,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is Element of the carrier of V
0. V is V56(V) Element of the carrier of V
(0. V) + C is Element of the carrier of V
{ (b1 * C) where b1 is V31() V32() Element of K93() : verum } is set
1 * C is Element of the carrier of V
the Mult of V . (1,C) is set
BC is set
L is V31() V32() Element of K93()
L * C is Element of the carrier of V
the Mult of V . (L,C) is set
bool the carrier of V is non empty set
BC is Element of bool the carrier of V
L is Element of the carrier of V
B9 is Element of the carrier of V
L + B9 is Element of the carrier of V
B is V31() V32() Element of K93()
B * C is Element of the carrier of V
the Mult of V . (B,C) is set
v is V31() V32() Element of K93()
v * C is Element of the carrier of V
the Mult of V . (v,C) is set
B + v is V31() V32() Element of K93()
(B + v) * C is Element of the carrier of V
the Mult of V . ((B + v),C) is set
L is V31() V32() Element of K93()
B9 is Element of the carrier of V
L * B9 is Element of the carrier of V
the Mult of V . (L,B9) is set
B is V31() V32() Element of K93()
B * C is Element of the carrier of V
the Mult of V . (B,C) is set
L * B is V31() V32() Element of K93()
(L * B) * C is Element of the carrier of V
the Mult of V . ((L * B),C) is set
L is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of L is non empty set
(V,W1,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,L,(V,W1,B)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B9 is Element of the carrier of V
B is V31() V32() Element of K93()
B * C is Element of the carrier of V
the Mult of V . (B,C) is set
B " is V31() V32() Element of K93()
(B ") * (B * C) is Element of the carrier of V
the Mult of V . ((B "),(B * C)) is set
(B ") * B is V31() V32() Element of K93()
((B ") * B) * C is Element of the carrier of V
the Mult of V . (((B ") * B),C) is set
the carrier of ((0). V) is non empty set
{(0. V)} is Element of bool the carrier of V
(V,L,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,L,B),W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B9 is Element of the carrier of V
B is Element of the carrier of V
v is Element of the carrier of V
B + v is Element of the carrier of V
B9 - v is Element of the carrier of V
- v is Element of the carrier of V
B9 + (- v) is Element of the carrier of V
(V,W1,(V,L,B)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B9 is Element of W3
[A,B9] is Element of [:W3,W3:]
{A,B9} is set
{A} is set
{{A,B9},{A}} is set
(V,B,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W1) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,((0). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((0). V),((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Coset of W1
S is Coset of W2
W3 /\ S is Element of bool the carrier of V
bool the carrier of V is non empty set
the Element of W3 /\ S is Element of W3 /\ S
C is Element of the carrier of V
C + W2 is Element of bool the carrier of V
{ (C + b1) where b1 is Element of the carrier of V : b1 in W2 } is set
C + W1 is Element of bool the carrier of V
{ (C + b1) where b1 is Element of the carrier of V : b1 in W1 } is set
C + (V,W1,W2) is Element of bool the carrier of V
{ (C + b1) where b1 is Element of the carrier of V : b1 in (V,W1,W2) } is set
AC is set
BC is Element of the carrier of V
C + BC is Element of the carrier of V
L is Element of the carrier of V
C + L is Element of the carrier of V
AC is set
BC is Element of the carrier of V
C + BC is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of V
W2 + W1 is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W2 + b1) where b1 is Element of the carrier of V : b1 in W1 } is set
W3 is Coset of W1
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 is non empty set
the carrier of W2 is non empty set
0. V is V56(V) Element of the carrier of V
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is Coset of W1
B is Coset of W2
A /\ B is Element of bool the carrier of V
bool the carrier of V is non empty set
C is Element of the carrier of V
C + W1 is Element of bool the carrier of V
{ (C + b1) where b1 is Element of the carrier of V : b1 in W1 } is set
AC is Element of the carrier of V
BC is Element of the carrier of V
AC + BC is Element of the carrier of V
L is Element of the carrier of V
L + W2 is Element of bool the carrier of V
{ (L + b1) where b1 is Element of the carrier of V : b1 in W2 } is set
B9 is Element of the carrier of V
B is Element of the carrier of V
B9 + B is Element of the carrier of V
BC + B9 is Element of the carrier of V
v is Element of the carrier of V
{v} is Element of bool the carrier of V
x is set
L - B is Element of the carrier of V
- B is Element of the carrier of V
L + (- B) is Element of the carrier of V
B9 + W2 is Element of bool the carrier of V
{ (B9 + b1) where b1 is Element of the carrier of V : b1 in W2 } is set
C - AC is Element of the carrier of V
- AC is Element of the carrier of V
C + (- AC) is Element of the carrier of V
BC + W1 is Element of bool the carrier of V
{ (BC + b1) where b1 is Element of the carrier of V : b1 in W1 } is set
x is set
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is Coset of (V,W1,W2)
u is Element of the carrier of V
{u} is Element of bool the carrier of V
A is Element of the carrier of V
B is Coset of W1
B /\ the carrier of W2 is Element of bool the carrier of V
bool the carrier of V is non empty set
C is Element of the carrier of V
{C} is Element of bool the carrier of V
AC is Element of the carrier of V
A - AC is Element of the carrier of V
- AC is Element of the carrier of V
A + (- AC) is Element of the carrier of V
AC + C is Element of the carrier of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of W1 /\ the carrier of W2 is set
A is Element of the carrier of V
{A} is Element of bool the carrier of V
the carrier of ((0). V) is non empty set
{(0. V)} is Element of bool the carrier of V
the carrier of (V,W1,W2) is non empty set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W3 is Element of the carrier of V
the carrier of S is non empty set
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of S
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of S
(S,A,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of S
the ZeroF of S is Element of the carrier of S
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 Mult of S is Relation-like [:K93(), the carrier of S:] -defined the carrier of S -valued Function-like V18([:K93(), the carrier of S:], the carrier of S) Element of bool [:[:K93(), the carrier of S:], the carrier of S:]
[:K93(), the carrier of S:] is Relation-like set
[:[:K93(), the carrier of S:], the carrier of S:] is Relation-like set
bool [:[:K93(), the carrier of S:], the carrier of S:] is non empty set
RLSStruct(# the carrier of S, the ZeroF of S, the addF of S, the Mult of S #) is non empty strict RLSStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Element of the carrier of V
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
S + W2 is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (S + b1) where b1 is Element of the carrier of V : b1 in W2 } is set
the carrier of W1 is non empty set
AC is Coset of W2
BC is Coset of W1
BC /\ AC is Element of bool the carrier of V
L is Element of the carrier of V
{L} is Element of bool the carrier of V
A - C is Element of the carrier of V
- C is Element of the carrier of V
A + (- C) is Element of the carrier of V
(S + A) - C is Element of the carrier of V
(S + A) + (- C) is Element of the carrier of V
S + (A - C) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of ((0). V) is non empty set
0. V is V56(V) Element of the carrier of V
{(0. V)} is Element of bool the carrier of V
bool the carrier of V is non empty set
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of (V,W1,W2) is non empty set
W3 is Element of the carrier of V
S is set
B is Element of the carrier of V
C is Element of the carrier of V
B + C is Element of the carrier of V
(B + C) + (0. V) is Element of the carrier of V
A is Element of the carrier of V
A - A is Element of the carrier of V
- A is Element of the carrier of V
A + (- A) is Element of the carrier of V
(B + C) + (A - A) is Element of the carrier of V
(B + C) + A is Element of the carrier of V
((B + C) + A) - A is Element of the carrier of V
((B + C) + A) + (- A) is Element of the carrier of V
B + A is Element of the carrier of V
(B + A) + C is Element of the carrier of V
((B + A) + C) - A is Element of the carrier of V
((B + A) + C) + (- A) is Element of the carrier of V
C - A is Element of the carrier of V
C + (- A) is Element of the carrier of V
(B + A) + (C - A) is Element of the carrier of V
C - (0. V) is Element of the carrier of V
- (0. V) is Element of the carrier of V
C + (- (0. V)) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
[: the carrier of V, the carrier of V:] is Relation-like non empty set
W1 is Element of the carrier of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
S is Element of the carrier of V
A is Element of the carrier of V
S + A is Element of the carrier of V
[S,A] is Element of [: the carrier of V, the carrier of V:]
{S,A} is set
{S} is set
{{S,A},{S}} is set
[S,A] `1 is Element of the carrier of V
[S,A] `2 is Element of the carrier of V
([S,A] `1) + ([S,A] `2) is Element of the carrier of V
S is Element of [: the carrier of V, the carrier of V:]
S `1 is Element of the carrier of V
S `2 is Element of the carrier of V
(S `1) + (S `2) is Element of the carrier of V
A is Element of [: the carrier of V, the carrier of V:]
A `1 is Element of the carrier of V
A `2 is Element of the carrier of V
(A `1) + (A `2) is Element of the carrier of V
[(S `1),(S `2)] is Element of [: the carrier of V, the carrier of V:]
{(S `1),(S `2)} is set
{(S `1)} is set
{{(S `1),(S `2)},{(S `1)}} is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `1 is Element of the carrier of V
(V,W3,W2,W1) is Element of [: the carrier of V, the carrier of V:]
(V,W3,W2,W1) `2 is Element of the carrier of V
(V,W3,W1,W2) `2 is Element of the carrier of V
(V,W3,W2,W1) `1 is Element of the carrier of V
((V,W3,W2,W1) `2) + ((V,W3,W2,W1) `1) is Element of the carrier of V
((V,W3,W1,W2) `1) + ((V,W3,W1,W2) `2) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `2 is Element of the carrier of V
(V,W3,W2,W1) is Element of [: the carrier of V, the carrier of V:]
(V,W3,W2,W1) `1 is Element of the carrier of V
(V,W3,W2,W1) `2 is Element of the carrier of V
((V,W3,W2,W1) `2) + ((V,W3,W2,W1) `1) is Element of the carrier of V
(V,W3,W1,W2) `1 is Element of the carrier of V
((V,W3,W1,W2) `1) + ((V,W3,W1,W2) `2) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is Relation-like non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
S is Element of [: the carrier of V, the carrier of V:]
S `1 is Element of the carrier of V
S `2 is Element of the carrier of V
(S `1) + (S `2) is Element of the carrier of V
W3 is Element of the carrier of V
(V,W3,W1,W2) is Element of [: the carrier of V, the carrier of V:]
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `1 is Element of the carrier of V
(V,W3,W1,W2) `2 is Element of the carrier of V
((V,W3,W1,W2) `1) + ((V,W3,W1,W2) `2) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `1 is Element of the carrier of V
S is Element of the carrier of V
(V,S,W1,W2) is Element of [: the carrier of V, the carrier of V:]
(V,S,W1,W2) `2 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `1 is Element of the carrier of V
(V,W3,W2,W1) is Element of [: the carrier of V, the carrier of V:]
(V,W3,W2,W1) `2 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,W1)
W3 is Element of the carrier of V
(V,W3,W1,W2) 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
(V,W3,W1,W2) `2 is Element of the carrier of V
(V,W3,W2,W1) is Element of [: the carrier of V, the carrier of V:]
(V,W3,W2,W1) `1 is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
W1 is Element of (V)
W2 is Element of (V)
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W3,S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is Element of (V)
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,B,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W1 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W2 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W3 is set
S is set
A is Element of (V)
B is Element of (V)
W1 . (A,B) is Element of (V)
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,C,AC) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 . (W3,S) is set
W2 . (W3,S) is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
W1 is Element of (V)
W2 is Element of (V)
W3 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W3,S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is Element of (V)
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,B,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W1 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W2 is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
W3 is set
S is set
A is Element of (V)
B is Element of (V)
W1 . (A,B) is Element of (V)
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,C,AC) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W1 . (W3,S) is set
W2 . (W3,S) is set
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict LattStr
the carrier of LattStr(# (V),(V),(V) #) is non empty set
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_meet of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "/\" W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . (W3,W2) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,S,A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_meet of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
(W2 "/\" W3) "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
the L_join of LattStr(# (V),(V),(V) #) . ((W2 "/\" W3),W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,S,A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (B,W3) is set
(V,(V,S,A),A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
S is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "\/" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_join of LattStr(# (V),(V),(V) #) . (W3,S) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" (W3 "\/" S) is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W2,(W3 "\/" S)) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
(W2 "\/" W3) "\/" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . ((W2 "\/" W3),S) is Element of the carrier of LattStr(# (V),(V),(V) #)
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,B,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
BC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (W2,BC) is set
(V,A,(V,B,C)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,A,B),C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (AC,S) is set
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_join of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" (W2 "\/" W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
the L_meet of LattStr(# (V),(V),(V) #) . (W2,(W2 "\/" W3)) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,S,A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (W2,B) is set
(V,S,(V,S,A)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
S is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "/\" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_meet of LattStr(# (V),(V),(V) #) . (W3,S) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" (W3 "/\" S) is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . (W2,(W3 "/\" S)) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
(W2 "/\" W3) "/\" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . ((W2 "/\" W3),S) is Element of the carrier of LattStr(# (V),(V),(V) #)
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,B,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
BC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (W2,BC) is set
(V,A,(V,B,C)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,A,B),C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (AC,S) is set
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_join of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "\/" W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W3,W2) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
A is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,S,A) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict LattStr
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of LattStr(# (V),(V),(V) #) is non empty set
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "/\" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_meet of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "/\" W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . (W3,W2) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((0). V),S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of LattStr(# (V),(V),(V) #) is non empty set
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_join of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "\/" W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W3,W2) is Element of the carrier of LattStr(# (V),(V),(V) #)
S is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,((Omega). V),S) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of LattStr(# (V),(V),(V) #) is non empty set
W2 is Element of the carrier of LattStr(# (V),(V),(V) #)
S is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
W3 "/\" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_meet of LattStr(# (V),(V),(V) #) . (W3,S) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" (W3 "/\" S) is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
the L_join of LattStr(# (V),(V),(V) #) . (W2,(W3 "/\" S)) is Element of the carrier of LattStr(# (V),(V),(V) #)
W2 "\/" W3 is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W2,W3) is Element of the carrier of LattStr(# (V),(V),(V) #)
(W2 "\/" W3) "/\" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . ((W2 "\/" W3),S) is Element of the carrier of LattStr(# (V),(V),(V) #)
A is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,B) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,B,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,A,C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 "\/" S is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . (W2,S) is Element of the carrier of LattStr(# (V),(V),(V) #)
BC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (W2,BC) is set
(V,A,(V,B,C)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,(V,A,B),C) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
AC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (AC,S) is set
V is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of V is non empty set
Top V is Element of the carrier of V
Bottom V is Element of the carrier of V
W1 is Element of the carrier of V
W2 is Element of the carrier of V
W1 "\/" W2 is Element of the carrier of V
the L_join 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 L_join of V . (W1,W2) is Element of the carrier of V
W1 "/\" W2 is Element of the carrier of V
the L_meet 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 L_meet of V . (W1,W2) is Element of the carrier of V
W2 "\/" W1 is Element of the carrier of V
the L_join of V . (W2,W1) is Element of the carrier of V
W2 "/\" W1 is Element of the carrier of V
the L_meet of V . (W2,W1) is Element of the carrier of V
W2 "\/" W1 is Element of the carrier of V
the L_join of V . (W2,W1) is Element of the carrier of V
W2 "/\" W1 is Element of the carrier of V
the L_meet of V . (W2,W1) is Element of the carrier of V
V is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of V is non empty set
Bottom V is Element of the carrier of V
W1 is Element of the carrier of V
W2 is Element of the carrier of V
W2 "/\" W1 is Element of the carrier of V
the L_meet 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 L_meet of V . (W2,W1) is Element of the carrier of V
W3 is Element of the carrier of V
W1 "/\" W3 is Element of the carrier of V
the L_meet of V . (W1,W3) is Element of the carrier of V
(Bottom V) "/\" W1 is Element of the carrier of V
the L_meet 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 L_meet of V . ((Bottom V),W1) is Element of the carrier of V
V is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of V is non empty set
Top V is Element of the carrier of V
W1 is Element of the carrier of V
W2 is Element of the carrier of V
W1 "\/" W2 is Element of the carrier of V
the L_join 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 L_join of V . (W1,W2) is Element of the carrier of V
W3 is Element of the carrier of V
W3 "\/" W1 is Element of the carrier of V
the L_join of V . (W3,W1) is Element of the carrier of V
(Top V) "\/" W1 is Element of the carrier of V
the L_join 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 L_join of V . ((Top V),W1) is Element of the carrier of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
W1 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V77() LattStr
the carrier of W1 is non empty set
(0). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(Omega). V is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
W2 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded LattStr
the carrier of W2 is non empty set
S is Element of the carrier of W1
W3 is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded LattStr
the carrier of W3 is non empty set
A is Element of the carrier of W1
AC is Element of the carrier of W2
B is Element of the carrier of W2
AC "/\" B is Element of the carrier of W2
the L_meet of W2 is Relation-like [: the carrier of W2, the carrier of W2:] -defined the carrier of W2 -valued Function-like V18([: the carrier of W2, the carrier of W2:], the carrier of W2) Element of bool [:[: the carrier of W2, the carrier of W2:], the carrier of W2:]
[: the carrier of W2, the carrier of W2:] is Relation-like non empty set
[:[: the carrier of W2, the carrier of W2:], the carrier of W2:] is Relation-like non empty set
bool [:[: the carrier of W2, the carrier of W2:], the carrier of W2:] is non empty set
the L_meet of W2 . (AC,B) is Element of the carrier of W2
BC is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,BC,((0). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
Bottom W1 is Element of the carrier of W1
AC is Element of the carrier of W3
C is Element of the carrier of W3
AC "\/" C is Element of the carrier of W3
the L_join of W3 is Relation-like [: the carrier of W3, the carrier of W3:] -defined the carrier of W3 -valued Function-like V18([: the carrier of W3, the carrier of W3:], the carrier of W3) Element of bool [:[: the carrier of W3, the carrier of W3:], the carrier of W3:]
[: the carrier of W3, the carrier of W3:] is Relation-like non empty set
[:[: the carrier of W3, the carrier of W3:], the carrier of W3:] is Relation-like non empty set
bool [:[: the carrier of W3, the carrier of W3:], the carrier of W3:] is non empty set
the L_join of W3 . (AC,C) is Element of the carrier of W3
BC is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,BC,((Omega). V)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
Top W1 is Element of the carrier of W1
AC is Element of the carrier of W1
BC is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,BC) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,BC)
B9 is Element of the carrier of W1
B is Element of the carrier of W1
B "/\" AC is Element of the carrier of W1
the L_meet of W1 is Relation-like [: the carrier of W1, the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([: the carrier of W1, the carrier of W1:], the carrier of W1) Element of bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:]
[: the carrier of W1, the carrier of W1:] is Relation-like non empty set
[:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is Relation-like non empty set
bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:] is non empty set
the L_meet of W1 . (B,AC) is Element of the carrier of W1
(V, the non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,BC),BC) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
B "\/" AC is Element of the carrier of W1
the L_join of W1 is Relation-like [: the carrier of W1, the carrier of W1:] -defined the carrier of W1 -valued Function-like V18([: the carrier of W1, the carrier of W1:], the carrier of W1) Element of bool [:[: the carrier of W1, the carrier of W1:], the carrier of W1:]
the L_join of W1 . (B,AC) is Element of the carrier of W1
(V, the non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() (V,BC),BC) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W3 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W1,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V,W2,W3) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
(V) is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
[:(V),(V):] is Relation-like non empty set
[:[:(V),(V):],(V):] is Relation-like non empty set
bool [:[:(V),(V):],(V):] is non empty set
(V) is Relation-like [:(V),(V):] -defined (V) -valued Function-like V18([:(V),(V):],(V)) Element of bool [:[:(V),(V):],(V):]
LattStr(# (V),(V),(V) #) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular lower-bounded upper-bounded V77() complemented LattStr
the carrier of LattStr(# (V),(V),(V) #) is non empty set
A is Element of the carrier of LattStr(# (V),(V),(V) #)
B is Element of the carrier of LattStr(# (V),(V),(V) #)
A "\/" B is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
[:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is Relation-like non empty set
bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):] is non empty set
the L_join of LattStr(# (V),(V),(V) #) . (A,B) is Element of the carrier of LattStr(# (V),(V),(V) #)
(V,W1,W2) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
C is Element of the carrier of LattStr(# (V),(V),(V) #)
A "/\" C is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) is Relation-like [: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):] -defined the carrier of LattStr(# (V),(V),(V) #) -valued Function-like V18([: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #)) Element of bool [:[: the carrier of LattStr(# (V),(V),(V) #), the carrier of LattStr(# (V),(V),(V) #):], the carrier of LattStr(# (V),(V),(V) #):]
the L_meet of LattStr(# (V),(V),(V) #) . (A,C) is Element of the carrier of LattStr(# (V),(V),(V) #)
B "/\" C is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_meet of LattStr(# (V),(V),(V) #) . (B,C) is Element of the carrier of LattStr(# (V),(V),(V) #)
(A "/\" C) "\/" (B "/\" C) is Element of the carrier of LattStr(# (V),(V),(V) #)
the L_join of LattStr(# (V),(V),(V) #) . ((A "/\" C),(B "/\" C)) is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (A,C) is set
BC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (((V) . (A,C)),BC) is set
AC is Element of the carrier of LattStr(# (V),(V),(V) #)
(V) . (AC,BC) is set
(V,(V,W1,W3),(V,W2,W3)) is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
V is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of V is non empty set
S is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of S is non empty set
W1 is Element of the carrier of V
W2 is Element of the carrier of V
W3 is Element of the carrier of V
W2 + W3 is Element of the carrier of V
W1 - W3 is Element of the carrier of V
- W3 is Element of the carrier of V
W1 + (- W3) is Element of the carrier of V
B is Element of the carrier of S
A is Element of the carrier of S
C is Element of the carrier of S
A - C is Element of the carrier of S
- C is Element of the carrier of S
A + (- C) is Element of the carrier of S
B + C is Element of the carrier of S
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
the ZeroF of V is Element of the carrier 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 Mult of V is Relation-like [:K93(), the carrier of V:] -defined the carrier of V -valued Function-like V18([:K93(), the carrier of V:], the carrier of V) Element of bool [:[:K93(), the carrier of V:], the carrier of V:]
[:K93(), the carrier of V:] is Relation-like set
[:[:K93(), the carrier of V:], the carrier of V:] is Relation-like set
bool [:[:K93(), the carrier of V:], the carrier of V:] is non empty set
RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is non empty strict RLSStruct
V is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() RLSStruct
the carrier of V is non empty set
W1 is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V131() Subspace of V
W2 is Element of the carrier of V
V is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of V is non empty set
W1 is Element of the carrier of V
Bottom V is Element of the carrier of V
V is non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of V is non empty set
W1 is Element of the carrier of V
Top V is Element of the carrier of V