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

1 is non empty set

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

the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V49(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
u is Element of bool the carrier of V
the Element of u is Element of u
0. 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

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

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

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

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

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

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

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

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

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

the carrier of V is non empty set

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

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

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

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

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

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

the carrier of R is non empty set
V is right_complementable Element of the carrier of 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

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

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

the carrier of W is non empty set
B is right_complementable Element of the carrier of W
- B is right_complementable Element of the carrier of W
1_ 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

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

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

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

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

the carrier of C is non empty set
x is right_complementable Element of the carrier of C
x is right_complementable Element of the carrier of C
x + x is right_complementable Element of the carrier of C
the addF of C is Relation-like Function-like V18([: the carrier of C, the carrier of C:], the carrier of C) Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is Relation-like non empty set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is Relation-like non empty set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is non empty set
the addF of C . (x,x) is right_complementable Element of the carrier of C
[x,x] is set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
the addF of C . [x,x] is set
z is right_complementable Element of the carrier of W
the carrier of R is non empty set
C is right_complementable Element of the carrier of R
c8 is right_complementable Element of the carrier of V
c8 * 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 . (c8,C) is right_complementable Element of the carrier of V
[c8,C] is set
{c8,C} is non empty set
{c8} is non empty set
{{c8,C},{c8}} is non empty set
the rmult of V . [c8,C] is set

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

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

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

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

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

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

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

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

the carrier of R is non empty set
V is right_complementable Element of the carrier of 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

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

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

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

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

the 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

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

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 #)
c8 is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
C + c8 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,c8) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[C,c8] is set
{C,c8} is non empty set
{C} is non empty set
{{C,c8},{C}} is non empty set
the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,c8] is set
(C + c8) * 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 + c8),B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C + c8),B] is set
{(C + c8),B} is non empty set
{(C + c8)} is non empty set
{{(C + c8),B},{(C + c8)}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C + c8),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
c8 * 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 #) . (c8,B) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[c8,B] is set
{c8,B} is non empty set
{c8} is non empty set
{{c8,B},{c8}} is non empty set
the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [c8,B] is set
(C * B) + (c8 * 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),(c8 * B)) is Element of the carrier of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #)
[(C * B),(c8 * B)] is set
{(C * B),(c8 * B)} is non empty set
{(C * B)} is non empty set
{{(C * B),(c8 * 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),(c8 * 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 #)
c8 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 + c8 is right_complementable Element of the carrier of V
the addF of V . (C,c8) is right_complementable Element of the carrier of V
[C,c8] is set
{C,c8} is non empty set
{C} is non empty set
{{C,c8},{C}} is non empty set
the addF of V . [C,c8] is set
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 #)