:: VECTSP_4 semantic presentation

K126() is Element of bool K122()
K122() is set
bool K122() is non empty set
K121() is set
bool K121() is non empty set
bool K126() is non empty set

1 is non empty set

the carrier of GF is non empty set

the carrier of V is non empty set
u is right_complementable Element of the carrier of GF
W is right_complementable Element of the carrier of GF
u - W is right_complementable Element of the carrier of GF
- W is right_complementable Element of the carrier of GF
u + (- W) is right_complementable Element of the carrier of GF
the addF of GF is Relation-like Function-like V18([: the carrier of GF, the carrier of GF:], the carrier of GF) Element of bool [:[: the carrier of GF, the carrier of GF:], the carrier of GF:]
[: the carrier of GF, the carrier of GF:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of GF:], the carrier of GF:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of GF:], the carrier of GF:] is non empty set
the addF of GF . (u,(- W)) is right_complementable Element of the carrier of GF
[u,(- W)] is set
{u,(- W)} is non empty set
{u} is non empty set
{{u,(- W)},{u}} is non empty set
the addF of GF . [u,(- W)] is set
B is right_complementable Element of the carrier of V
(u - W) * B is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((u - W),B) is right_complementable Element of the carrier of V
[(u - W),B] is set
{(u - W),B} is non empty set
{(u - W)} is non empty set
{{(u - W),B},{(u - W)}} is non empty set
the lmult of V . [(u - W),B] is set
u * B is right_complementable Element of the carrier of V
the lmult of V . (u,B) is right_complementable Element of the carrier of V
[u,B] is set
{u,B} is non empty set
{{u,B},{u}} is non empty set
the lmult of V . [u,B] is set
W * B is right_complementable Element of the carrier of V
the lmult of V . (W,B) is right_complementable Element of the carrier of V
[W,B] is set
{W,B} is non empty set
{W} is non empty set
{{W,B},{W}} is non empty set
the lmult of V . [W,B] is set
(u * B) - (W * B) is right_complementable Element of the carrier of V
- (W * B) is right_complementable Element of the carrier of V
(u * B) + (- (W * B)) is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . ((u * B),(- (W * B))) is right_complementable Element of the carrier of V
[(u * B),(- (W * B))] is set
{(u * B),(- (W * B))} is non empty set
{(u * B)} is non empty set
{{(u * B),(- (W * B))},{(u * B)}} is non empty set
the addF of V . [(u * B),(- (W * B))] is set
(- W) * B is right_complementable Element of the carrier of V
the lmult of V . ((- W),B) is right_complementable Element of the carrier of V
[(- W),B] is set
{(- W),B} is non empty set
{(- W)} is non empty set
{{(- W),B},{(- W)}} is non empty set
the lmult of V . [(- W),B] is set
(u * B) + ((- W) * B) is right_complementable Element of the carrier of V
the addF of V . ((u * B),((- W) * B)) is right_complementable Element of the carrier of V
[(u * B),((- W) * B)] is set
{(u * B),((- W) * B)} is non empty set
{{(u * B),((- W) * B)},{(u * B)}} is non empty set
the addF of V . [(u * B),((- W) * B)] is set
GF is non empty multMagma
V is non empty VectSpStr over GF
the carrier of V is non empty set
bool the carrier of V is non empty set

the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
u is Element of bool the carrier of V
the Element of u is Element of u
0. GF is V49(GF) right_complementable Element of the carrier of GF
the carrier of GF is non empty set
the ZeroF of GF is right_complementable Element of the carrier of GF
B is right_complementable Element of the carrier of V
(0. GF) * B is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((0. GF),B) is right_complementable Element of the carrier of V
[(0. GF),B] is set
{(0. GF),B} is non empty set
{(0. GF)} is non empty set
{{(0. GF),B},{(0. GF)}} is non empty set
the lmult of V . [(0. GF),B] is set

the carrier of V is non empty set
bool the carrier of V is non empty set
u is Element of bool the carrier of V
W is right_complementable Element of the carrier of V
- W is right_complementable Element of the carrier of V
1_ GF is right_complementable Element of the carrier of GF
the carrier of GF is non empty set
1. GF is right_complementable Element of the carrier of GF
the OneF of GF is right_complementable Element of the carrier of GF
- (1_ GF) is right_complementable Element of the carrier of GF
(- (1_ GF)) * W is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((- (1_ GF)),W) is right_complementable Element of the carrier of V
[(- (1_ GF)),W] is set
{(- (1_ GF)),W} is non empty set
{(- (1_ GF))} is non empty set
{{(- (1_ GF)),W},{(- (1_ GF))}} is non empty set
the lmult of V . [(- (1_ GF)),W] is set

