:: 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

1 is non empty set

the carrier of V is non empty set

{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
bool the carrier of V is non empty set
the carrier of S is non empty set
the carrier of S0 is non empty set
I1 is set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(0. V) + (0. V) is Element of the carrier of V
I1 is Element of bool the carrier of V
S1 is Element of bool the carrier of V
W9 is Element of bool the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in W9 ) } is set
Z is set
Z0 is Element of the carrier of V
A is Element of the carrier of V
Z0 + A is Element of the carrier of V
Z is set
Z0 is Element of the carrier of V
A is Element of the carrier of V
Z0 + A is Element of the carrier of V

the carrier of S1 is non empty set

the carrier of W9 is non empty set

the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S ) } is set
I is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
I is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V

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
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

the carrier of S1 is non empty set

the carrier of W9 is non empty set

the carrier of S1 is non empty set

the carrier of W9 is non empty set

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

the carrier of V is non empty set

S1 is set
the carrier of (F,V,S,S0) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
the carrier of (F,V,S,S0) is non empty set

the carrier of V is non empty set

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

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

the carrier of S is non empty set

the carrier of (F,V,S,S0) is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
I is Element of the carrier of S
I1 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
I1 + (0. V) is Element of the carrier of V

the carrier of S is non empty set

the carrier of S0 is non empty set

the carrier of (F,V,S,S0) is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V

the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S1 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in S1 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in (F,V,S0,S1) ) } is set
the carrier of (F,V,S,(F,V,S0,S1)) is non empty set
Z0 is set
A is Element of the carrier of V
W is Element of the carrier of V
A + W is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
L is Element of the carrier of V
W99 is Element of the carrier of V
L + W99 is Element of the carrier of V
W99 + W is Element of the carrier of V
the carrier of (F,V,S0,S1) is non empty set
L + (W99 + W) is Element of the carrier of V
Z0 is set
A is Element of the carrier of V
W is Element of the carrier of V
A + W is Element of the carrier of V
the carrier of (F,V,S0,S1) is non empty set
L is Element of the carrier of V
W99 is Element of the carrier of V
L + W99 is Element of the carrier of V
A + L is Element of the carrier of V
the carrier of (F,V,S,S0) is non empty set
(A + L) + W99 is Element of the carrier of V

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

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

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

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

the carrier of S is non empty set

the carrier of S0 is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V

the carrier of S is non empty set

the carrier of S0 is non empty set

the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in S0 ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S1 & b2 in S ) } is set
W9 is Element of the carrier of V
the carrier of (F,V,S1,S) is non empty set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
the carrier of (F,V,S1,S0) is non empty set
the carrier of (F,V,S1,S0) is non empty set
Z is Element of the carrier of V
Z0 is Element of the carrier of V
Z + Z0 is Element of the carrier of V
the carrier of (F,V,S1,S) is non empty set

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

the carrier of S is non empty set
the carrier of () is non empty set
0. S is V47(S) Element of the carrier of S
0. () is V47( (Omega). V) Element of the carrier of ()
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 () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is Relation-like non empty set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is non empty set
K114( the addF of (), 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 () is Relation-like [: the carrier of F, the carrier of ():] -defined the carrier of () -valued Function-like V18([: the carrier of F, the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of F, the carrier of ():], the carrier of ():]
[: the carrier of F, the carrier of ():] is Relation-like non empty set
[:[: the carrier of F, the carrier of ():], the carrier of ():] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of ():], the carrier of ():] is non empty set
the lmult of () | [: 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 ():] -defined the carrier of () -valued set
0. V is V47(V) Element of the carrier of V

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

the carrier of 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

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

the carrier of () is non empty set

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

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

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

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

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
the carrier of S /\ the carrier of S0 is set

