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
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
the Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty set
1 is non empty set
GF is non empty right_complementable unital associative commutative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of GF is non empty set
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
GF 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 GF
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
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (V,u)
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (V,u)
the carrier of W is non empty set
the carrier of B is non empty set
GF is set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over V
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (V,u)
the carrier of W is non empty set
the carrier of u is non empty set
GF 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 GF
the carrier of V is non empty set
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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. 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
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of GF is non empty set
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
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
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
GF 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 GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
the carrier of V is non empty set
bool the carrier of V is non empty set
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
C is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
C is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
GF 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 GF
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
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
GF 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 GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of GF is non empty set
V is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
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
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,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
GF 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 GF
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
B is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
GF 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 GF
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
GF is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
V is non empty right_complementable strict vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF
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
GF 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 GF
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
the carrier of u is non empty set
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
the carrier of V is non empty set
u is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
W is non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed (GF,V)
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
GF 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 GF
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