the carrier of V is non empty set
bool the carrier of V is non empty set
u is Element of bool the carrier of V
W is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of V
W - B is right_complementable Element of the carrier of V
- B is right_complementable Element of the carrier of V
W + (- B) is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (W,(- B)) is right_complementable Element of the carrier of V
[W,(- B)] is set
{W,(- B)} is non empty set
{W} is non empty set
{{W,(- B)},{W}} is non empty set
the addF of V . [W,(- B)] is set

the carrier of V is non empty set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
{(0. V)} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
u + W is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the addF of V . [u,W] is set
the carrier of GF is non empty set
u is right_complementable Element of the carrier of GF
W is right_complementable Element of the carrier of V
u * W is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the lmult of V . [u,W] is set

the carrier of V is non empty set
bool the carrier of V is non empty set
u is Element of bool the carrier of V
W is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of V
W + B is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (W,B) is right_complementable Element of the carrier of V
[W,B] is set
{W,B} is non empty set
{W} is non empty set
{{W,B},{W}} is non empty set
the addF of V . [W,B] is set
the carrier of GF is non empty set
W is right_complementable Element of the carrier of GF
B is right_complementable Element of the carrier of V
W * B is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (W,B) is right_complementable Element of the carrier of V
[W,B] is set
{W,B} is non empty set
{W} is non empty set
{{W,B},{W}} is non empty set
the lmult of V . [W,B] is set

the carrier of V is non empty set
bool the carrier of V is non empty set
u is Element of bool the carrier of V
W is Element of bool the carrier of V
B is Element of bool the carrier of V
{ (b1 + b2) where b1, b2 is right_complementable Element of the carrier of V : ( b1 in u & b2 in W ) } is set
C is right_complementable Element of the carrier of V
C is right_complementable Element of the carrier of V
C + C is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (C,C) is right_complementable Element of the carrier of V
[C,C] is set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the addF of V . [C,C] is set
c8 is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c8 + x is right_complementable Element of the carrier of V
the addF of V . (c8,x) is right_complementable Element of the carrier of V
[c8,x] is set
{c8,x} is non empty set
{c8} is non empty set
{{c8,x},{c8}} is non empty set
the addF of V . [c8,x] is set
x is right_complementable Element of the carrier of V
z is right_complementable Element of the carrier of V
x + z is right_complementable Element of the carrier of V
the addF of V . (x,z) is right_complementable Element of the carrier of V
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the addF of V . [x,z] is set
(c8 + x) + x is right_complementable Element of the carrier of V
the addF of V . ((c8 + x),x) is right_complementable Element of the carrier of V
[(c8 + x),x] is set
{(c8 + x),x} is non empty set
{(c8 + x)} is non empty set
{{(c8 + x),x},{(c8 + x)}} is non empty set
the addF of V . [(c8 + x),x] is set
((c8 + x) + x) + z is right_complementable Element of the carrier of V
the addF of V . (((c8 + x) + x),z) is right_complementable Element of the carrier of V
[((c8 + x) + x),z] is set
{((c8 + x) + x),z} is non empty set
{((c8 + x) + x)} is non empty set
{{((c8 + x) + x),z},{((c8 + x) + x)}} is non empty set
the addF of V . [((c8 + x) + x),z] is set
c8 + x is right_complementable Element of the carrier of V
the addF of V . (c8,x) is right_complementable Element of the carrier of V
[c8,x] is set
{c8,x} is non empty set
{{c8,x},{c8}} is non empty set
the addF of V . [c8,x] is set
(c8 + x) + x is right_complementable Element of the carrier of V
the addF of V . ((c8 + x),x) is right_complementable Element of the carrier of V
[(c8 + x),x] is set
{(c8 + x),x} is non empty set
{(c8 + x)} is non empty set
{{(c8 + x),x},{(c8 + x)}} is non empty set
the addF of V . [(c8 + x),x] is set
((c8 + x) + x) + z is right_complementable Element of the carrier of V
the addF of V . (((c8 + x) + x),z) is right_complementable Element of the carrier of V
[((c8 + x) + x),z] is set
{((c8 + x) + x),z} is non empty set
{((c8 + x) + x)} is non empty set
{{((c8 + x) + x),z},{((c8 + x) + x)}} is non empty set
the addF of V . [((c8 + x) + x),z] is set
x + z is right_complementable Element of the carrier of V
the addF of V . (x,z) is right_complementable Element of the carrier of V
[x,z] is set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the addF of V . [x,z] is set
(c8 + x) + (x + z) is right_complementable Element of the carrier of V
the addF of V . ((c8 + x),(x + z)) is right_complementable Element of the carrier of V
[(c8 + x),(x + z)] is set
{(c8 + x),(x + z)} is non empty set
{{(c8 + x),(x + z)},{(c8 + x)}} is non empty set
the addF of V . [(c8 + x),(x + z)] is set
the carrier of GF is non empty set
C is right_complementable Element of the carrier of GF
C is right_complementable Element of the carrier of V
C * C is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (C,C) is right_complementable Element of the carrier of V
[C,C] is set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the lmult of V . [C,C] is set
c8 is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c8 + x is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (c8,x) is right_complementable Element of the carrier of V
[c8,x] is set
{c8,x} is non empty set
{c8} is non empty set
{{c8,x},{c8}} is non empty set
the addF of V . [c8,x] is set
C * c8 is right_complementable Element of the carrier of V
the lmult of V . (C,c8) is right_complementable Element of the carrier of V
[C,c8] is set
{C,c8} is non empty set
{{C,c8},{C}} is non empty set
the lmult of V . [C,c8] is set
C * x is right_complementable Element of the carrier of V
the lmult of V . (C,x) is right_complementable Element of the carrier of V
[C,x] is set
{C,x} is non empty set
{{C,x},{C}} is non empty set
the lmult of V . [C,x] is set
(C * c8) + (C * x) is right_complementable Element of the carrier of V
the addF of V . ((C * c8),(C * x)) is right_complementable Element of the carrier of V
[(C * c8),(C * x)] is set
{(C * c8),(C * x)} is non empty set
{(C * c8)} is non empty set
{{(C * c8),(C * x)},{(C * c8)}} is non empty set
the addF of V . [(C * c8),(C * x)] is set