the carrier of (F,V,S,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 is non empty set

the carrier of S is non empty set

the carrier of S0 is non empty set

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

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

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

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
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

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

the carrier of (F,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

the carrier of V is non empty set
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]
[: the carrier of V, the carrier of V:] is Relation-like non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the ZeroF of V is Element of the carrier of V
the lmult of V is Relation-like [: the carrier of F, the carrier of V:] -defined the carrier of V -valued Function-like V18([: the carrier of F, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of F, the carrier of V:], the carrier of V:]
the carrier of F is non empty set
[: the carrier of F, the carrier of V:] is Relation-like non empty set
[:[: the carrier of F, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of F, the carrier of V:], the carrier of V:] is non empty set
VectSpStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) is non empty strict VectSpStr over F

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

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

the carrier of (F,V,(F,V,S,S0),S0) is non empty set
the carrier of S0 is non empty set
S1 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in S0 ) } is set
W9 is Element of the carrier of V
I is Element of the carrier of V
W9 + I is Element of the carrier of V
S1 is set

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

the carrier of S is non empty set

the carrier of (F,V,S,(F,V,S,S0)) is non empty set
S1 is set
the carrier of (F,V,S,S0) is non empty set
the carrier of S /\ the carrier of (F,V,S,S0) is set
S1 is set
the carrier of V is non empty set
W9 is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
W9 + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
the carrier of (F,V,S,S0) is non empty set
the carrier of S /\ the carrier of (F,V,S,S0) is set

(F,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 (F,V,S0,(F,V,S,S1)) is non empty set
W9 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in (F,V,S,S0) & b2 in (F,V,S0,S1) ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V

(F,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,S0,(F,V,S,S1)) is non empty set

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set
W9 is set
the carrier of S0 is non empty set
the carrier of (F,V,S,S1) is non empty set
the carrier of S0 /\ the carrier of (F,V,S,S1) is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S1 ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
I1 + I is Element of the carrier of V
(I1 + I) - I is Element of the carrier of V
- I is Element of the carrier of V
(I1 + I) + (- I) is Element of the carrier of V
I - I is Element of the carrier of V
I + (- I) is Element of the carrier of V
I1 + (I - I) is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
I1 + (0. V) is Element of the carrier of V

(F,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,S,(F,V,S0,S1)) is non empty set

(F,V,(F,V,S0,S),(F,V,S,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of (F,V,(F,V,S0,S),(F,V,S,S1)) is non empty set
W9 is set
the carrier of V is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in (F,V,S0,S1) ) } is set
I is Element of the carrier of V
I1 is Element of the carrier of V
I + I1 is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S1 ) } is set
the carrier of (F,V,S,S1) is non empty set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in S ) } is set
the carrier of (F,V,S0,S) is non empty set
the carrier of (F,V,S0,S) /\ the carrier of (F,V,S,S1) is set

(F,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,S0,(F,V,S,S1)) is non empty set

(F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed Subspace of V
the carrier of (F,V,(F,V,S,S0),(F,V,S0,S1)) is non empty set
the carrier of V is non empty set
bool the carrier of V is non empty set
the carrier of S0 is non empty set
W9 is Element of bool the carrier of V
the carrier of S is non empty set
I is set
the carrier of (F,V,S,S0) is non empty set
the carrier of (F,V,S0,S1) is non empty set
the carrier of (F,V,S,S0) /\ the carrier of (F,V,S0,S1) is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S & b2 in S0 ) } is set
I1 is Element of the carrier of V
Z is Element of the carrier of V
I1 + Z is Element of the carrier of V
0. V is V47(V) Element of the carrier of V
(I1 + Z) + (0. V) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in S0 & b2 in (F,V,S,S1) ) } is set

(F,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,(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,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,(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,(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,(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

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

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 non empty set

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

the carrier of I is non empty set

the carrier of I1 is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
S is set
S1 is set

S0 is set
the carrier of I is non empty set
W9 is set

the carrier of I1 is non empty set

S1 is set

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

the carrier of I is non empty set

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

(F,V) is set

(F,V) is non empty set

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