:: VECTSP_5 semantic presentation

K148() is Element of bool K144()

K144() is set

bool K144() is non empty set

K121() is set

bool K121() is non empty set

bool K148() is non empty set

{} is Relation-like non-empty empty-yielding empty set

the Relation-like non-empty empty-yielding empty set is Relation-like non-empty empty-yielding empty set

1 is non empty set

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

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

the carrier of V is non empty set

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

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

{ (b

bool the carrier of V is non empty set

the carrier of S is non empty set

the carrier of S0 is non empty set

I1 is set

Z is Element of the carrier of V

Z0 is Element of the carrier of V

Z + Z0 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

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

I1 is Element of bool the carrier of V

S1 is Element of bool the carrier of V

W9 is Element of bool the carrier of V

{ (b

Z is set

Z0 is Element of the carrier of V

A is Element of the carrier of V

Z0 + A is Element of the carrier of V

Z is set

Z0 is Element of the carrier of V

A is Element of the carrier of V

Z0 + A is Element of the carrier of V

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

the carrier of S1 is non empty set

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

the carrier of W9 is non empty set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of V is non empty set

{ (b

{ (b

I is set

I1 is Element of the carrier of V

Z is Element of the carrier of V

I1 + Z is Element of the carrier of V

the carrier of (F,V,S,S0) is non empty set

I is set

I1 is Element of the carrier of V

Z is Element of the carrier of V

I1 + Z is Element of the carrier of V

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

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

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

the carrier of S is non empty set

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

the carrier of S0 is non empty set

the carrier of S /\ the carrier of S0 is set

the carrier of V is non empty set

0. V is V47(V) Element of the carrier of V

the carrier of V /\ the carrier of V is set

bool the carrier of V is non empty set

I1 is Element of bool the carrier of V

Z is Element of bool the carrier of V

Z0 is Element of bool the carrier of V

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

the carrier of S1 is non empty set

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

the carrier of W9 is non empty set

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

the carrier of S1 is non empty set

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

the carrier of W9 is non empty set

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

the carrier of I is non empty set

the carrier of W9 /\ the carrier of I is set

the carrier of I /\ the carrier of W9 is set

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

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

the carrier of V is non empty set

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

S1 is set

the carrier of (F,V,S,S0) is non empty set

{ (b

W9 is Element of the carrier of V

I is Element of the carrier of V

W9 + I is Element of the carrier of V

W9 is Element of the carrier of V

I is Element of the carrier of V

W9 + I is Element of the carrier of V

{ (b

the carrier of (F,V,S,S0) is non empty set

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

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

the carrier of V is non empty set

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

S1 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

S1 + (0. V) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

(0. V) + S1 is Element of the carrier of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

S1 is set

the carrier of (F,V,S,S0) is non empty set

the carrier of S is non empty set

the carrier of S0 is non empty set

the carrier of S /\ the carrier of S0 is set

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

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

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

the carrier of S is non empty set

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

S1 is set

the carrier of V is non empty set

{ (b

I is Element of the carrier of S

I1 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

I1 + (0. V) is Element of the carrier of V

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

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

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

the carrier of S is non empty set

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

the carrier of S0 is non empty set

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

S1 is set

the carrier of V is non empty set

{ (b

W9 is Element of the carrier of V

I is Element of the carrier of V

W9 + I is Element of the carrier of V

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

(F,V,S,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of V is non empty set

{ (b

{ (b

{ (b

{ (b

the carrier of (F,V,S,(F,V,S0,S1)) is non empty set

Z0 is set

A is Element of the carrier of V

W is Element of the carrier of V

A + W is Element of the carrier of V

the carrier of (F,V,S,S0) is non empty set

L is Element of the carrier of V

W99 is Element of the carrier of V

L + W99 is Element of the carrier of V

W99 + W is Element of the carrier of V

the carrier of (F,V,S0,S1) is non empty set

L + (W99 + W) is Element of the carrier of V

Z0 is set

A is Element of the carrier of V

W is Element of the carrier of V

A + W is Element of the carrier of V

the carrier of (F,V,S0,S1) is non empty set

L is Element of the carrier of V

W99 is Element of the carrier of V

L + W99 is Element of the carrier of V

A + L is Element of the carrier of V

the carrier of (F,V,S,S0) is non empty set

(A + L) + W99 is Element of the carrier of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S is non empty set

the carrier of (F,V,S,S0) is non empty set

the carrier of S0 is non empty set

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,S) is non empty set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S is non empty set

the carrier of S0 is non empty set

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

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

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

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

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

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

the carrier of ((0). V) is non empty set

the carrier of S is non empty set

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

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

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

the carrier of S is non empty set

(F,V,S,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

the carrier of S0 is non empty set

S1 is set

the carrier of V is non empty set

{ (b

W9 is Element of the carrier of V

I is Element of the carrier of V

W9 + I is Element of the carrier of V

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

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

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

the carrier of S is non empty set

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

the carrier of S0 is non empty set

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

(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of V is non empty set

{ (b

{ (b

W9 is Element of the carrier of V

the carrier of (F,V,S1,S) is non empty set

Z is Element of the carrier of V

Z0 is Element of the carrier of V

Z + Z0 is Element of the carrier of V

the carrier of (F,V,S1,S0) is non empty set

the carrier of (F,V,S1,S0) is non empty set

Z is Element of the carrier of V

Z0 is Element of the carrier of V

Z + Z0 is Element of the carrier of V

the carrier of (F,V,S1,S) is non empty set

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

the carrier of S is non empty set

the carrier of ((Omega). V) is non empty set

0. S is V47(S) Element of the carrier of S

0. ((Omega). V) is V47( (Omega). V) Element of the carrier of ((Omega). V)

the addF of S is Relation-like [: the carrier of S, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of S, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of S, the carrier of S:], the carrier of S:]

[: the carrier of S, the carrier of S:] is Relation-like non empty set

[:[: the carrier of S, the carrier of S:], the carrier of S:] is Relation-like non empty set

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

the addF of ((Omega). V) is Relation-like [: the carrier of ((Omega). V), the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V)) Element of bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):]

[: the carrier of ((Omega). V), the carrier of ((Omega). V):] is Relation-like non empty set

[:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is Relation-like non empty set

bool [:[: the carrier of ((Omega). V), the carrier of ((Omega). V):], the carrier of ((Omega). V):] is non empty set

K114( the addF of ((Omega). V), the carrier of S) is set

the lmult of S is Relation-like [: the carrier of F, the carrier of S:] -defined the carrier of S -valued Function-like V18([: the carrier of F, the carrier of S:], the carrier of S) Element of bool [:[: the carrier of F, the carrier of S:], the carrier of S:]

[: the carrier of F, the carrier of S:] is Relation-like non empty set

[:[: the carrier of F, the carrier of S:], the carrier of S:] is Relation-like non empty set

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

the lmult of ((Omega). V) is Relation-like [: the carrier of F, the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued Function-like V18([: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V)) Element of bool [:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):]

[: the carrier of F, the carrier of ((Omega). V):] is Relation-like non empty set

[:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):] is Relation-like non empty set

bool [:[: the carrier of F, the carrier of ((Omega). V):], the carrier of ((Omega). V):] is non empty set

the lmult of ((Omega). V) | [: the carrier of F, the carrier of S:] is Relation-like [: the carrier of F, the carrier of S:] -defined [: the carrier of F, the carrier of ((Omega). V):] -defined the carrier of ((Omega). V) -valued set

0. V is V47(V) Element of the carrier of V

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

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

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

S0 is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over S

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

the carrier of S0 is non empty set

the addF of S0 is Relation-like [: the carrier of S0, the carrier of S0:] -defined the carrier of S0 -valued Function-like V18([: the carrier of S0, the carrier of S0:], the carrier of S0) Element of bool [:[: the carrier of S0, the carrier of S0:], the carrier of S0:]

[: the carrier of S0, the carrier of S0:] is Relation-like non empty set

[:[: the carrier of S0, the carrier of S0:], the carrier of S0:] is Relation-like non empty set

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

the ZeroF of S0 is Element of the carrier of S0

the lmult of S0 is Relation-like [: the carrier of S, the carrier of S0:] -defined the carrier of S0 -valued Function-like V18([: the carrier of S, the carrier of S0:], the carrier of S0) Element of bool [:[: the carrier of S, the carrier of S0:], the carrier of S0:]

the carrier of S is non empty set

[: the carrier of S, the carrier of S0:] is Relation-like non empty set

[:[: the carrier of S, the carrier of S0:], the carrier of S0:] is Relation-like non empty set

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

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

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

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

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

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

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

the carrier of ((Omega). V) is non empty set

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

the carrier of S0 is non empty set

the carrier of S is non empty set

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

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

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

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

(F,V,S,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S is non empty set

the carrier of S /\ the carrier of S is set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S is non empty set

the carrier of S0 is non empty set

the carrier of S1 is non empty set

the carrier of (F,V,S,(F,V,S0,S1)) is non empty set

the carrier of (F,V,S0,S1) is non empty set

the carrier of S /\ the carrier of (F,V,S0,S1) is set

the carrier of S0 /\ the carrier of S1 is set

the carrier of S /\ ( the carrier of S0 /\ the carrier of S1) is set

the carrier of S /\ the carrier of S0 is set

( the carrier of S /\ the carrier of S0) /\ the carrier of S1 is set

the carrier of (F,V,S,S0) is non empty set

the carrier of (F,V,S,S0) /\ the carrier of S1 is set

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

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

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

the carrier of S is non empty set

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

the carrier of S0 is non empty set

the carrier of S /\ the carrier of S0 is set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

the carrier of S is non empty set

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,S) is non empty set

the carrier of S0 is non empty set

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

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

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

the carrier of S is non empty set

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

the carrier of S0 is non empty set

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

(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S1,S) is non empty set

the carrier of S1 is non empty set

the carrier of S1 /\ the carrier of S0 is set

the carrier of (F,V,S1,S0) is non empty set

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

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

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

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

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S0 is non empty set

the carrier of S is non empty set

the carrier of (F,V,S0,S) is non empty set

the carrier of S0 /\ the carrier of S is set

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

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of S is non empty set

the carrier of S0 is non empty set

the carrier of S1 is non empty set

the carrier of (F,V,S,S1) is non empty set

the carrier of S /\ the carrier of S1 is set

the carrier of S0 /\ the carrier of S1 is set

the carrier of (F,V,S0,S1) is non empty set

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of V is non empty set

W9 is Element of the carrier of V

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

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

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

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

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

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

0. V is V47(V) Element of the carrier of V

the carrier of V is non empty set

the carrier of S is non empty set

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

bool the carrier of V is non empty set

{(0. V)} /\ the carrier of S is Element of bool the carrier of V

the carrier of (F,V,((0). V),S) is non empty set

the carrier of ((0). V) is non empty set

the carrier of ((0). V) /\ the carrier of S is set

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

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

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

the carrier of (F,V,((Omega). V),S) is non empty set

the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty set

the carrier of S is non empty set

the carrier of VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) /\ the carrier of S is set

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

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

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the ZeroF of V is Element of the carrier of V

the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]

the carrier of F is non empty set

[: the carrier of F, the carrier of V:] is Relation-like non empty set

[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

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

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

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,S0) is non empty set

the carrier of S is non empty set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,(F,V,S,S0),S0) is non empty set

the carrier of S0 is non empty set

S1 is set

the carrier of V is non empty set

{ (b

W9 is Element of the carrier of V

I is Element of the carrier of V

W9 + I is Element of the carrier of V

S1 is set

(F,V,S0,(F,V,S,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,(F,V,S,S0)) is non empty set

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

the carrier of S is non empty set

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,(F,V,S,S0)) is non empty set

S1 is set

the carrier of (F,V,S,S0) is non empty set

the carrier of S /\ the carrier of (F,V,S,S0) is set

S1 is set

the carrier of V is non empty set

W9 is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

W9 + (0. V) is Element of the carrier of V

{ (b

the carrier of (F,V,S,S0) is non empty set

the carrier of S /\ the carrier of (F,V,S,S0) is set

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

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

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

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

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S0,S)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,(F,V,S,S1)) is non empty set

W9 is set

the carrier of V is non empty set

{ (b

I is Element of the carrier of V

I1 is Element of the carrier of V

I + I1 is Element of the carrier of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,(F,V,S,S1)) is non empty set

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set

W9 is set

the carrier of S0 is non empty set

the carrier of (F,V,S,S1) is non empty set

the carrier of S0 /\ the carrier of (F,V,S,S1) is set

the carrier of V is non empty set

{ (b

I is Element of the carrier of V

I1 is Element of the carrier of V

I + I1 is Element of the carrier of V

I1 + I is Element of the carrier of V

(I1 + I) - I is Element of the carrier of V

- I is Element of the carrier of V

(I1 + I) + (- I) is Element of the carrier of V

I - I is Element of the carrier of V

I + (- I) is Element of the carrier of V

I1 + (I - I) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

I1 + (0. V) is Element of the carrier of V

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S,(F,V,S0,S1)) is non empty set

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S0,S),(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,(F,V,S0,S),(F,V,S,S1)) is non empty set

W9 is set

the carrier of V is non empty set

{ (b

I is Element of the carrier of V

I1 is Element of the carrier of V

I + I1 is Element of the carrier of V

{ (b

the carrier of (F,V,S,S1) is non empty set

{ (b

the carrier of (F,V,S0,S) is non empty set

the carrier of (F,V,S0,S) /\ the carrier of (F,V,S,S1) is set

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

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

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

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

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S0,S),(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,S0,(F,V,S,S1)) is non empty set

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set

the carrier of V is non empty set

bool the carrier of V is non empty set

the carrier of S0 is non empty set

W9 is Element of bool the carrier of V

the carrier of S is non empty set

I is set

the carrier of (F,V,S,S0) is non empty set

the carrier of (F,V,S0,S1) is non empty set

the carrier of (F,V,S,S0) /\ the carrier of (F,V,S0,S1) is set

{ (b

I1 is Element of the carrier of V

Z is Element of the carrier of V

I1 + Z is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

(I1 + Z) + (0. V) is Element of the carrier of V

{ (b

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S0,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

(F,V,S1,(F,V,S0,S)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S1,S0),S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S1,S),(F,V,S,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S1),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S1),(F,V,S1,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S1),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,(F,V,S,S1),S1),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S1,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S1,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,(F,V,S1,S1)),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S1),S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S1,S0)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,S,S0) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

(F,V,(F,V,S,S0),S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

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

(F,V,S0,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

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

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

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

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

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

(F,V,S,S1) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V

the carrier of V is non empty set

W9 is Element of the carrier of V

I is Element of the carrier of V

I1 is Element of the carrier of V

I + I1 is Element of the carrier of V

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

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

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

the carrier of S is non empty set

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

the carrier of S0 is non empty set

the carrier of S \/ the carrier of S0 is non empty set

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

the carrier of I is non empty set

Z is set

the carrier of V is non empty set

Z0 is Element of the carrier of S0

bool the carrier of V is non empty set

W is Element of bool the carrier of V

L is set

W99 is Element of the carrier of S

B is Element of bool the carrier of V

B9 is Element of the carrier of V

A is Element of the carrier of V

B9 + A is Element of the carrier of V

(B9 + A) - A is Element of the carrier of V

- A is Element of the carrier of V

(B9 + A) + (- A) is Element of the carrier of V

A - A is Element of the carrier of V

A + (- A) is Element of the carrier of V

B9 + (A - A) is Element of the carrier of V

0. V is V47(V) Element of the carrier of V

B9 + (0. V) is Element of the carrier of V

B is Element of bool the carrier of V

A + B9 is Element of the carrier of V

(A + B9) - B9 is Element of the carrier of V

- B9 is Element of the carrier of V

(A + B9) + (- B9) is Element of the carrier of V

B9 - B9 is Element of the carrier of V

B9 + (- B9) is Element of the carrier of V

A + (B9 - B9) is Element of the carrier of V

A + (0. V) is Element of the carrier of V

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

the carrier of I is non empty set

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

the carrier of I1 is non empty set

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

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

the carrier of V is non empty set

bool the carrier of V is non empty set

S is set

S1 is set

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

S0 is set

the carrier of I is non empty set

W9 is set

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

the carrier of I1 is non empty set

S0 is Relation-like Function-like set

S1 is set

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

the carrier of W9 is non empty set

I is set

[S1,I] is set

{S1,I} is non empty set

{S1} is non empty set

{{S1,I},{S1}} is non empty set

W9 is set

[S1,W9] is set

{S1,W9} is non empty set

{S1} is non empty set

{{S1,W9},{S1}} is non empty set

dom S0 is set

rng S0 is set

S1 is set

W9 is set

S0 . W9 is set

[W9,S1] is set

{W9,S1} is non empty set

{W9} is non empty set

{{W9,S1},{W9}} is non empty set

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

the carrier of I is non empty set

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

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

the carrier of I is non empty set

I1 is set

[I1,S1] is set

{I1,S1} is non empty set

{I1} is non empty set

{{I1,S1},{I1}} is non empty set

S0 . I1 is set

S is set

S0 is set

S1 is set

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

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

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

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

(F,V) is set

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

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

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

(F,V) is non empty set

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

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

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

the