the carrier of V is non empty set
bool the carrier of V is non empty set
u is Element of bool the carrier of V
W is Element of bool the carrier of V
u /\ W is Element of bool the carrier of V
B is right_complementable Element of the carrier of V
C is right_complementable Element of the carrier of V
B + C is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (B,C) is right_complementable Element of the carrier of V
[B,C] is set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
the addF of V . [B,C] is set
the carrier of GF is non empty set
B is right_complementable Element of the carrier of GF
C is right_complementable Element of the carrier of V
B * C is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (B,C) is right_complementable Element of the carrier of V
[B,C] is set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
the lmult of V . [B,C] is set

the carrier of V is non empty set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty set
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the addF of V || the carrier of V is Relation-like Function-like set
the addF of V | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the lmult of V | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
GF is set

the carrier of W is non empty set
the carrier of B is non empty set
GF is set

the carrier of W is non empty set
the carrier of u is non empty set

the carrier of V is non empty set

the carrier of u is non empty set
W is right_complementable Element of the carrier of u

0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u
0. V is V49(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V

0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u

0. W is V49(W) right_complementable Element of the carrier of W
the carrier of W is non empty set
the ZeroF of W is right_complementable Element of the carrier of W
0. V is V49(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
u + W is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the addF of V . [u,W] is set

the carrier of B is non empty set
C is right_complementable Element of the carrier of B
C is right_complementable Element of the carrier of B
C + C is right_complementable Element of the carrier of B
the addF of B is Relation-like Function-like V18([: the carrier of B, the carrier of B:], the carrier of B) Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
the addF of B . (C,C) is right_complementable Element of the carrier of B
[C,C] is set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the addF of B . [C,C] is set
the addF of V || the carrier of B is Relation-like Function-like set
the addF of V | [: the carrier of B, the carrier of B:] is Relation-like Function-like set
[C,C] is Element of [: the carrier of B, the carrier of B:]
( the addF of V || the carrier of B) . [C,C] is set

the carrier of GF is non empty set

the carrier of V is non empty set
u is right_complementable Element of the carrier of GF
W is right_complementable Element of the carrier of V
u * W is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the lmult of V . [u,W] is set

the carrier of B is non empty set
C is right_complementable Element of the carrier of B
u * C is right_complementable Element of the carrier of B
the lmult of B is Relation-like Function-like V18([: the carrier of GF, the carrier of B:], the carrier of B) Element of bool [:[: the carrier of GF, the carrier of B:], the carrier of B:]
[: the carrier of GF, the carrier of B:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of B:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of B:], the carrier of B:] is non empty set
the lmult of B . (u,C) is right_complementable Element of the carrier of B
[u,C] is set
{u,C} is non empty set
{{u,C},{u}} is non empty set
the lmult of B . [u,C] is set
the lmult of V | [: the carrier of GF, the carrier of B:] is Relation-like Function-like set
[u,C] is Element of [: the carrier of GF, the carrier of B:]
( the lmult of V | [: the carrier of GF, the carrier of B:]) . [u,C] is set

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V

the carrier of W is non empty set
B is right_complementable Element of the carrier of W
- B is right_complementable Element of the carrier of W
1_ GF is right_complementable Element of the carrier of GF
the carrier of GF is non empty set
1. GF is right_complementable Element of the carrier of GF
the OneF of GF is right_complementable Element of the carrier of GF
- (1_ GF) is right_complementable Element of the carrier of GF
(- (1_ GF)) * u is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((- (1_ GF)),u) is right_complementable Element of the carrier of V
[(- (1_ GF)),u] is set
{(- (1_ GF)),u} is non empty set
{(- (1_ GF))} is non empty set
{{(- (1_ GF)),u},{(- (1_ GF))}} is non empty set
the lmult of V . [(- (1_ GF)),u] is set
(- (1_ GF)) * B is right_complementable Element of the carrier of W
the lmult of W is Relation-like Function-like V18([: the carrier of GF, the carrier of W:], the carrier of W) Element of bool [:[: the carrier of GF, the carrier of W:], the carrier of W:]
[: the carrier of GF, the carrier of W:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of W:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of W:], the carrier of W:] is non empty set
the lmult of W . ((- (1_ GF)),B) is right_complementable Element of the carrier of W
[(- (1_ GF)),B] is set
{(- (1_ GF)),B} is non empty set
{{(- (1_ GF)),B},{(- (1_ GF))}} is non empty set
the lmult of W . [(- (1_ GF)),B] is set

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
u - W is right_complementable Element of the carrier of V
- W is right_complementable Element of the carrier of V
u + (- W) is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (u,(- W)) is right_complementable Element of the carrier of V
[u,(- W)] is set
{u,(- W)} is non empty set
{u} is non empty set
{{u,(- W)},{u}} is non empty set
the addF of V . [u,(- W)] is set

