:: RMOD_2 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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
bool the carrier of V is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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. R is V49(R) right_complementable Element of the carrier of R
the carrier of R is non empty set
the ZeroF of R is right_complementable Element of the carrier of R
B is right_complementable Element of the carrier of V
B * (0. R) is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (B,(0. R)) is right_complementable Element of the carrier of V
[B,(0. R)] is set
{B,(0. R)} is non empty set
{B} is non empty set
{{B,(0. R)},{B}} is non empty set
the rmult of V . [B,(0. R)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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_ R is right_complementable Element of the carrier of R
the carrier of R is non empty set
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
- (1_ R) is right_complementable Element of the carrier of R
W * (- (1_ R)) is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (W,(- (1_ R))) is right_complementable Element of the carrier of V
[W,(- (1_ R))] is set
{W,(- (1_ R))} is non empty set
{W} is non empty set
{{W,(- (1_ R))},{W}} is non empty set
the rmult of V . [W,(- (1_ R))] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 R is non empty set
u is right_complementable Element of the carrier of R
W is right_complementable Element of the carrier of V
W * u is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (W,u) is right_complementable Element of the carrier of V
[W,u] is set
{W,u} is non empty set
{W} is non empty set
{{W,u},{W}} is non empty set
the rmult of V . [W,u] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 R is non empty set
W is right_complementable Element of the carrier of R
B is right_complementable Element of the carrier of V
B * W is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (B,W) is right_complementable Element of the carrier of V
[B,W] is set
{B,W} is non empty set
{B} is non empty set
{{B,W},{B}} is non empty set
the rmult of V . [B,W] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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₁ + b₂) where b₁, b₂ is right_complementable Element of the carrier of V : ( b₁ in u & b₂ in W ) } is set
B is Element of bool the carrier of V
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₈ is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c₈ + x is right_complementable Element of the carrier of V
the addF of V . (c₈,x) is right_complementable Element of the carrier of V
[c₈,x] is set
{c₈,x} is non empty set
{c₈} is non empty set
{{c₈,x},{c₈}} is non empty set
the addF of V . [c₈,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
(c₈ + x) + x is right_complementable Element of the carrier of V
the addF of V . ((c₈ + x),x) is right_complementable Element of the carrier of V
[(c₈ + x),x] is set
{(c₈ + x),x} is non empty set
{(c₈ + x)} is non empty set
{{(c₈ + x),x},{(c₈ + x)}} is non empty set
the addF of V . [(c₈ + x),x] is set
((c₈ + x) + x) + z is right_complementable Element of the carrier of V
the addF of V . (((c₈ + x) + x),z) is right_complementable Element of the carrier of V
[((c₈ + x) + x),z] is set
{((c₈ + x) + x),z} is non empty set
{((c₈ + x) + x)} is non empty set
{{((c₈ + x) + x),z},{((c₈ + x) + x)}} is non empty set
the addF of V . [((c₈ + x) + x),z] is set
c₈ + x is right_complementable Element of the carrier of V
the addF 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 addF of V . [c₈,x] is set
(c₈ + x) + x is right_complementable Element of the carrier of V
the addF of V . ((c₈ + x),x) is right_complementable Element of the carrier of V
[(c₈ + x),x] is set
{(c₈ + x),x} is non empty set
{(c₈ + x)} is non empty set
{{(c₈ + x),x},{(c₈ + x)}} is non empty set
the addF of V . [(c₈ + x),x] is set
((c₈ + x) + x) + z is right_complementable Element of the carrier of V
the addF of V . (((c₈ + x) + x),z) is right_complementable Element of the carrier of V
[((c₈ + x) + x),z] is set
{((c₈ + x) + x),z} is non empty set
{((c₈ + x) + x)} is non empty set
{{((c₈ + x) + x),z},{((c₈ + x) + x)}} is non empty set
the addF of V . [((c₈ + 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
(c₈ + x) + (x + z) is right_complementable Element of the carrier of V
the addF of V . ((c₈ + x),(x + z)) is right_complementable Element of the carrier of V
[(c₈ + x),(x + z)] is set
{(c₈ + x),(x + z)} is non empty set
{{(c₈ + x),(x + z)},{(c₈ + x)}} is non empty set
the addF of V . [(c₈ + x),(x + z)] is set
the carrier of R is non empty set
C is right_complementable Element of the carrier of R
C is right_complementable Element of the carrier of V
C * C is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult 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 rmult of V . [C,C] is set
c₈ is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c₈ + 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 . (c₈,x) is right_complementable Element of the carrier of V
[c₈,x] is set
{c₈,x} is non empty set
{c₈} is non empty set
{{c₈,x},{c₈}} is non empty set
the addF of V . [c₈,x] is set
c₈ * C is right_complementable Element of the carrier of V
the rmult of V . (c₈,C) is right_complementable Element of the carrier of V
[c₈,C] is set
{c₈,C} is non empty set
{{c₈,C},{c₈}} is non empty set
the rmult of V . [c₈,C] is set
x * C is right_complementable Element of the carrier of V
the rmult of V . (x,C) is right_complementable Element of the carrier of V
[x,C] is set
{x,C} is non empty set
{x} is non empty set
{{x,C},{x}} is non empty set
the rmult of V . [x,C] is set
(c₈ * C) + (x * C) is right_complementable Element of the carrier of V
the addF of V . ((c₈ * C),(x * C)) is right_complementable Element of the carrier of V
[(c₈ * C),(x * C)] is set
{(c₈ * C),(x * C)} is non empty set
{(c₈ * C)} is non empty set
{{(c₈ * C),(x * C)},{(c₈ * C)}} is non empty set
the addF of V . [(c₈ * C),(x * C)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 R is non empty set
B is right_complementable Element of the carrier of R
C is right_complementable Element of the carrier of V
C * B is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (C,B) is right_complementable Element of the carrier of V
[C,B] is set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
the rmult of V . [C,B] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the addF of V | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the rmult of V | [: the carrier of V, the carrier of R:] is Relation-like Function-like set
R is set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (V,u)
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (V,u)
the carrier of W is non empty set
the carrier of B is non empty set
R is set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (V,u)
the carrier of W is non empty set
the carrier of u is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,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 Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,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, 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, the carrier of B:]) . [C,C] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
V is right_complementable Element of the carrier of R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
W * V is right_complementable Element of the carrier of u
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of u . (W,V) is right_complementable Element of the carrier of u
[W,V] is set
{W,V} is non empty set
{W} is non empty set
{{W,V},{W}} is non empty set
the rmult of u . [W,V] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,u)
the carrier of B is non empty set
C is right_complementable Element of the carrier of B
C * V is right_complementable Element of the carrier of B
the rmult of B is Relation-like Function-like V18([: the carrier of B, the carrier of R:], the carrier of B) Element of bool [:[: the carrier of B, the carrier of R:], the carrier of B:]
[: the carrier of B, the carrier of R:] is Relation-like non empty set
[:[: the carrier of B, the carrier of R:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of R:], the carrier of B:] is non empty set
the rmult of B . (C,V) is right_complementable Element of the carrier of B
[C,V] is set
{C,V} is non empty set
{C} is non empty set
{{C,V},{C}} is non empty set
the rmult of B . [C,V] is set
the rmult of u | [: the carrier of B, the carrier of R:] is Relation-like Function-like set
[C,V] is Element of [: the carrier of B, the carrier of R:]
( the rmult of u | [: the carrier of B, the carrier of R:]) . [C,V] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,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_ R is right_complementable Element of the carrier of R
the carrier of R is non empty set
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
- (1_ R) is right_complementable Element of the carrier of R
u * (- (1_ R)) is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (u,(- (1_ R))) is right_complementable Element of the carrier of V
[u,(- (1_ R))] is set
{u,(- (1_ R))} is non empty set
{u} is non empty set
{{u,(- (1_ R))},{u}} is non empty set
the rmult of V . [u,(- (1_ R))] is set
B * (- (1_ R)) is right_complementable Element of the carrier of W
the rmult of W is Relation-like Function-like V18([: the carrier of W, the carrier of R:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of R:], the carrier of W:]
[: the carrier of W, the carrier of R:] is Relation-like non empty set
[:[: the carrier of W, the carrier of R:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of R:], the carrier of W:] is non empty set
the rmult of W . (B,(- (1_ R))) is right_complementable Element of the carrier of W
[B,(- (1_ R))] is set
{B,(- (1_ R))} is non empty set
{B} is non empty set
{{B,(- (1_ R))},{B}} is non empty set
the rmult of W . [B,(- (1_ R))] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of W is non empty 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
C is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 W
the carrier of R is non empty set
C is right_complementable Element of the carrier of R
c₈ is right_complementable Element of the carrier of V
c₈ * C is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult 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 rmult of V . [c₈,C] is set
C is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of C is non empty set
x is right_complementable Element of the carrier of C
x * C is right_complementable Element of the carrier of C
the rmult of C is Relation-like Function-like V18([: the carrier of C, the carrier of R:], the carrier of C) Element of bool [:[: the carrier of C, the carrier of R:], the carrier of C:]
[: the carrier of C, the carrier of R:] is Relation-like non empty set
[:[: the carrier of C, the carrier of R:], the carrier of C:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of R:], the carrier of C:] is non empty set
the rmult of C . (x,C) is right_complementable Element of the carrier of C
[x,C] is set
{x,C} is non empty set
{x} is non empty set
{{x,C},{x}} is non empty set
the rmult of C . [x,C] is set
x is right_complementable Element of the carrier of W
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,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 Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
V is right_complementable Element of the carrier of R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
W * V is right_complementable Element of the carrier of u
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of u . (W,V) is right_complementable Element of the carrier of u
[W,V] is set
{W,V} is non empty set
{W} is non empty set
{{W,V},{W}} is non empty set
the rmult of u . [W,V] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,u)
bool the carrier of u is non empty set
the carrier of B is non empty set
C is Element of bool the carrier of u
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
1_ R is right_complementable Element of the carrier of R
the carrier of R is non empty set
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
- (1_ R) is right_complementable Element of the carrier of R
u * (- (1_ R)) is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (u,(- (1_ R))) is right_complementable Element of the carrier of V
[u,(- (1_ R))] is set
{u,(- (1_ R))} is non empty set
{u} is non empty set
{{u,(- (1_ R))},{u}} is non empty set
the rmult of V . [u,(- (1_ R))] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of V is non empty set
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V | [: the carrier of V, the carrier of R:] 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, the carrier of V:] is Relation-like Function-like set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like RightModStr over R
V is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like RightModStr over R
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 rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of u | [: the carrier of V, the carrier of R:] 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 rmult of V | [: the carrier of u, the carrier of R:] is Relation-like Function-like set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of V is non empty set
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], 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
RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is non empty strict RightModStr over R
the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is non empty set
B is right_complementable Element of the carrier of R
C is right_complementable Element of the carrier of R
B + C is right_complementable Element of the carrier of R
the addF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is Relation-like non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (B,C) is right_complementable Element of the carrier of R
[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 R . [B,C] is set
C * B is right_complementable Element of the carrier of R
the multF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (C,B) is right_complementable Element of the carrier of R
[C,B] is set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
the multF of R . [C,B] is set
1_ R is right_complementable Element of the carrier of R
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
c₈ is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C + c₈ is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,c₈) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,c₈] is set
(C + c₈) * B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of R:] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((C + c₈),B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C + c₈),B] is set
{(C + c₈),B} is non empty set
{(C + c₈)} is non empty set
{{(C + c₈),B},{(C + c₈)}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C + c₈),B] is set
C * B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,B] is set
{C,B} is non empty set
{{C,B},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,B] is set
c₈ * B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (c₈,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[c₈,B] is set
{c₈,B} is non empty set
{c₈} is non empty set
{{c₈,B},{c₈}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [c₈,B] is set
(C * B) + (c₈ * B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((C * B),(c₈ * B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C * B),(c₈ * B)] is set
{(C * B),(c₈ * B)} is non empty set
{(C * B)} is non empty set
{{(C * B),(c₈ * B)},{(C * B)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C * B),(c₈ * B)] is set
C * (B + C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,(B + C)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,(B + C)] is set
{C,(B + C)} is non empty set
{{C,(B + C)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,(B + C)] is set
C * C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,C] is set
{C,C} is non empty set
{{C,C},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,C] is set
(C * B) + (C * C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((C * B),(C * C)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C * B),(C * C)] is set
{(C * B),(C * C)} is non empty set
{{(C * B),(C * C)},{(C * B)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C * B),(C * C)] is set
C * (C * B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,(C * B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,(C * B)] is set
{C,(C * B)} is non empty set
{{C,(C * B)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,(C * B)] is set
(C * C) * B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((C * C),B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C * C),B] is set
{(C * C),B} is non empty set
{(C * C)} is non empty set
{{(C * C),B},{(C * C)}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C * C),B] is set
C * (1_ R) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,(1_ R)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,(1_ R)] is set
{C,(1_ R)} is non empty set
{{C,(1_ R)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,(1_ R)] is set
x is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
x + x is right_complementable Element of the carrier of V
the addF of V . (x,x) is right_complementable Element of the carrier of V
[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 V . [x,x] is set
(x + x) * B is right_complementable Element of the carrier of V
the rmult of V . ((x + x),B) is right_complementable Element of the carrier of V
[(x + x),B] is set
{(x + x),B} is non empty set
{(x + x)} is non empty set
{{(x + x),B},{(x + x)}} is non empty set
the rmult of V . [(x + x),B] is set
x * B is right_complementable Element of the carrier of V
the rmult of V . (x,B) is right_complementable Element of the carrier of V
[x,B] is set
{x,B} is non empty set
{{x,B},{x}} is non empty set
the rmult of V . [x,B] is set
x * B is right_complementable Element of the carrier of V
the rmult of V . (x,B) is right_complementable Element of the carrier of V
[x,B] is set
{x,B} is non empty set
{x} is non empty set
{{x,B},{x}} is non empty set
the rmult of V . [x,B] is set
(x * B) + (x * B) is right_complementable Element of the carrier of V
the addF of V . ((x * B),(x * B)) is right_complementable Element of the carrier of V
[(x * B),(x * B)] is set
{(x * B),(x * B)} is non empty set
{(x * B)} is non empty set
{{(x * B),(x * B)},{(x * B)}} is non empty set
the addF of V . [(x * B),(x * B)] is set
B + C is right_complementable Element of the carrier of R
C * (B + C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,(B + C)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,(B + C)] is set
{C,(B + C)} is non empty set
{{C,(B + C)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,(B + C)] is set
x * (B + C) is right_complementable Element of the carrier of V
the rmult of V . (x,(B + C)) is right_complementable Element of the carrier of V
[x,(B + C)] is set
{x,(B + C)} is non empty set
{{x,(B + C)},{x}} is non empty set
the rmult of V . [x,(B + C)] is set
x * C is right_complementable Element of the carrier of V
the rmult of V . (x,C) is right_complementable Element of the carrier of V
[x,C] is set
{x,C} is non empty set
{{x,C},{x}} is non empty set
the rmult of V . [x,C] is set
(x * B) + (x * C) is right_complementable Element of the carrier of V
the addF of V . ((x * B),(x * C)) is right_complementable Element of the carrier of V
[(x * B),(x * C)] is set
{(x * B),(x * C)} is non empty set
{{(x * B),(x * C)},{(x * B)}} is non empty set
the addF of V . [(x * B),(x * C)] is set
x * (C * B) is right_complementable Element of the carrier of V
the rmult of V . (x,(C * B)) is right_complementable Element of the carrier of V
[x,(C * B)] is set
{x,(C * B)} is non empty set
{{x,(C * B)},{x}} is non empty set
the rmult of V . [x,(C * B)] is set
(x * C) * B is right_complementable Element of the carrier of V
the rmult of V . ((x * C),B) is right_complementable Element of the carrier of V
[(x * C),B] is set
{(x * C),B} is non empty set
{(x * C)} is non empty set
{{(x * C),B},{(x * C)}} is non empty set
the rmult of V . [(x * C),B] is set
x * (1_ R) is right_complementable Element of the carrier of V
the rmult of V . (x,(1_ R)) is right_complementable Element of the carrier of V
[x,(1_ R)] is set
{x,(1_ R)} is non empty set
{{x,(1_ R)},{x}} is non empty set
the rmult of V . [x,(1_ R)] is set
the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is non empty set
C is right_complementable Element of the carrier of V
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
c₈ is right_complementable Element of the carrier of V
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,C] is set
C + c₈ is right_complementable Element of the carrier of V
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
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,C] is set
C + B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,B] is set
{C,B} is non empty set
{C} is non empty set
{{C,B},{C}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,B] 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 . (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
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,C] is set
(B + C) + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((B + C),C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(B + C),C] is set
{(B + C),C} is non empty set
{(B + C)} is non empty set
{{(B + C),C},{(B + C)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(B + C),C] is set
c₈ is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c₈ + x is right_complementable Element of the carrier of V
the addF of V . (c₈,x) is right_complementable Element of the carrier of V
[c₈,x] is set
{c₈,x} is non empty set
{c₈} is non empty set
{{c₈,x},{c₈}} is non empty set
the addF of V . [c₈,x] is set
x is right_complementable Element of the carrier of V
(c₈ + x) + x is right_complementable Element of the carrier of V
the addF of V . ((c₈ + x),x) is right_complementable Element of the carrier of V
[(c₈ + x),x] is set
{(c₈ + x),x} is non empty set
{(c₈ + x)} is non empty set
{{(c₈ + x),x},{(c₈ + x)}} is non empty set
the addF of V . [(c₈ + x),x] is set
x + x is right_complementable Element of the carrier of V
the addF of V . (x,x) is right_complementable Element of the carrier of V
[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 V . [x,x] is set
c₈ + (x + x) is right_complementable Element of the carrier of V
the addF of V . (c₈,(x + x)) is right_complementable Element of the carrier of V
[c₈,(x + x)] is set
{c₈,(x + x)} is non empty set
{{c₈,(x + x)},{c₈}} is non empty set
the addF of V . [c₈,(x + x)] is set
C + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (C,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,C] is set
B + (C + C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,(C + C)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[B,(C + C)] is set
{B,(C + C)} is non empty set
{{B,(C + C)},{B}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,(C + C)] is set
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is V49( RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the ZeroF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
B + (0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,(0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #))) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[B,(0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #))] is set
{B,(0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #))} is non empty set
{B} is non empty set
{{B,(0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #))},{B}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,(0. RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #))] is set
C is right_complementable Element of the carrier of V
C + (0. V) is right_complementable Element of the carrier of V
the addF of V . (C,(0. V)) is right_complementable Element of the carrier of V
[C,(0. V)] is set
{C,(0. V)} is non empty set
{C} is non empty set
{{C,(0. V)},{C}} is non empty set
the addF of V . [C,(0. V)] is set
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
comp V is Relation-like Function-like V18( the carrier of V, the carrier of V) Element of bool [: the carrier of V, the carrier of V:]
bool [: the carrier of V, the carrier of V:] is non empty set
C is right_complementable Element of the carrier of V
(comp V) . C is right_complementable Element of the carrier of V
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult 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 RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [B,C] is set
- 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 . (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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
0. B is V49(B) right_complementable Element of the carrier of B
the carrier of B is non empty set
the ZeroF of B 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 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
the rmult of B is Relation-like Function-like V18([: the carrier of B, the carrier of R:], the carrier of B) Element of bool [:[: the carrier of B, the carrier of R:], the carrier of B:]
[: the carrier of B, the carrier of R:] is Relation-like non empty set
[:[: the carrier of B, the carrier of R:], the carrier of B:] is Relation-like non empty set
bool [:[: the carrier of B, the carrier of R:], the carrier of B:] is non empty set
the rmult of V | [: the carrier of B, the carrier of R:] is Relation-like Function-like set
C is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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, 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 rmult of W is Relation-like Function-like V18([: the carrier of W, the carrier of R:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of R:], the carrier of W:]
the carrier of R is non empty set
[: the carrier of W, the carrier of R:] is Relation-like non empty set
[:[: the carrier of W, the carrier of R:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of R:], the carrier of W:] is non empty set
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of u | [: the carrier of V, the carrier of R:] is Relation-like Function-like set
the rmult of W | [: the carrier of u, the carrier of R:] is Relation-like Function-like set
( the rmult of W | [: the carrier of u, the carrier of R:]) | [: the carrier of V, the carrier of R:] is Relation-like Function-like set
the rmult of W | [: the carrier of V, the carrier of R:] 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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of W is non empty set
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
the carrier of R is non empty set
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of W is Relation-like Function-like V18([: the carrier of W, the carrier of R:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of R:], the carrier of W:]
[: the carrier of W, the carrier of R:] is Relation-like non empty set
[:[: the carrier of W, the carrier of R:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of R:], 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 rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], 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, the carrier of u:] is Relation-like Function-like set
the rmult of V | [: the carrier of u, the carrier of R:] is Relation-like Function-like set
the rmult of V | [: the carrier of W, the carrier of R:] is Relation-like Function-like set
the rmult of W | [: the carrier of u, the carrier of R:] 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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of u is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of W is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,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
C is right_complementable Element of the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like RightModStr over R
the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of u is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like RightModStr over R
the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
W is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
bool the carrier of V is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of W is non empty set
u is Element of bool the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 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
comp V is Relation-like Function-like V18( 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 Relation-like non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
(comp V) | W is Relation-like Function-like set
dom (comp V) is set
dom ((comp V) | W) is set
rng ((comp V) | W) is set
c₈ is set
x is set
((comp V) | W) . x is set
x is right_complementable Element of the carrier of V
(comp V) . x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
[:W, the carrier of R:] is Relation-like non empty set
the rmult of V | [:W, the carrier of R:] is Relation-like Function-like set
dom the rmult of V is set
dom ( the rmult of V | [:W, the carrier of R:]) is set
rng ( the rmult of V | [:W, the carrier of R:]) is set
x is set
x is set
( the rmult of V | [:W, the carrier of R:]) . x is set
z is set
u1 is set
[z,u1] is set
{z,u1} is non empty set
{z} is non empty set
{{z,u1},{z}} is non empty set
W is right_complementable Element of the carrier of R
W is right_complementable Element of the carrier of V
W * W is right_complementable Element of the carrier of V
the rmult of V . (W,W) is right_complementable Element of the carrier of V
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the rmult of V . [W,W] is set
[:W,W:] is Relation-like non empty set
bool [:W,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:], 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 is Relation-like Function-like set
the addF of V | [:W,W:] is Relation-like Function-like set
dom the addF of V is set
dom ( the addF of V || W) is set
rng ( the addF of V || W) is set
z is set
u1 is set
( the addF of V || W) . u1 is set
W is set
W is set
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
W is right_complementable Element of the carrier of V
c₁₆ is right_complementable Element of the carrier of V
W + c₁₆ is right_complementable Element of the carrier of V
the addF of V . (W,c₁₆) is right_complementable Element of the carrier of V
[W,c₁₆] is set
{W,c₁₆} is non empty set
{W} is non empty set
{{W,c₁₆},{W}} is non empty set
the addF of V . [W,c₁₆] is set
[:[:W, the carrier of R:],W:] is Relation-like non empty set
bool [:[:W, the carrier of R:],W:] is non empty set
[:[:W,W:],W:] is Relation-like non empty set
bool [:[:W,W:],W:] is non empty set
u1 is Relation-like Function-like V18([:W,W:],W) Element of bool [:[:W,W:],W:]
B is Element of W
z is Relation-like Function-like V18([:W, the carrier of R:],W) Element of bool [:[:W, the carrier of R:],W:]
RightModStr(# W,u1,B,z #) is non empty strict RightModStr over R
the carrier of RightModStr(# W,u1,B,z #) is non empty set
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W + W is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) is Relation-like Function-like V18([: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #)) Element of bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):]
[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is non empty set
the addF of RightModStr(# W,u1,B,z #) . (W,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,W] is set
c₁₆ is right_complementable Element of the carrier of V
w is right_complementable Element of the carrier of V
c₁₆ + w is right_complementable Element of the carrier of V
the addF of V . (c₁₆,w) is right_complementable Element of the carrier of V
[c₁₆,w] is set
{c₁₆,w} is non empty set
{c₁₆} is non empty set
{{c₁₆,w},{c₁₆}} is non empty set
the addF of V . [c₁₆,w] is set
[W,W] is Element of [: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):]
u1 . [W,W] is set
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W + W is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) is Relation-like Function-like V18([: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #)) Element of bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):]
[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is non empty set
the addF of RightModStr(# W,u1,B,z #) . (W,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,W] is set
W + W is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . (W,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,W] is set
w is right_complementable Element of the carrier of V
c₁₆ is right_complementable Element of the carrier of V
w + c₁₆ is right_complementable Element of the carrier of V
the addF of V . (w,c₁₆) is right_complementable Element of the carrier of V
[w,c₁₆] is set
{w,c₁₆} is non empty set
{w} is non empty set
{{w,c₁₆},{w}} is non empty set
the addF of V . [w,c₁₆] is set
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W is Element of the carrier of RightModStr(# W,u1,B,z #)
c₁₆ is Element of the carrier of RightModStr(# W,u1,B,z #)
W + c₁₆ is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) is Relation-like Function-like V18([: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #)) Element of bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):]
[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is non empty set
the addF of RightModStr(# W,u1,B,z #) . (W,c₁₆) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,c₁₆] is set
{W,c₁₆} is non empty set
{W} is non empty set
{{W,c₁₆},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,c₁₆] is set
x is right_complementable Element of the carrier of V
y is right_complementable Element of the carrier of V
x + y is right_complementable Element of the carrier of V
the addF of V . (x,y) is right_complementable Element of the carrier of V
[x,y] is set
{x,y} is non empty set
{x} is non empty set
{{x,y},{x}} is non empty set
the addF of V . [x,y] is set
W + W is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . (W,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,W] is set
w is right_complementable Element of the carrier of V
w + x is right_complementable Element of the carrier of V
the addF of V . (w,x) is right_complementable Element of the carrier of V
[w,x] is set
{w,x} is non empty set
{w} is non empty set
{{w,x},{w}} is non empty set
the addF of V . [w,x] is set
(W + W) + c₁₆ is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . ((W + W),c₁₆) is Element of the carrier of RightModStr(# W,u1,B,z #)
[(W + W),c₁₆] is set
{(W + W),c₁₆} is non empty set
{(W + W)} is non empty set
{{(W + W),c₁₆},{(W + W)}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [(W + W),c₁₆] is set
(w + x) + y is right_complementable Element of the carrier of V
the addF of V . ((w + x),y) is right_complementable Element of the carrier of V
[(w + x),y] is set
{(w + x),y} is non empty set
{(w + x)} is non empty set
{{(w + x),y},{(w + x)}} is non empty set
the addF of V . [(w + x),y] is set
w + (x + y) is right_complementable Element of the carrier of V
the addF of V . (w,(x + y)) is right_complementable Element of the carrier of V
[w,(x + y)] is set
{w,(x + y)} is non empty set
{{w,(x + y)},{w}} is non empty set
the addF of V . [w,(x + y)] is set
W + (W + c₁₆) is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . (W,(W + c₁₆)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,(W + c₁₆)] is set
{W,(W + c₁₆)} is non empty set
{{W,(W + c₁₆)},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,(W + c₁₆)] is set
W is Element of the carrier of RightModStr(# W,u1,B,z #)
0. RightModStr(# W,u1,B,z #) is V49( RightModStr(# W,u1,B,z #)) Element of the carrier of RightModStr(# W,u1,B,z #)
the ZeroF of RightModStr(# W,u1,B,z #) is Element of the carrier of RightModStr(# W,u1,B,z #)
W + (0. RightModStr(# W,u1,B,z #)) is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . (W,(0. RightModStr(# W,u1,B,z #))) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,(0. RightModStr(# W,u1,B,z #))] is set
{W,(0. RightModStr(# W,u1,B,z #))} is non empty set
{W} is non empty set
{{W,(0. RightModStr(# W,u1,B,z #))},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,(0. RightModStr(# W,u1,B,z #))] is set
W is right_complementable Element of the carrier of V
W + (0. V) is right_complementable Element of the carrier of V
the addF of V . (W,(0. V)) is right_complementable Element of the carrier of V
[W,(0. V)] is set
{W,(0. V)} is non empty set
{W} is non empty set
{{W,(0. V)},{W}} is non empty set
the addF of V . [W,(0. V)] is set
W is Element of the carrier of RightModStr(# W,u1,B,z #)
W is right_complementable Element of the carrier of V
(comp V) . W is right_complementable Element of the carrier of V
x is Relation-like Function-like V18(W,W) Element of bool [:W,W:]
x . W is set
((comp V) | W) . W is set
w is Element of the carrier of RightModStr(# W,u1,B,z #)
W + w is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . (W,w) is Element of the carrier of RightModStr(# W,u1,B,z #)
[W,w] is set
{W,w} is non empty set
{W} is non empty set
{{W,w},{W}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [W,w] is set
c₁₆ is right_complementable Element of the carrier of V
W + c₁₆ is right_complementable Element of the carrier of V
the addF of V . (W,c₁₆) is right_complementable Element of the carrier of V
[W,c₁₆] is set
{W,c₁₆} is non empty set
{W} is non empty set
{{W,c₁₆},{W}} is non empty set
the addF of V . [W,c₁₆] is set
- W is right_complementable Element of the carrier of V
W + (- W) is right_complementable Element of the carrier of V
the addF of V . (W,(- W)) is right_complementable Element of the carrier of V
[W,(- W)] is set
{W,(- W)} is non empty set
{{W,(- W)},{W}} is non empty set
the addF of V . [W,(- W)] is set
W is right_complementable Element of the carrier of R
W is right_complementable Element of the carrier of R
W + W is right_complementable Element of the carrier of R
the addF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is Relation-like non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (W,W) is right_complementable Element of the carrier of R
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the addF of R . [W,W] is set
W * W is right_complementable Element of the carrier of R
the multF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (W,W) is right_complementable Element of the carrier of R
[W,W] is set
{W,W} is non empty set
{W} is non empty set
{{W,W},{W}} is non empty set
the multF of R . [W,W] is set
1_ R is right_complementable Element of the carrier of R
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
c₁₆ is Element of the carrier of RightModStr(# W,u1,B,z #)
w is Element of the carrier of RightModStr(# W,u1,B,z #)
c₁₆ + w is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) is Relation-like Function-like V18([: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #)) Element of bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):]
[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of RightModStr(# W,u1,B,z #):], the carrier of RightModStr(# W,u1,B,z #):] is non empty set
the addF of RightModStr(# W,u1,B,z #) . (c₁₆,w) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,w] is set
{c₁₆,w} is non empty set
{c₁₆} is non empty set
{{c₁₆,w},{c₁₆}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [c₁₆,w] is set
(c₁₆ + w) * W is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) is Relation-like Function-like V18([: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:], the carrier of RightModStr(# W,u1,B,z #)) Element of bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:], the carrier of RightModStr(# W,u1,B,z #):]
[: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:] is Relation-like non empty set
[:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:], the carrier of RightModStr(# W,u1,B,z #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:], the carrier of RightModStr(# W,u1,B,z #):] is non empty set
the rmult of RightModStr(# W,u1,B,z #) . ((c₁₆ + w),W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[(c₁₆ + w),W] is set
{(c₁₆ + w),W} is non empty set
{(c₁₆ + w)} is non empty set
{{(c₁₆ + w),W},{(c₁₆ + w)}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [(c₁₆ + w),W] is set
c₁₆ * W is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,W] is set
{c₁₆,W} is non empty set
{{c₁₆,W},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,W] is set
w * W is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (w,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[w,W] is set
{w,W} is non empty set
{w} is non empty set
{{w,W},{w}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [w,W] is set
(c₁₆ * W) + (w * W) is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . ((c₁₆ * W),(w * W)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[(c₁₆ * W),(w * W)] is set
{(c₁₆ * W),(w * W)} is non empty set
{(c₁₆ * W)} is non empty set
{{(c₁₆ * W),(w * W)},{(c₁₆ * W)}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [(c₁₆ * W),(w * W)] is set
c₁₆ * (W + W) is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,(W + W)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,(W + W)] is set
{c₁₆,(W + W)} is non empty set
{{c₁₆,(W + W)},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,(W + W)] is set
c₁₆ * W is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,W] is set
{c₁₆,W} is non empty set
{{c₁₆,W},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,W] is set
(c₁₆ * W) + (c₁₆ * W) is Element of the carrier of RightModStr(# W,u1,B,z #)
the addF of RightModStr(# W,u1,B,z #) . ((c₁₆ * W),(c₁₆ * W)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[(c₁₆ * W),(c₁₆ * W)] is set
{(c₁₆ * W),(c₁₆ * W)} is non empty set
{{(c₁₆ * W),(c₁₆ * W)},{(c₁₆ * W)}} is non empty set
the addF of RightModStr(# W,u1,B,z #) . [(c₁₆ * W),(c₁₆ * W)] is set
c₁₆ * (W * W) is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,(W * W)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,(W * W)] is set
{c₁₆,(W * W)} is non empty set
{{c₁₆,(W * W)},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,(W * W)] is set
(c₁₆ * W) * W is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . ((c₁₆ * W),W) is Element of the carrier of RightModStr(# W,u1,B,z #)
[(c₁₆ * W),W] is set
{(c₁₆ * W),W} is non empty set
{(c₁₆ * W)} is non empty set
{{(c₁₆ * W),W},{(c₁₆ * W)}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [(c₁₆ * W),W] is set
c₁₆ * (1_ R) is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,(1_ R)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,(1_ R)] is set
{c₁₆,(1_ R)} is non empty set
{{c₁₆,(1_ R)},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,(1_ R)] is set
y is right_complementable Element of the carrier of V
x is Element of the carrier of RightModStr(# W,u1,B,z #)
a is right_complementable Element of the carrier of R
[x,a] is Element of [: the carrier of RightModStr(# W,u1,B,z #), the carrier of R:]
{x,a} is non empty set
{x} is non empty set
{{x,a},{x}} is non empty set
dom z is set
x * a is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (x,a) is Element of the carrier of RightModStr(# W,u1,B,z #)
[x,a] is set
the rmult of RightModStr(# W,u1,B,z #) . [x,a] is set
y * a is right_complementable Element of the carrier of V
the rmult of V . (y,a) is right_complementable Element of the carrier of V
[y,a] is set
{y,a} is non empty set
{y} is non empty set
{{y,a},{y}} is non empty set
the rmult of V . [y,a] is set
x is right_complementable Element of the carrier of V
x * W is right_complementable Element of the carrier of V
the rmult of V . (x,W) is right_complementable Element of the carrier of V
[x,W] is set
{x,W} is non empty set
{x} is non empty set
{{x,W},{x}} is non empty set
the rmult of V . [x,W] is set
y is right_complementable Element of the carrier of V
y * W is right_complementable Element of the carrier of V
the rmult of V . (y,W) is right_complementable Element of the carrier of V
[y,W] is set
{y,W} is non empty set
{y} is non empty set
{{y,W},{y}} is non empty set
the rmult of V . [y,W] is set
x + y is right_complementable Element of the carrier of V
the addF of V . (x,y) is right_complementable Element of the carrier of V
[x,y] is set
{x,y} is non empty set
{{x,y},{x}} is non empty set
the addF of V . [x,y] is set
(x + y) * W is right_complementable Element of the carrier of V
the rmult of V . ((x + y),W) is right_complementable Element of the carrier of V
[(x + y),W] is set
{(x + y),W} is non empty set
{(x + y)} is non empty set
{{(x + y),W},{(x + y)}} is non empty set
the rmult of V . [(x + y),W] is set
(x * W) + (y * W) is right_complementable Element of the carrier of V
the addF of V . ((x * W),(y * W)) is right_complementable Element of the carrier of V
[(x * W),(y * W)] is set
{(x * W),(y * W)} is non empty set
{(x * W)} is non empty set
{{(x * W),(y * W)},{(x * W)}} is non empty set
the addF of V . [(x * W),(y * W)] is set
x * W is right_complementable Element of the carrier of V
the rmult of V . (x,W) is right_complementable Element of the carrier of V
[x,W] is set
{x,W} is non empty set
{{x,W},{x}} is non empty set
the rmult of V . [x,W] is set
W + W is right_complementable Element of the carrier of R
c₁₆ * (W + W) is Element of the carrier of RightModStr(# W,u1,B,z #)
the rmult of RightModStr(# W,u1,B,z #) . (c₁₆,(W + W)) is Element of the carrier of RightModStr(# W,u1,B,z #)
[c₁₆,(W + W)] is set
{c₁₆,(W + W)} is non empty set
{{c₁₆,(W + W)},{c₁₆}} is non empty set
the rmult of RightModStr(# W,u1,B,z #) . [c₁₆,(W + W)] is set
x * (W + W) is right_complementable Element of the carrier of V
the rmult of V . (x,(W + W)) is right_complementable Element of the carrier of V
[x,(W + W)] is set
{x,(W + W)} is non empty set
{{x,(W + W)},{x}} is non empty set
the rmult of V . [x,(W + W)] is set
(x * W) + (x * W) is right_complementable Element of the carrier of V
the addF of V . ((x * W),(x * W)) is right_complementable Element of the carrier of V
[(x * W),(x * W)] is set
{(x * W),(x * W)} is non empty set
{{(x * W),(x * W)},{(x * W)}} is non empty set
the addF of V . [(x * W),(x * W)] is set
x * (W * W) is right_complementable Element of the carrier of V
the rmult of V . (x,(W * W)) is right_complementable Element of the carrier of V
[x,(W * W)] is set
{x,(W * W)} is non empty set
{{x,(W * W)},{x}} is non empty set
the rmult of V . [x,(W * W)] is set
(x * W) * W is right_complementable Element of the carrier of V
the rmult of V . ((x * W),W) is right_complementable Element of the carrier of V
[(x * W),W] is set
{(x * W),W} is non empty set
{(x * W)} is non empty set
{{(x * W),W},{(x * W)}} is non empty set
the rmult of V . [(x * W),W] is set
x * (1_ R) is right_complementable Element of the carrier of V
the rmult of V . (x,(1_ R)) is right_complementable Element of the carrier of V
[x,(1_ R)] is set
{x,(1_ R)} is non empty set
{{x,(1_ R)},{x}} is non empty set
the rmult of V . [x,(1_ R)] is set
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of W is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of u is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
the carrier of W is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
the ZeroF of V is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty set
W is right_complementable Element of the carrier of R
B is right_complementable Element of the carrier of R
W + B is right_complementable Element of the carrier of R
the addF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
[: the carrier of R, the carrier of R:] is Relation-like non empty set
[:[: the carrier of R, the carrier of R:], the carrier of R:] is Relation-like non empty set
bool [:[: the carrier of R, the carrier of R:], the carrier of R:] is non empty set
the addF of R . (W,B) is right_complementable Element of the carrier of R
[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 R . [W,B] is set
B * W is right_complementable Element of the carrier of R
the multF of R is Relation-like Function-like V18([: the carrier of R, the carrier of R:], the carrier of R) Element of bool [:[: the carrier of R, the carrier of R:], the carrier of R:]
the multF of R . (B,W) is right_complementable Element of the carrier of R
[B,W] is set
{B,W} is non empty set
{B} is non empty set
{{B,W},{B}} is non empty set
the multF of R . [B,W] is set
1_ R is right_complementable Element of the carrier of R
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
C + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,C] is set
(C + C) * W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . ((C + C),W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[(C + C),W] is set
{(C + C),W} is non empty set
{(C + C)} is non empty set
{{(C + C),W},{(C + C)}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [(C + C),W] is set
C * W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,W] is set
{C,W} is non empty set
{{C,W},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,W] is set
C * W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,W] is set
{C,W} is non empty set
{C} is non empty set
{{C,W},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,W] is set
(C * W) + (C * W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . ((C * W),(C * W)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[(C * W),(C * W)] is set
{(C * W),(C * W)} is non empty set
{(C * W)} is non empty set
{{(C * W),(C * W)},{(C * W)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [(C * W),(C * W)] is set
C * (W + B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,(W + B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,(W + B)] is set
{C,(W + B)} is non empty set
{{C,(W + B)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,(W + B)] is set
C * B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,B] is set
{C,B} is non empty set
{{C,B},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,B] is set
(C * W) + (C * B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . ((C * W),(C * B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[(C * W),(C * B)] is set
{(C * W),(C * B)} is non empty set
{{(C * W),(C * B)},{(C * W)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [(C * W),(C * B)] is set
C * (B * W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,(B * W)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,(B * W)] is set
{C,(B * W)} is non empty set
{{C,(B * W)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,(B * W)] is set
(C * B) * W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . ((C * B),W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[(C * B),W] is set
{(C * B),W} is non empty set
{(C * B)} is non empty set
{{(C * B),W},{(C * B)}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [(C * B),W] is set
C * (1_ R) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,(1_ R)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,(1_ R)] is set
{C,(1_ R)} is non empty set
{{C,(1_ R)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,(1_ R)] is set
c₈ is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c₈ + x is right_complementable Element of the carrier of V
the addF of V . (c₈,x) is right_complementable Element of the carrier of V
[c₈,x] is set
{c₈,x} is non empty set
{c₈} is non empty set
{{c₈,x},{c₈}} is non empty set
the addF of V . [c₈,x] is set
(c₈ + x) * W is right_complementable Element of the carrier of V
the rmult of V . ((c₈ + x),W) is right_complementable Element of the carrier of V
[(c₈ + x),W] is set
{(c₈ + x),W} is non empty set
{(c₈ + x)} is non empty set
{{(c₈ + x),W},{(c₈ + x)}} is non empty set
the rmult of V . [(c₈ + x),W] is set
c₈ * W is right_complementable Element of the carrier of V
the rmult of V . (c₈,W) is right_complementable Element of the carrier of V
[c₈,W] is set
{c₈,W} is non empty set
{{c₈,W},{c₈}} is non empty set
the rmult of V . [c₈,W] is set
x * W is right_complementable Element of the carrier of V
the rmult of V . (x,W) is right_complementable Element of the carrier of V
[x,W] is set
{x,W} is non empty set
{x} is non empty set
{{x,W},{x}} is non empty set
the rmult of V . [x,W] is set
(c₈ * W) + (x * W) is right_complementable Element of the carrier of V
the addF of V . ((c₈ * W),(x * W)) is right_complementable Element of the carrier of V
[(c₈ * W),(x * W)] is set
{(c₈ * W),(x * W)} is non empty set
{(c₈ * W)} is non empty set
{{(c₈ * W),(x * W)},{(c₈ * W)}} is non empty set
the addF of V . [(c₈ * W),(x * W)] is set
W + B is right_complementable Element of the carrier of R
C * (W + B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (C,(W + B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[C,(W + B)] is set
{C,(W + B)} is non empty set
{{C,(W + B)},{C}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [C,(W + B)] is set
c₈ * (W + B) is right_complementable Element of the carrier of V
the rmult of V . (c₈,(W + B)) is right_complementable Element of the carrier of V
[c₈,(W + B)] is set
{c₈,(W + B)} is non empty set
{{c₈,(W + B)},{c₈}} is non empty set
the rmult of V . [c₈,(W + B)] is set
c₈ * B is right_complementable Element of the carrier of V
the rmult of V . (c₈,B) is right_complementable Element of the carrier of V
[c₈,B] is set
{c₈,B} is non empty set
{{c₈,B},{c₈}} is non empty set
the rmult of V . [c₈,B] is set
(c₈ * W) + (c₈ * B) is right_complementable Element of the carrier of V
the addF of V . ((c₈ * W),(c₈ * B)) is right_complementable Element of the carrier of V
[(c₈ * W),(c₈ * B)] is set
{(c₈ * W),(c₈ * B)} is non empty set
{{(c₈ * W),(c₈ * B)},{(c₈ * W)}} is non empty set
the addF of V . [(c₈ * W),(c₈ * B)] is set
c₈ * (B * W) is right_complementable Element of the carrier of V
the rmult of V . (c₈,(B * W)) is right_complementable Element of the carrier of V
[c₈,(B * W)] is set
{c₈,(B * W)} is non empty set
{{c₈,(B * W)},{c₈}} is non empty set
the rmult of V . [c₈,(B * W)] is set
(c₈ * B) * W is right_complementable Element of the carrier of V
the rmult of V . ((c₈ * B),W) is right_complementable Element of the carrier of V
[(c₈ * B),W] is set
{(c₈ * B),W} is non empty set
{(c₈ * B)} is non empty set
{{(c₈ * B),W},{(c₈ * B)}} is non empty set
the rmult of V . [(c₈ * B),W] is set
c₈ * (1_ R) is right_complementable Element of the carrier of V
the rmult of V . (c₈,(1_ R)) is right_complementable Element of the carrier of V
[c₈,(1_ R)] is set
{c₈,(1_ R)} is non empty set
{{c₈,(1_ R)},{c₈}} is non empty set
the rmult of V . [c₈,(1_ R)] is set
the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty set
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
C is right_complementable Element of the carrier of V
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
c₈ is right_complementable Element of the carrier of V
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [B,C] is set
C + c₈ is right_complementable Element of the carrier of V
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
W is right_complementable Element of the carrier of R
B * W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of R:], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (B,W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[B,W] is set
{B,W} is non empty set
{{B,W},{B}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [B,W] is set
C * W is right_complementable Element of the carrier of V
the rmult of V . (C,W) is right_complementable Element of the carrier of V
[C,W] is set
{C,W} is non empty set
{{C,W},{C}} is non empty set
the rmult of V . [C,W] is set
W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
W + B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (W,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [W,B] is set
B + W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (B,W) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[B,W] is set
{B,W} is non empty set
{B} is non empty set
{{B,W},{B}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [B,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 . (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
W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
W + B is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Relation-like Function-like V18([: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):]
[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
[:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is Relation-like non empty set
bool [:[: the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #), the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):], the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #):] is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (W,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [W,B] is set
(W + B) + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . ((W + B),C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[(W + B),C] is set
{(W + B),C} is non empty set
{(W + B)} is non empty set
{{(W + B),C},{(W + B)}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [(W + B),C] 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 . (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
x is right_complementable Element of the carrier of V
(C + c₈) + x is right_complementable Element of the carrier of V
the addF of V . ((C + c₈),x) is right_complementable Element of the carrier of V
[(C + c₈),x] is set
{(C + c₈),x} is non empty set
{(C + c₈)} is non empty set
{{(C + c₈),x},{(C + c₈)}} is non empty set
the addF of V . [(C + c₈),x] is set
c₈ + x is right_complementable Element of the carrier of V
the addF of V . (c₈,x) is right_complementable Element of the carrier of V
[c₈,x] is set
{c₈,x} is non empty set
{c₈} is non empty set
{{c₈,x},{c₈}} is non empty set
the addF of V . [c₈,x] is set
C + (c₈ + x) is right_complementable Element of the carrier of V
the addF of V . (C,(c₈ + x)) is right_complementable Element of the carrier of V
[C,(c₈ + x)] is set
{C,(c₈ + x)} is non empty set
{{C,(c₈ + x)},{C}} is non empty set
the addF of V . [C,(c₈ + x)] is set
B + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (B,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [B,C] is set
W + (B + C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (W,(B + C)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[W,(B + C)] is set
{W,(B + C)} is non empty set
{{W,(B + C)},{W}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [W,(B + C)] is set
W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is V49( RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the ZeroF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
W + (0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (W,(0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #))) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[W,(0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #))] is set
{W,(0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #))} is non empty set
{W} is non empty set
{{W,(0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #))},{W}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [W,(0. RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #))] is set
B is right_complementable Element of the carrier of V
0. V is V49(V) right_complementable Element of the carrier of V
B + (0. V) is right_complementable Element of the carrier of V
the addF of V . (B,(0. V)) is right_complementable Element of the carrier of V
[B,(0. V)] is set
{B,(0. V)} is non empty set
{B} is non empty set
{{B,(0. V)},{B}} is non empty set
the addF of V . [B,(0. V)] is set
W is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult 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 . (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
C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
W + C is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . (W,C) is Element of the carrier of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #)
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) . [W,C] is set
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the rmult of W is Relation-like Function-like V18([: the carrier of W, the carrier of R:], the carrier of W) Element of bool [:[: the carrier of W, the carrier of R:], the carrier of W:]
the carrier of W is non empty set
[: the carrier of W, the carrier of R:] is Relation-like non empty set
[:[: the carrier of W, the carrier of R:], the carrier of W:] is Relation-like non empty set
bool [:[: the carrier of W, the carrier of R:], the carrier of W:] is non empty set
the rmult of V | [: the carrier of W, the carrier of R:] is Relation-like Function-like set
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
0. V is V49(V) right_complementable Element of the carrier of V
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, the carrier of W:] is Relation-like Function-like set
R is set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over V
(V,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (V,u)
0. u is V49(u) right_complementable Element of the carrier of u
the carrier of u is non empty set
the ZeroF of u is right_complementable Element of the carrier of u
the carrier of (V,u) is non empty set
{(0. u)} is non empty Element of bool the carrier of u
bool the carrier of u is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,u)
the carrier of (R,u) is non empty set
the carrier of u is non empty 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. u)} is non empty Element of bool the carrier of u
bool the carrier of u is non empty set
the carrier of (R,V) is non empty set
the carrier of V is non empty set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
{(0. V)} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,u)
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,W) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,W)
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,u)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,u)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,u) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,u)
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,W) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,W)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like RightModStr over R
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,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
the ZeroF of V is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
bool the carrier of V is non empty set
C is set
C is set
C is Element of bool the carrier of V
c₈ is set
x is right_complementable Element of the carrier of V
u + 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 . (u,x) is right_complementable Element of the carrier of V
[u,x] is set
{u,x} is non empty set
{u} is non empty set
{{u,x},{u}} is non empty set
the addF of V . [u,x] is set
c₈ is set
x is right_complementable Element of the carrier of V
u + 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 . (u,x) is right_complementable Element of the carrier of V
[u,x] is set
{u,x} is non empty set
{u} is non empty set
{{u,x},{u}} is non empty set
the addF of V . [u,x] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,(0. V),u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ ((0. V) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
the carrier of u is non empty set
B is set
C is right_complementable Element of the carrier of V
(0. V) + 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 . ((0. V),C) is right_complementable Element of the carrier of V
[(0. V),C] is set
{(0. V),C} is non empty set
{(0. V)} is non empty set
{{(0. V),C},{(0. V)}} is non empty set
the addF of V . [(0. V),C] is set
B is set
C is right_complementable Element of the carrier of V
(0. V) + 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 . ((0. V),C) is right_complementable Element of the carrier of V
[(0. V),C] is set
{(0. V),C} is non empty set
{(0. V)} is non empty set
{{(0. V),C},{(0. V)}} is non empty set
the addF of V . [(0. V),C] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
bool the carrier of V is non empty set
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
W is Element of bool the carrier of V
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
(R,V,(0. V),u) is Element of bool the carrier of V
{ ((0. V) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
R is set
V is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over V
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (V,u)
(V,u,W,B) is Element of bool the carrier of u
bool the carrier of u is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of u : b₁ in B } is set
C is right_complementable Element of the carrier of u
W + C is right_complementable Element of the carrier of u
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 . (W,C) is right_complementable Element of the carrier of u
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of u . [W,C] is set
C is right_complementable Element of the carrier of u
W + C is right_complementable Element of the carrier of u
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 . (W,C) is right_complementable Element of the carrier of u
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of u . [W,C] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
B is right_complementable Element of the carrier of V
u + 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) is right_complementable Element of the carrier of V
[u,B] is set
{u,B} is non empty set
{u} is non empty set
{{u,B},{u}} is non empty set
the addF of V . [u,B] is set
- B is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
u + (- u) 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,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{u} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is 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 + (0. 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 . (u,(0. V)) is right_complementable Element of the carrier of V
[u,(0. V)] is set
{u,(0. V)} is non empty set
{u} is non empty set
{{u,(0. V)},{u}} is non empty set
the addF of V . [u,(0. V)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,(0. V),u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ ((0. V) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
the carrier of u is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
u is right_complementable Element of the carrier of V
(R,V,u,(R,V)) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
{u} is non empty Element of bool the carrier of V
W is set
B is right_complementable Element of the carrier of V
u + 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) is right_complementable Element of the carrier of V
[u,B] is set
{u,B} is non empty set
{u} is non empty set
{{u,B},{u}} is non empty set
the addF of V . [u,B] is set
the carrier of (R,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
W is 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 + (0. 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 . (u,(0. V)) is right_complementable Element of the carrier of V
[u,(0. V)] is set
{u,(0. V)} is non empty set
{u} is non empty set
{{u,(0. V)},{u}} is non empty set
the addF of V . [u,(0. V)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
the carrier of W 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 + (0. 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 . (u,(0. V)) is right_complementable Element of the carrier of V
[u,(0. V)] is set
{u,(0. V)} is non empty set
{u} is non empty set
{{u,(0. V)},{u}} is non empty set
the addF of V . [u,(0. V)] is set
B is set
C is right_complementable Element of the carrier of V
u + C is right_complementable Element of the carrier of V
the addF of V . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
B is set
C is right_complementable Element of the carrier of W
C is right_complementable Element of the carrier of W
C - C is right_complementable Element of the carrier of W
- C is right_complementable Element of the carrier of W
C + (- C) is right_complementable Element of the carrier of W
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 . (C,(- C)) is right_complementable Element of the carrier of W
[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 W . [C,(- C)] is set
C + (C - C) is right_complementable Element of the carrier of W
the addF of W . (C,(C - C)) is right_complementable Element of the carrier of W
[C,(C - C)] is set
{C,(C - C)} is non empty set
{C} is non empty set
{{C,(C - C)},{C}} is non empty set
the addF of W . [C,(C - C)] is set
C + (- C) is right_complementable Element of the carrier of W
the addF of W . (C,(- C)) is right_complementable Element of the carrier of W
[C,(- C)] is set
{C,(- C)} is non empty set
{{C,(- C)},{C}} is non empty set
the addF of W . [C,(- C)] is set
C + (C + (- C)) is right_complementable Element of the carrier of W
the addF of W . (C,(C + (- C))) is right_complementable Element of the carrier of W
[C,(C + (- C))] is set
{C,(C + (- C))} is non empty set
{{C,(C + (- C))},{C}} is non empty set
the addF of W . [C,(C + (- C))] is set
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
C + (0. W) is right_complementable Element of the carrier of W
the addF of W . (C,(0. W)) is right_complementable Element of the carrier of W
[C,(0. W)] is set
{C,(0. W)} is non empty set
{{C,(0. W)},{C}} is non empty set
the addF of W . [C,(0. W)] is set
c₈ is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
c₈ - x is right_complementable Element of the carrier of V
- x is right_complementable Element of the carrier of V
c₈ + (- x) is right_complementable Element of the carrier of V
the addF of V . (c₈,(- x)) is right_complementable Element of the carrier of V
[c₈,(- x)] is set
{c₈,(- x)} is non empty set
{c₈} is non empty set
{{c₈,(- x)},{c₈}} is non empty set
the addF of V . [c₈,(- x)] is set
x + (c₈ - x) is right_complementable Element of the carrier of V
the addF of V . (x,(c₈ - x)) is right_complementable Element of the carrier of V
[x,(c₈ - x)] is set
{x,(c₈ - x)} is non empty set
{x} is non empty set
{{x,(c₈ - x)},{x}} is non empty set
the addF of V . [x,(c₈ - x)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,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 ZeroF of V is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
u is right_complementable Element of the carrier of V
(R,V,u,(R,V)) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
the carrier of W is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
B is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
C is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over B
the carrier of C is non empty set
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
u is right_complementable Element of the carrier of V
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
the carrier of W is non empty set
C is right_complementable Element of the carrier of C
c₈ is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (B,C)
(B,C,C,c₈) is Element of bool the carrier of C
bool the carrier of C is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of C : b₁ in c₈ } is set
the carrier of c₈ is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
V is right_complementable Element of the carrier of R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
W * V is right_complementable Element of the carrier of u
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of u . (W,V) is right_complementable Element of the carrier of u
[W,V] is set
{W,V} is non empty set
{W} is non empty set
{{W,V},{W}} is non empty set
the rmult of u . [W,V] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,u)
(R,u,(W * V),B) is Element of bool the carrier of u
bool the carrier of u is non empty set
{ ((W * V) + b₁) where b₁ is right_complementable Element of the carrier of u : b₁ in B } is set
the carrier of B is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
W + u 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,u) is right_complementable Element of the carrier of V
[W,u] is set
{W,u} is non empty set
{W} is non empty set
{{W,u},{W}} is non empty set
the addF of V . [W,u] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,(W + u),B) is Element of bool the carrier of V
{ ((W + u) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is set
C is right_complementable Element of the carrier of V
W + C is right_complementable Element of the carrier of V
the addF of V . (W,C) is right_complementable Element of the carrier of V
[W,C] is set
{W,C} is non empty set
{{W,C},{W}} is non empty set
the addF of V . [W,C] is set
C - u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
C + (- u) is right_complementable Element of the carrier of V
the addF of V . (C,(- u)) is right_complementable Element of the carrier of V
[C,(- u)] is set
{C,(- u)} is non empty set
{C} is non empty set
{{C,(- u)},{C}} is non empty set
the addF of V . [C,(- u)] is set
(W + u) + (C - u) is right_complementable Element of the carrier of V
the addF of V . ((W + u),(C - u)) is right_complementable Element of the carrier of V
[(W + u),(C - u)] is set
{(W + u),(C - u)} is non empty set
{(W + u)} is non empty set
{{(W + u),(C - u)},{(W + u)}} is non empty set
the addF of V . [(W + u),(C - u)] is set
u + (C - u) is right_complementable Element of the carrier of V
the addF of V . (u,(C - u)) is right_complementable Element of the carrier of V
[u,(C - u)] is set
{u,(C - u)} is non empty set
{u} is non empty set
{{u,(C - u)},{u}} is non empty set
the addF of V . [u,(C - u)] is set
W + (u + (C - u)) is right_complementable Element of the carrier of V
the addF of V . (W,(u + (C - u))) is right_complementable Element of the carrier of V
[W,(u + (C - u))] is set
{W,(u + (C - u))} is non empty set
{{W,(u + (C - u))},{W}} is non empty set
the addF of V . [W,(u + (C - u))] is set
C + u is right_complementable Element of the carrier of V
the addF of V . (C,u) is right_complementable Element of the carrier of V
[C,u] is set
{C,u} is non empty set
{{C,u},{C}} is non empty set
the addF of V . [C,u] is set
(C + u) - u is right_complementable Element of the carrier of V
(C + u) + (- u) is right_complementable Element of the carrier of V
the addF of V . ((C + u),(- u)) is right_complementable Element of the carrier of V
[(C + u),(- u)] is set
{(C + u),(- u)} is non empty set
{(C + u)} is non empty set
{{(C + u),(- u)},{(C + u)}} is non empty set
the addF of V . [(C + u),(- u)] is set
W + ((C + u) - u) is right_complementable Element of the carrier of V
the addF of V . (W,((C + u) - u)) is right_complementable Element of the carrier of V
[W,((C + u) - u)] is set
{W,((C + u) - u)} is non empty set
{{W,((C + u) - u)},{W}} is non empty set
the addF of V . [W,((C + u) - u)] is set
u - u is right_complementable Element of the carrier of V
u + (- u) is right_complementable Element of the carrier of V
the addF of V . (u,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
C + (u - u) is right_complementable Element of the carrier of V
the addF of V . (C,(u - u)) is right_complementable Element of the carrier of V
[C,(u - u)] is set
{C,(u - u)} is non empty set
{{C,(u - u)},{C}} is non empty set
the addF of V . [C,(u - u)] is set
W + (C + (u - u)) is right_complementable Element of the carrier of V
the addF of V . (W,(C + (u - u))) is right_complementable Element of the carrier of V
[W,(C + (u - u))] is set
{W,(C + (u - u))} is non empty set
{{W,(C + (u - u))},{W}} is non empty set
the addF of V . [W,(C + (u - u))] is 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
C + (0. V) is right_complementable Element of the carrier of V
the addF of V . (C,(0. V)) is right_complementable Element of the carrier of V
[C,(0. V)] is set
{C,(0. V)} is non empty set
{{C,(0. V)},{C}} is non empty set
the addF of V . [C,(0. V)] is set
W + (C + (0. V)) is right_complementable Element of the carrier of V
the addF of V . (W,(C + (0. V))) is right_complementable Element of the carrier of V
[W,(C + (0. V))] is set
{W,(C + (0. V))} is non empty set
{{W,(C + (0. V))},{W}} is non empty set
the addF of V . [W,(C + (0. V))] is set
C is set
C is right_complementable Element of the carrier of V
(W + u) + C is right_complementable Element of the carrier of V
the addF of V . ((W + u),C) is right_complementable Element of the carrier of V
[(W + u),C] is set
{(W + u),C} is non empty set
{(W + u)} is non empty set
{{(W + u),C},{(W + u)}} is non empty set
the addF of V . [(W + u),C] is set
u + C is right_complementable Element of the carrier of V
the addF of V . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
W + (u + C) is right_complementable Element of the carrier of V
the addF of V . (W,(u + C)) is right_complementable Element of the carrier of V
[W,(u + C)] is set
{W,(u + C)} is non empty set
{{W,(u + C)},{W}} is non empty set
the addF of V . [W,(u + C)] is 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
W + (0. V) is right_complementable Element of the carrier of V
the addF of V . (W,(0. V)) is right_complementable Element of the carrier of V
[W,(0. V)] is set
{W,(0. V)} is non empty set
{{W,(0. V)},{W}} is non empty set
the addF of V . [W,(0. V)] is set
C is right_complementable Element of the carrier of V
(W + u) + C is right_complementable Element of the carrier of V
the addF of V . ((W + u),C) is right_complementable Element of the carrier of V
[(W + u),C] is set
{(W + u),C} is non empty set
{(W + u)} is non empty set
{{(W + u),C},{(W + u)}} is non empty set
the addF of V . [(W + u),C] is set
u + C is right_complementable Element of the carrier of V
the addF of V . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
W + (u + C) is right_complementable Element of the carrier of V
the addF of V . (W,(u + C)) is right_complementable Element of the carrier of V
[W,(u + C)] is set
{W,(u + C)} is non empty set
{{W,(u + C)},{W}} is non empty set
the addF of V . [W,(u + C)] is set
- C is right_complementable Element of the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
W - u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
W + (- u) 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,(- u)) is right_complementable Element of the carrier of V
[W,(- u)] is set
{W,(- u)} is non empty set
{W} is non empty set
{{W,(- u)},{W}} is non empty set
the addF of V . [W,(- u)] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,(W - u),B) is Element of bool the carrier of V
{ ((W - u) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
- (- u) is right_complementable Element of the carrier of V
W + (- u) is right_complementable Element of the carrier of V
(R,V,(W + (- u)),B) is Element of bool the carrier of V
{ ((W + (- u)) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,u,B) is Element of bool the carrier of V
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
W + 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 . (W,C) is right_complementable Element of the carrier of V
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of V . [W,C] is set
C is set
c₈ is right_complementable Element of the carrier of V
W + c₈ is right_complementable Element of the carrier of V
the addF of V . (W,c₈) is right_complementable Element of the carrier of V
[W,c₈] is set
{W,c₈} is non empty set
{{W,c₈},{W}} is non empty set
the addF of V . [W,c₈] is set
u - C is right_complementable Element of the carrier of V
- C is right_complementable Element of the carrier of V
u + (- C) is right_complementable Element of the carrier of V
the addF of V . (u,(- C)) is right_complementable Element of the carrier of V
[u,(- C)] is set
{u,(- C)} is non empty set
{u} is non empty set
{{u,(- C)},{u}} is non empty set
the addF of V . [u,(- C)] is set
C - 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 . (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
W + (C - C) is right_complementable Element of the carrier of V
the addF of V . (W,(C - C)) is right_complementable Element of the carrier of V
[W,(C - C)] is set
{W,(C - C)} is non empty set
{{W,(C - C)},{W}} is non empty set
the addF of V . [W,(C - C)] is 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
W + (0. V) is right_complementable Element of the carrier of V
the addF of V . (W,(0. V)) is right_complementable Element of the carrier of V
[W,(0. V)] is set
{W,(0. V)} is non empty set
{{W,(0. V)},{W}} is non empty set
the addF of V . [W,(0. V)] is set
c₈ + (- C) is right_complementable Element of the carrier of V
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
u + (c₈ + (- C)) is right_complementable Element of the carrier of V
the addF of V . (u,(c₈ + (- C))) is right_complementable Element of the carrier of V
[u,(c₈ + (- C))] is set
{u,(c₈ + (- C))} is non empty set
{{u,(c₈ + (- C))},{u}} is non empty set
the addF of V . [u,(c₈ + (- C))] is set
c₈ - C is right_complementable Element of the carrier of V
c₈ + (- C) is right_complementable Element of the carrier of V
u + (c₈ - C) is right_complementable Element of the carrier of V
the addF of V . (u,(c₈ - C)) is right_complementable Element of the carrier of V
[u,(c₈ - C)] is set
{u,(c₈ - C)} is non empty set
{{u,(c₈ - C)},{u}} is non empty set
the addF of V . [u,(c₈ - C)] is set
C is set
c₈ is right_complementable Element of the carrier of V
u + c₈ is right_complementable Element of the carrier of V
the addF of V . (u,c₈) is right_complementable Element of the carrier of V
[u,c₈] is set
{u,c₈} is non empty set
{u} is non empty set
{{u,c₈},{u}} is non empty set
the addF of V . [u,c₈] is set
C + c₈ is right_complementable Element of the carrier of V
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
W + (C + c₈) is right_complementable Element of the carrier of V
the addF of V . (W,(C + c₈)) is right_complementable Element of the carrier of V
[W,(C + c₈)] is set
{W,(C + c₈)} is non empty set
{{W,(C + c₈)},{W}} is non empty set
the addF of V . [W,(C + c₈)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is right_complementable Element of the carrier of V
C is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,C) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
(R,V,B,C) is Element of bool the carrier of V
{ (B + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
(R,V,u,C) is Element of bool the carrier of V
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of R is non empty set
V is right_complementable Element of the carrier of R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of u is non empty set
W is right_complementable Element of the carrier of u
W * V is right_complementable Element of the carrier of u
the rmult of u is Relation-like Function-like V18([: the carrier of u, the carrier of R:], the carrier of u) Element of bool [:[: the carrier of u, the carrier of R:], the carrier of u:]
[: the carrier of u, the carrier of R:] is Relation-like non empty set
[:[: the carrier of u, the carrier of R:], the carrier of u:] is Relation-like non empty set
bool [:[: the carrier of u, the carrier of R:], the carrier of u:] is non empty set
the rmult of u . (W,V) is right_complementable Element of the carrier of u
[W,V] is set
{W,V} is non empty set
{W} is non empty set
{{W,V},{W}} is non empty set
the rmult of u . [W,V] is set
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,u)
(R,u,W,B) is Element of bool the carrier of u
bool the carrier of u is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of u : b₁ in B } is set
the carrier of B is non empty set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
1_ R is right_complementable Element of the carrier of R
the carrier of R is non empty set
K147(R) is right_complementable Element of the carrier of R
the OneF of R is right_complementable Element of the carrier of R
- (1_ R) is right_complementable Element of the carrier of R
u * (- (1_ R)) is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
the rmult of V . (u,(- (1_ R))) is right_complementable Element of the carrier of V
[u,(- (1_ R))] is set
{u,(- (1_ R))} is non empty set
{u} is non empty set
{{u,(- (1_ R))},{u}} is non empty set
the rmult of V . [u,(- (1_ R))] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
W + C is right_complementable Element of the carrier of V
the addF of V . (W,C) is right_complementable Element of the carrier of V
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of V . [W,C] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(- W) + u is right_complementable Element of the carrier of V
the addF of V . ((- W),u) is right_complementable Element of the carrier of V
[(- W),u] is set
{(- W),u} is non empty set
{(- W)} is non empty set
{{(- W),u},{(- W)}} is non empty set
the addF of V . [(- W),u] is set
- (- W) is right_complementable Element of the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,W,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
W + 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 . (W,C) is right_complementable Element of the carrier of V
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of V . [W,C] is set
- C is right_complementable Element of the carrier of V
C is right_complementable Element of the carrier of V
W - C is right_complementable Element of the carrier of V
- C is right_complementable Element of the carrier of V
W + (- C) is right_complementable Element of the carrier of V
the addF of V . (W,(- C)) is right_complementable Element of the carrier of V
[W,(- C)] is set
{W,(- C)} is non empty set
{{W,(- C)},{W}} is non empty set
the addF of V . [W,(- C)] is set
C is right_complementable Element of the carrier of V
W - C is right_complementable Element of the carrier of V
- C is right_complementable Element of the carrier of V
W + (- 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 . (W,(- C)) is right_complementable Element of the carrier of V
[W,(- C)] is set
{W,(- C)} is non empty set
{W} is non empty set
{{W,(- C)},{W}} is non empty set
the addF of V . [W,(- C)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
C is right_complementable Element of the carrier of V
(R,V,C,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
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 . (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₈ is right_complementable Element of the carrier of V
C + c₈ is right_complementable Element of the carrier of V
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,c₈},{C}} is non empty set
the addF of V . [C,c₈] is set
c₈ + C is right_complementable Element of the carrier of V
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 is right_complementable Element of the carrier of V
(- C) - 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 . ((- 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₈ + C) + ((- C) - C) is right_complementable Element of the carrier of V
the addF of V . ((c₈ + C),((- C) - C)) is right_complementable Element of the carrier of V
[(c₈ + C),((- C) - C)] is set
{(c₈ + C),((- C) - C)} is non empty set
{(c₈ + C)} is non empty set
{{(c₈ + C),((- C) - C)},{(c₈ + C)}} is non empty set
the addF of V . [(c₈ + C),((- C) - C)] is set
(c₈ + C) + (- C) is right_complementable Element of the carrier of V
the addF of V . ((c₈ + C),(- C)) is right_complementable Element of the carrier of V
[(c₈ + C),(- C)] is set
{(c₈ + C),(- C)} is non empty set
{{(c₈ + C),(- C)},{(c₈ + C)}} is non empty set
the addF of V . [(c₈ + C),(- C)] is set
((c₈ + C) + (- C)) - C is right_complementable Element of the carrier of V
((c₈ + C) + (- C)) + (- C) is right_complementable Element of the carrier of V
the addF of V . (((c₈ + C) + (- C)),(- C)) is right_complementable Element of the carrier of V
[((c₈ + C) + (- C)),(- C)] is set
{((c₈ + C) + (- C)),(- C)} is non empty set
{((c₈ + C) + (- C))} is non empty set
{{((c₈ + C) + (- C)),(- C)},{((c₈ + C) + (- C))}} is non empty set
the addF of V . [((c₈ + C) + (- C)),(- C)] is set
C + (- C) is right_complementable Element of the carrier of V
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,(- C)},{C}} is non empty set
the addF of V . [C,(- C)] is set
c₈ + (C + (- C)) is right_complementable Element of the carrier of V
the addF of V . (c₈,(C + (- C))) is right_complementable Element of the carrier of V
[c₈,(C + (- C))] is set
{c₈,(C + (- C))} is non empty set
{{c₈,(C + (- C))},{c₈}} is non empty set
the addF of V . [c₈,(C + (- C))] is set
(c₈ + (C + (- C))) - C is right_complementable Element of the carrier of V
(c₈ + (C + (- C))) + (- C) is right_complementable Element of the carrier of V
the addF of V . ((c₈ + (C + (- C))),(- C)) is right_complementable Element of the carrier of V
[(c₈ + (C + (- C))),(- C)] is set
{(c₈ + (C + (- C))),(- C)} is non empty set
{(c₈ + (C + (- C)))} is non empty set
{{(c₈ + (C + (- C))),(- C)},{(c₈ + (C + (- C)))}} is non empty set
the addF of V . [(c₈ + (C + (- C))),(- C)] is 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
c₈ + (0. V) is right_complementable Element of the carrier of V
the addF of V . (c₈,(0. V)) is right_complementable Element of the carrier of V
[c₈,(0. V)] is set
{c₈,(0. V)} is non empty set
{{c₈,(0. V)},{c₈}} is non empty set
the addF of V . [c₈,(0. V)] is set
(c₈ + (0. V)) - C is right_complementable Element of the carrier of V
(c₈ + (0. V)) + (- C) is right_complementable Element of the carrier of V
the addF of V . ((c₈ + (0. V)),(- C)) is right_complementable Element of the carrier of V
[(c₈ + (0. V)),(- C)] is set
{(c₈ + (0. V)),(- C)} is non empty set
{(c₈ + (0. V))} is non empty set
{{(c₈ + (0. V)),(- C)},{(c₈ + (0. V))}} is non empty set
the addF of V . [(c₈ + (0. V)),(- C)] is set
c₈ - 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 . (c₈,(- C)) is right_complementable Element of the carrier of V
[c₈,(- C)] is set
{c₈,(- C)} is non empty set
{{c₈,(- C)},{c₈}} is non empty set
the addF of V . [c₈,(- C)] is set
- (u - W) is right_complementable Element of the carrier of V
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
u + (- (u - W)) is right_complementable Element of the carrier of V
the addF of V . (u,(- (u - W))) is right_complementable Element of the carrier of V
[u,(- (u - W))] is set
{u,(- (u - W))} is non empty set
{{u,(- (u - W))},{u}} is non empty set
the addF of V . [u,(- (u - W))] is set
- u is right_complementable Element of the carrier of V
(- u) + W is right_complementable Element of the carrier of V
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
u + ((- u) + W) is right_complementable Element of the carrier of V
the addF of V . (u,((- u) + W)) is right_complementable Element of the carrier of V
[u,((- u) + W)] is set
{u,((- u) + W)} is non empty set
{{u,((- u) + W)},{u}} is non empty set
the addF of V . [u,((- u) + W)] is set
u + (- u) is right_complementable Element of the carrier of V
the addF of V . (u,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
(u + (- u)) + W is right_complementable Element of the carrier of V
the addF of V . ((u + (- u)),W) is right_complementable Element of the carrier of V
[(u + (- u)),W] is set
{(u + (- u)),W} is non empty set
{(u + (- u))} is non empty set
{{(u + (- u)),W},{(u + (- u))}} is non empty set
the addF of V . [(u + (- u)),W] is 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) + W is right_complementable Element of the carrier of V
the addF of V . ((0. V),W) is right_complementable Element of the carrier of V
[(0. V),W] is set
{(0. V),W} is non empty set
{(0. V)} is non empty set
{{(0. V),W},{(0. V)}} is non empty set
the addF of V . [(0. V),W] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,W,B) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
W + 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 . (W,C) is right_complementable Element of the carrier of V
[W,C] is set
{W,C} is non empty set
{W} is non empty set
{{W,C},{W}} is non empty set
the addF of V . [W,C] is set
W - u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
W + (- u) is right_complementable Element of the carrier of V
the addF of V . (W,(- u)) is right_complementable Element of the carrier of V
[W,(- u)] is set
{W,(- u)} is non empty set
{{W,(- u)},{W}} is non empty set
the addF of V . [W,(- u)] is set
C is right_complementable Element of the carrier of V
u + C is right_complementable Element of the carrier of V
the addF of V . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is 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
(W + C) - u is right_complementable Element of the carrier of V
(W + C) + (- u) is right_complementable Element of the carrier of V
the addF of V . ((W + C),(- u)) is right_complementable Element of the carrier of V
[(W + C),(- u)] is set
{(W + C),(- u)} is non empty set
{(W + C)} is non empty set
{{(W + C),(- u)},{(W + C)}} is non empty set
the addF of V . [(W + C),(- u)] is set
C + (W - u) is right_complementable Element of the carrier of V
the addF of V . (C,(W - u)) is right_complementable Element of the carrier of V
[C,(W - u)] is set
{C,(W - u)} is non empty set
{C} is non empty set
{{C,(W - u)},{C}} is non empty set
the addF of V . [C,(W - u)] is set
- C is right_complementable Element of the carrier of V
W + u is right_complementable Element of the carrier of V
the addF of V . (W,u) is right_complementable Element of the carrier of V
[W,u] is set
{W,u} is non empty set
{{W,u},{W}} is non empty set
the addF of V . [W,u] is set
(W + u) - u is right_complementable Element of the carrier of V
(W + u) + (- u) is right_complementable Element of the carrier of V
the addF of V . ((W + u),(- u)) is right_complementable Element of the carrier of V
[(W + u),(- u)] is set
{(W + u),(- u)} is non empty set
{(W + u)} is non empty set
{{(W + u),(- u)},{(W + u)}} is non empty set
the addF of V . [(W + u),(- u)] is set
u - u is right_complementable Element of the carrier of V
u + (- u) is right_complementable Element of the carrier of V
the addF of V . (u,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
W + (u - u) is right_complementable Element of the carrier of V
the addF of V . (W,(u - u)) is right_complementable Element of the carrier of V
[W,(u - u)] is set
{W,(u - u)} is non empty set
{{W,(u - u)},{W}} is non empty set
the addF of V . [W,(u - u)] is set
W + (0. V) is right_complementable Element of the carrier of V
the addF of V . (W,(0. V)) is right_complementable Element of the carrier of V
[W,(0. V)] is set
{W,(0. V)} is non empty set
{{W,(0. V)},{W}} is non empty set
the addF of V . [W,(0. V)] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,W,B) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
u + 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 . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
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 . (u,(- W)) is right_complementable Element of the carrier of V
[u,(- W)] is set
{u,(- W)} is non empty set
{{u,(- W)},{u}} is non empty set
the addF of V . [u,(- W)] is set
C is right_complementable Element of the carrier of V
u - C is right_complementable Element of the carrier of V
- C is right_complementable Element of the carrier of V
u + (- C) is right_complementable Element of the carrier of V
the addF of V . (u,(- C)) is right_complementable Element of the carrier of V
[u,(- C)] is set
{u,(- C)} is non empty set
{{u,(- C)},{u}} is non empty set
the addF of V . [u,(- C)] is 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 + C) - W is right_complementable Element of the carrier of V
(u + C) + (- W) is right_complementable Element of the carrier of V
the addF of V . ((u + C),(- W)) is right_complementable Element of the carrier of V
[(u + C),(- W)] is set
{(u + C),(- W)} is non empty set
{(u + C)} is non empty set
{{(u + C),(- W)},{(u + C)}} is non empty set
the addF of V . [(u + C),(- W)] is set
C + (u - W) is right_complementable Element of the carrier of V
the addF of V . (C,(u - W)) is right_complementable Element of the carrier of V
[C,(u - W)] is set
{C,(u - W)} is non empty set
{C} is non empty set
{{C,(u - W)},{C}} is non empty set
the addF of V . [C,(u - W)] is set
- C is right_complementable Element of the carrier of V
u - u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
u + (- u) is right_complementable Element of the carrier of V
the addF of V . (u,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
(u - u) + W is right_complementable Element of the carrier of V
the addF of V . ((u - u),W) is right_complementable Element of the carrier of V
[(u - u),W] is set
{(u - u),W} is non empty set
{(u - u)} is non empty set
{{(u - u),W},{(u - u)}} is non empty set
the addF of V . [(u - u),W] is set
(0. V) + W is right_complementable Element of the carrier of V
the addF of V . ((0. V),W) is right_complementable Element of the carrier of V
[(0. V),W] is set
{(0. V),W} is non empty set
{(0. V)} is non empty set
{{(0. V),W},{(0. V)}} is non empty set
the addF of V . [(0. V),W] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
B is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
(R,V,u,B) is Element of bool the carrier of V
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
the carrier of W is non empty set
the carrier of B is non empty set
C is set
C is right_complementable Element of the carrier of V
u + 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 . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
x is right_complementable Element of the carrier of V
u + x is right_complementable Element of the carrier of V
the addF of V . (u,x) is right_complementable Element of the carrier of V
[u,x] is set
{u,x} is non empty set
{{u,x},{u}} is non empty set
the addF of V . [u,x] is set
C is set
C is right_complementable Element of the carrier of V
u + 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 . (u,C) is right_complementable Element of the carrier of V
[u,C] is set
{u,C} is non empty set
{u} is non empty set
{{u,C},{u}} is non empty set
the addF of V . [u,C] is set
x is right_complementable Element of the carrier of V
u + x is right_complementable Element of the carrier of V
the addF of V . (u,x) is right_complementable Element of the carrier of V
[u,x] is set
{u,x} is non empty set
{{u,x},{u}} is non empty set
the addF of V . [u,x] is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
(R,V,W,C) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
the carrier of C is non empty set
the carrier of B is non empty set
the carrier of B \ the carrier of C is Element of bool the carrier of B
bool the carrier of B is non empty set
the Element of the carrier of B \ the carrier of C is Element of the carrier of B \ the carrier of C
x is right_complementable Element of the carrier of V
u + 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 . (u,x) is right_complementable Element of the carrier of V
[u,x] is set
{u,x} is non empty set
{u} is non empty set
{{u,x},{u}} is non empty set
the addF of V . [u,x] is set
u1 is right_complementable Element of the carrier of V
W + u1 is right_complementable Element of the carrier of V
the addF of V . (W,u1) is right_complementable Element of the carrier of V
[W,u1] is set
{W,u1} is non empty set
{W} is non empty set
{{W,u1},{W}} is non empty set
the addF of V . [W,u1] is 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) + x is right_complementable Element of the carrier of V
the addF of V . ((0. V),x) is right_complementable Element of the carrier of V
[(0. V),x] is set
{(0. V),x} is non empty set
{(0. V)} is non empty set
{{(0. V),x},{(0. V)}} is non empty set
the addF of V . [(0. V),x] is set
- u is right_complementable Element of the carrier of V
u + (- u) is right_complementable Element of the carrier of V
the addF of V . (u,(- u)) is right_complementable Element of the carrier of V
[u,(- u)] is set
{u,(- u)} is non empty set
{{u,(- u)},{u}} is non empty set
the addF of V . [u,(- u)] is set
(u + (- u)) + x is right_complementable Element of the carrier of V
the addF of V . ((u + (- u)),x) is right_complementable Element of the carrier of V
[(u + (- u)),x] is set
{(u + (- u)),x} is non empty set
{(u + (- u))} is non empty set
{{(u + (- u)),x},{(u + (- u))}} is non empty set
the addF of V . [(u + (- u)),x] is set
(- u) + (W + u1) is right_complementable Element of the carrier of V
the addF of V . ((- u),(W + u1)) is right_complementable Element of the carrier of V
[(- u),(W + u1)] is set
{(- u),(W + u1)} is non empty set
{(- u)} is non empty set
{{(- u),(W + u1)},{(- u)}} is non empty set
the addF of V . [(- u),(W + u1)] is set
u + ((- u) + (W + u1)) is right_complementable Element of the carrier of V
the addF of V . (u,((- u) + (W + u1))) is right_complementable Element of the carrier of V
[u,((- u) + (W + u1))] is set
{u,((- u) + (W + u1))} is non empty set
{{u,((- u) + (W + u1))},{u}} is non empty set
the addF of V . [u,((- u) + (W + u1))] is set
(R,V,(u + ((- u) + (W + u1))),B) is Element of bool the carrier of V
{ ((u + ((- u) + (W + u1))) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(u + (- u)) + (W + u1) is right_complementable Element of the carrier of V
the addF of V . ((u + (- u)),(W + u1)) is right_complementable Element of the carrier of V
[(u + (- u)),(W + u1)] is set
{(u + (- u)),(W + u1)} is non empty set
{{(u + (- u)),(W + u1)},{(u + (- u))}} is non empty set
the addF of V . [(u + (- u)),(W + u1)] is set
(0. V) + (W + u1) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(W + u1)) is right_complementable Element of the carrier of V
[(0. V),(W + u1)] is set
{(0. V),(W + u1)} is non empty set
{{(0. V),(W + u1)},{(0. V)}} is non empty set
the addF of V . [(0. V),(W + u1)] is set
(R,V,(W + u1),C) is Element of bool the carrier of V
{ ((W + u1) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
(R,V,(W + u1),B) is Element of bool the carrier of V
{ ((W + u1) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
the carrier of C \ the carrier of B is Element of bool the carrier of C
bool the carrier of C is non empty set
the Element of the carrier of C \ the carrier of B is Element of the carrier of C \ the carrier of B
x is right_complementable Element of the carrier of V
W + x is right_complementable Element of the carrier of V
the addF of V . (W,x) is right_complementable Element of the carrier of V
[W,x] is set
{W,x} is non empty set
{{W,x},{W}} is non empty set
the addF of V . [W,x] is set
u1 is right_complementable Element of the carrier of V
u + u1 is right_complementable Element of the carrier of V
the addF of V . (u,u1) is right_complementable Element of the carrier of V
[u,u1] is set
{u,u1} is non empty set
{{u,u1},{u}} is non empty set
the addF of V . [u,u1] is set
(0. V) + x is right_complementable Element of the carrier of V
the addF of V . ((0. V),x) is right_complementable Element of the carrier of V
[(0. V),x] is set
{(0. V),x} is non empty set
{{(0. V),x},{(0. V)}} is non empty set
the addF of V . [(0. V),x] is set
- W is right_complementable Element of the carrier of V
W + (- W) is right_complementable Element of the carrier of V
the addF of V . (W,(- W)) is right_complementable Element of the carrier of V
[W,(- W)] is set
{W,(- W)} is non empty set
{{W,(- W)},{W}} is non empty set
the addF of V . [W,(- W)] is set
(W + (- W)) + x is right_complementable Element of the carrier of V
the addF of V . ((W + (- W)),x) is right_complementable Element of the carrier of V
[(W + (- W)),x] is set
{(W + (- W)),x} is non empty set
{(W + (- W))} is non empty set
{{(W + (- W)),x},{(W + (- W))}} is non empty set
the addF of V . [(W + (- W)),x] is set
(- W) + (u + u1) is right_complementable Element of the carrier of V
the addF of V . ((- W),(u + u1)) is right_complementable Element of the carrier of V
[(- W),(u + u1)] is set
{(- W),(u + u1)} is non empty set
{(- W)} is non empty set
{{(- W),(u + u1)},{(- W)}} is non empty set
the addF of V . [(- W),(u + u1)] is set
W + ((- W) + (u + u1)) is right_complementable Element of the carrier of V
the addF of V . (W,((- W) + (u + u1))) is right_complementable Element of the carrier of V
[W,((- W) + (u + u1))] is set
{W,((- W) + (u + u1))} is non empty set
{{W,((- W) + (u + u1))},{W}} is non empty set
the addF of V . [W,((- W) + (u + u1))] is set
(R,V,(W + ((- W) + (u + u1))),C) is Element of bool the carrier of V
{ ((W + ((- W) + (u + u1))) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
(W + (- W)) + (u + u1) is right_complementable Element of the carrier of V
the addF of V . ((W + (- W)),(u + u1)) is right_complementable Element of the carrier of V
[(W + (- W)),(u + u1)] is set
{(W + (- W)),(u + u1)} is non empty set
{{(W + (- W)),(u + u1)},{(W + (- W))}} is non empty set
the addF of V . [(W + (- W)),(u + u1)] is set
(0. V) + (u + u1) is right_complementable Element of the carrier of V
the addF of V . ((0. V),(u + u1)) is right_complementable Element of the carrier of V
[(0. V),(u + u1)] is set
{(0. V),(u + u1)} is non empty set
{{(0. V),(u + u1)},{(0. V)}} is non empty set
the addF of V . [(0. V),(u + u1)] is set
(R,V,(u + u1),B) is Element of bool the carrier of V
{ ((u + u1) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,(u + u1),C) is Element of bool the carrier of V
{ ((u + u1) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in C } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
B is (R,V,W)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
W is (R,V,u)
the carrier of V is non empty set
B is right_complementable Element of the carrier of V
(R,V,B,u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (B + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is 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
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
W is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
B is (R,V,u)
C is (R,V,W)
the carrier of V is non empty set
C is right_complementable Element of the carrier of V
(R,V,C,u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
c₈ is right_complementable Element of the carrier of V
(R,V,c₈,W) is Element of bool the carrier of V
{ (c₈ + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
u is right_complementable Element of the carrier of V
{u} is non empty Element of bool the carrier of V
bool the carrier of V is non empty set
(R,V,u,(R,V)) is Element of bool the carrier of V
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
bool the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,V)
u is Element of bool the carrier of V
W is right_complementable Element of the carrier of V
(R,V,W,(R,V)) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
{W} is non empty Element of bool the carrier of V
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
u is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
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
(R,V,(0. V),u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ ((0. V) + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,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 ZeroF of V is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
the right_complementable Element of the carrier of V is right_complementable Element of the carrier of V
bool the carrier of V is non empty set
W is Element of bool the carrier of V
(R,V, the right_complementable Element of the carrier of V,(R,V)) is Element of bool the carrier of V
{ ( the right_complementable Element of the carrier of V + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
bool the carrier of V is non empty set
(R,V) is non empty right_complementable Abelian add-associative right_zeroed strict RightMod-like (R,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 ZeroF of V is right_complementable Element of the carrier of V
the rmult of V is Relation-like Function-like V18([: the carrier of V, the carrier of R:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of R:], the carrier of V:]
the carrier of R is non empty set
[: the carrier of V, the carrier of R:] is Relation-like non empty set
[:[: the carrier of V, the carrier of R:], the carrier of V:] is Relation-like non empty set
bool [:[: the carrier of V, the carrier of R:], the carrier of V:] is non empty set
RightModStr(# the carrier of V, the addF of V, the ZeroF of V, the rmult of V #) is non empty strict RightModStr over R
u is Element of bool the carrier of V
W is right_complementable Element of the carrier of V
(R,V,W,(R,V)) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in (R,V) } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
the carrier of u is non empty set
W is (R,V,u)
B is right_complementable Element of the carrier of V
(R,V,B,u) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (B + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in u } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
(R,V,u,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
B is (R,V,W)
C is right_complementable Element of the carrier of V
(R,V,C,W) is Element of bool the carrier of V
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
C is (R,V,B)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,W,B) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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
B is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
C is (R,V,B)
(R,V,u,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (u + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
(R,V,W,B) is Element of bool the carrier of V
{ (W + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
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 Abelian add-associative right_zeroed RightMod-like (R,V)
C is (R,V,B)
C is right_complementable Element of the carrier of V
(R,V,C,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is right_complementable Element of the carrier of V
(R,V,C,B) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in B } is set
C is (R,V,B)
R is non empty right_complementable unital associative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
V is non empty right_complementable Abelian add-associative right_zeroed RightMod-like RightModStr over R
the carrier of V is non empty set
u is right_complementable Element of the carrier of V
W is non empty right_complementable Abelian add-associative right_zeroed RightMod-like (R,V)
B is (R,V,W)
C is (R,V,W)
C is right_complementable Element of the carrier of V
(R,V,C,W) is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (C + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set
c₈ is right_complementable Element of the carrier of V
(R,V,c₈,W) is Element of bool the carrier of V
{ (c₈ + b₁) where b₁ is right_complementable Element of the carrier of V : b₁ in W } is set