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

x is right_complementable Element of the carrier of V

c

the addF of V . (c

[c

{c

{c

{{c

the addF of V . [c

x is right_complementable Element of the carrier of V

z is right_complementable Element of the carrier of V

x + z is right_complementable Element of the carrier of V

the addF of V . (x,z) is right_complementable Element of the carrier of V

[x,z] is set

{x,z} is non empty set

{x} is non empty set

{{x,z},{x}} is non empty set

the addF of V . [x,z] is set

(c

the addF of V . ((c

[(c

{(c

{(c

{{(c

the addF of V . [(c

((c

the addF of V . (((c

[((c

{((c

{((c

{{((c

the addF of V . [((c

c

the addF of V . (c

[c

{c

{{c

the addF of V . [c

(c

the addF of V . ((c

[(c

{(c

{(c

{{(c

the addF of V . [(c

((c

the addF of V . (((c

[((c

{((c

{((c

{{((c

the addF of V . [((c

x + z is right_complementable Element of the carrier of V

the addF of V . (x,z) is right_complementable Element of the carrier of V

[x,z] is set

{x,z} is non empty set

{x} is non empty set

{{x,z},{x}} is non empty set

the addF of V . [x,z] is set

(c

the addF of V . ((c

[(c

{(c

{{(c

the addF of V . [(c

the carrier of 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

x is right_complementable Element of the carrier of V

c

the addF of V is Relation-like Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the addF of V . (c

[c

{c

{c

{{c

the addF of V . [c

c

the rmult of V . (c

[c

{c

{{c

the rmult of V . [c

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

the addF of V . ((c

[(c

{(c

{(c

{{(c

the addF of V . [(c

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

C + c

the addF of V is Relation-like Function-like V18([: the carrier of V, the carrier of V:], the carrier of V) Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

[: the carrier of V, the carrier of V:] is Relation-like non empty set

[:[: the carrier of V, the carrier of V:], the carrier of V:] is Relation-like non empty set

bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set

the addF of V . (C,c

[C,c

{C,c

{C} is non empty set

{{C,c

the addF of V . [C,c

C is non empty right_complementable 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

c

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

{c

{c

{{c

the rmult of V . [c

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

C + c

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

[C,c

{C,c

{C} is non empty set

{{C,c

the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [C,c

(C + c

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

[(C + c

{(C + c

{(C + c

{{(C + c

the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C + 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,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

the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . (c

[c

{c

{c

{{c

the rmult of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [c

(C * B) + (c

the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . ((C * B),(c

[(C * B),(c

{(C * B),(c

{(C * B)} is non empty set

{{(C * B),(c

the addF of RightModStr(# the carrier of V, the addF of V,(0. V), the rmult of V #) . [(C * B),(c

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

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

the addF of V . (C,c

[C,c

{C,c

{C} is non empty set

{{C,c

the addF 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 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 #)