the carrier of B is non empty set
C is right_complementable Element of the carrier of B
C is right_complementable Element of the carrier of B
C - C is right_complementable Element of the carrier of B
- C is right_complementable Element of the carrier of B
C + (- C) is right_complementable Element of the carrier of B
the addF of B is Relation-like Function-like V18([: the carrier of B, the carrier of B:], the carrier of B) Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is Relation-like non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
the addF of B . (C,(- C)) is right_complementable Element of the carrier of B
[C,(- C)] is set
{C,(- C)} is non empty set
{C} is non empty set
{{C,(- C)},{C}} is non empty set
the addF of B . [C,(- C)] is set

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

the carrier of u is non empty set
W is Element of bool the carrier of V
C is right_complementable Element of the carrier of V
c8 is right_complementable Element of the carrier of V
C + c8 is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (C,c8) is right_complementable Element of the carrier of V
[C,c8] is set
{C,c8} is non empty set
{C} is non empty set
{{C,c8},{C}} is non empty set
the addF of V . [C,c8] is set

the carrier of C is non empty set
x is right_complementable Element of the carrier of C
x is right_complementable Element of the carrier of C
x + x is right_complementable Element of the carrier of C
the addF of C is Relation-like Function-like V18([: the carrier of C, the carrier of C:], the carrier of C) Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is non empty set
the addF of C . (x,x) is right_complementable Element of the carrier of C
[x,x] is set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
the addF of C . [x,x] is set
z is right_complementable Element of the carrier of u
the carrier of GF is non empty set
C is right_complementable Element of the carrier of GF
c8 is right_complementable Element of the carrier of V
C * c8 is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (C,c8) is right_complementable Element of the carrier of V
[C,c8] is set
{C,c8} is non empty set
{C} is non empty set
{{C,c8},{C}} is non empty set
the lmult of V . [C,c8] is set

