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

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

{ (b

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

c

x is right_complementable Element of the carrier of V

c

the addF of V . (c

[c

{c

{c

{{c

the addF of V . [c

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

(c

the addF of V . ((c

[(c

{(c

{(c

{{(c

the addF of V . [(c

((c

the addF of V . (((c

[((c

{((c

{((c

{{((c

the addF of V . [((c

c

the addF of V . (c

[c

{c

{{c

the addF of V . [c

(c

the addF of V . ((c

[(c

{(c

{(c

{{(c

the addF of V . [(c

((c

the addF of V . (((c

[((c

{((c

{((c

{{((c

the addF of V . [((c

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

(c

the addF of V . ((c

[(c

{(c

{{(c

the addF of V . [(c

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

c

x is right_complementable Element of the carrier of V

c

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

{c

{c

{{c

the addF of V . [c

C * c

the lmult of V . (C,c

[C,c

{C,c

{{C,c

the lmult of V . [C,c

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

the addF of V . ((C * c

[(C * c

{(C * c

{(C * c

{{(C * c

the addF of V . [(C * c

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

c

C + c

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

[C,c

{C,c

{C} is non empty set

{{C,c

the addF of V . [C,c

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

c

C * c

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

[C,c

{C,c

{C} is non empty set

{{C,c

the lmult of V . [C,c

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