the carrier of C is non empty set
x is right_complementable Element of the carrier of C
C * x is right_complementable Element of the carrier of C
the lmult of C is Relation-like Function-like V18([: the carrier of GF, the carrier of C:], the carrier of C) Element of bool [:[: the carrier of GF, the carrier of C:], the carrier of C:]
[: the carrier of GF, the carrier of C:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of C:], the carrier of C:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of C:], the carrier of C:] is non empty set
the lmult of C . (C,x) is right_complementable Element of the carrier of C
[C,x] is set
{C,x} is non empty set
{{C,x},{C}} is non empty set
the lmult of C . [C,x] is set
x is right_complementable Element of the carrier of u

0. V is V49(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V

0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u

0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u

0. V is V49(V) right_complementable Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is right_complementable Element of the carrier of V

0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
u + W is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the addF of V . [u,W] is set

bool the carrier of V is non empty set
the carrier of B is non empty set
C is Element of bool the carrier of V

the carrier of GF is non empty set

the carrier of V is non empty set
u is right_complementable Element of the carrier of GF
W is right_complementable Element of the carrier of V
u * W is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . (u,W) is right_complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the lmult of V . [u,W] is set

bool the carrier of V is non empty set
the carrier of B is non empty set
C is Element of bool the carrier of V

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V

1_ GF is right_complementable Element of the carrier of GF
the carrier of GF is non empty set
1. GF is right_complementable Element of the carrier of GF
the OneF of GF is right_complementable Element of the carrier of GF
- (1_ GF) is right_complementable Element of the carrier of GF
(- (1_ GF)) * u is right_complementable Element of the carrier of V
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V . ((- (1_ GF)),u) is right_complementable Element of the carrier of V
[(- (1_ GF)),u] is set
{(- (1_ GF)),u} is non empty set
{(- (1_ GF))} is non empty set
{{(- (1_ GF)),u},{(- (1_ GF))}} is non empty set
the lmult of V . [(- (1_ GF)),u] is set

the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is right_complementable Element of the carrier of V
u - W is right_complementable Element of the carrier of V
- W is right_complementable Element of the carrier of V
u + (- W) is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V . (u,(- W)) is right_complementable Element of the carrier of V
[u,(- W)] is set
{u,(- W)} is non empty set
{u} is non empty set
{{u,(- W)},{u}} is non empty set
the addF of V . [u,(- W)] is set

the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty set
the carrier of V is non empty set
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of V | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
the addF of V is Relation-like 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 addF of V || the carrier of V is Relation-like Function-like set
the addF of V | [: the carrier of V, the carrier of V:] is Relation-like Function-like set

the carrier of V is non empty set
the carrier of u is non empty set
the addF of V is Relation-like 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 addF of u is Relation-like Function-like V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]
[: the carrier of u, the carrier of u:] is Relation-like non empty set
[:[: the carrier of u, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of u:], the carrier of u:] is non empty set
the addF of V || the carrier of u is Relation-like Function-like set
the addF of V | [: the carrier of u, the carrier of u:] is Relation-like Function-like set
the addF of u || the carrier of V is Relation-like Function-like set
the addF of u | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty set
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of u is Relation-like Function-like V18([: the carrier of GF, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of GF, the carrier of u:], the carrier of u:]
[: the carrier of GF, the carrier of u:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of u:], the carrier of u:] is non empty set
the lmult of u | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
0. u is V49(u) right_complementable Element of the carrier of u
the ZeroF of u is right_complementable Element of the carrier of u
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
the lmult of V | [: the carrier of GF, the carrier of u:] is Relation-like Function-like set

the carrier of V is non empty set
the carrier of u is non empty set
the carrier of W is non empty set
the addF of V is Relation-like 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 addF of W is Relation-like Function-like V18([: the carrier of W, the carrier of W:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is Relation-like non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W || the carrier of V is Relation-like Function-like set
the addF of W | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the addF of u is Relation-like Function-like V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]
[: the carrier of u, the carrier of u:] is Relation-like non empty set
[:[: the carrier of u, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of u:], the carrier of u:] is non empty set
the addF of u || the carrier of V is Relation-like Function-like set
the addF of u | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the addF of W || the carrier of u is Relation-like Function-like set
the addF of W | [: the carrier of u, the carrier of u:] is Relation-like Function-like set
( the addF of W || the carrier of u) || the carrier of V is Relation-like Function-like set
( the addF of W || the carrier of u) | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the lmult of W is Relation-like Function-like V18([: the carrier of GF, the carrier of W:], the carrier of W) Element of bool [:[: the carrier of GF, the carrier of W:], the carrier of W:]
the carrier of GF is non empty set
[: the carrier of GF, the carrier of W:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of W:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of W:], the carrier of W:] is non empty set
the lmult of u is Relation-like Function-like V18([: the carrier of GF, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of GF, the carrier of u:], the carrier of u:]
[: the carrier of GF, the carrier of u:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of u:], the carrier of u:] is non empty set
the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the lmult of u | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
the lmult of W | [: the carrier of GF, the carrier of u:] is Relation-like Function-like set
( the lmult of W | [: the carrier of GF, the carrier of u:]) | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
the lmult of W | [: the carrier of GF, the carrier of V:] is Relation-like Function-like set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. u is V49(u) right_complementable Element of the carrier of u
the ZeroF of u is right_complementable Element of the carrier of u
0. W is V49(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W

the carrier of u is non empty set

the carrier of W is non empty set
the lmult of u is Relation-like Function-like V18([: the carrier of GF, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of GF, the carrier of u:], the carrier of u:]
the carrier of GF is non empty set
[: the carrier of GF, the carrier of u:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of u:], the carrier of u:] is non empty set
the lmult of W is Relation-like Function-like V18([: the carrier of GF, the carrier of W:], the carrier of W) Element of bool [:[: the carrier of GF, the carrier of W:], the carrier of W:]
[: the carrier of GF, the carrier of W:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of W:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of W:], the carrier of W:] is non empty set
the addF of V is Relation-like 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 is non empty set
[: 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 lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the addF of u is Relation-like Function-like V18([: the carrier of u, the carrier of u:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of u:], the carrier of u:]
[: the carrier of u, the carrier of u:] is Relation-like non empty set
[:[: the carrier of u, the carrier of u:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of u:], the carrier of u:] is non empty set
the addF of V || the carrier of u is Relation-like Function-like set
the addF of V | [: the carrier of u, the carrier of u:] is Relation-like Function-like set
the addF of W is Relation-like Function-like V18([: the carrier of W, the carrier of W:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is Relation-like non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of V || the carrier of W is Relation-like Function-like set
the addF of V | [: the carrier of W, the carrier of W:] is Relation-like Function-like set
the addF of W || the carrier of u is Relation-like Function-like set
the addF of W | [: the carrier of u, the carrier of u:] is Relation-like Function-like set
the lmult of V | [: the carrier of GF, the carrier of u:] is Relation-like Function-like set
the lmult of V | [: the carrier of GF, the carrier of W:] is Relation-like Function-like set
the lmult of W | [: the carrier of GF, the carrier of u:] is Relation-like Function-like set
0. u is V49(u) right_complementable Element of the carrier of u
the ZeroF of u is right_complementable Element of the carrier of u
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
0. W is V49(W) right_complementable Element of the carrier of W
the ZeroF of W is right_complementable Element of the carrier of W

the carrier of V is non empty set

the carrier of u is non empty set
the carrier of W is non empty set
B is set
C is right_complementable Element of the carrier of V

the lmult of V is Relation-like Function-like V18([: the carrier of GF, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of GF, the carrier of V:], the carrier of V:]
the carrier of GF is non empty set
the carrier of V is non empty set
[: the carrier of GF, the carrier of V:] is Relation-like non empty set
[:[: the carrier of GF, the carrier of V:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of V:], the carrier of V:] is non empty set
the addF of V is Relation-like 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
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is non empty strict VectSpStr over GF
the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is non empty set
B is right_complementable Element of the carrier of GF
C is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
C is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
C + C is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
the addF of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Relation-like Function-like V18([: the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #), the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) Element of bool [:[: the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #), the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):]
[: the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #), the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is Relation-like non empty set
[:[: the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #), the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is Relation-like non empty set
bool [:[: the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #), the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is non empty set
the addF of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) . (C,C) is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
[C,C] is set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the addF of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) . [C,C] is set
B * (C + C) is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
the lmult of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) is Relation-like Function-like V18([: the carrier of GF, the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)) Element of bool [:[: the carrier of GF, the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):]
[: the carrier of GF, the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is Relation-like non empty set
[:[: the carrier of GF, the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is Relation-like non empty set
bool [:[: the carrier of GF, the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):], the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #):] is non empty set
the lmult of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #) . (B,(C + C)) is Element of the carrier of VectSpStr(# the carrier of V, the addF of V,(0. V), the lmult of V #)
[B,(C + C)] is set
{B,(C + C)} is non empty set