:: RLSUB_1 semantic presentation

REAL is non empty V36() set

bool REAL is non empty set

bool NAT is non empty set
bool NAT is non empty set

- 1 is V31() real V33() Element of REAL

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

the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
u is Element of bool the carrier of V
the Element of u is Element of u

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (0,B) is set
[0,B] is set
{0,B} is non empty set
is non empty set
{{0,B},} is non empty set
the Mult of V . [0,B] 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 Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . ((- 1),W) is set
[(- 1),W] is set
{(- 1),W} is non empty set
{(- 1)} is non empty set
{{(- 1),W},{(- 1)}} is non empty set
the Mult of V . [(- 1),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

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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

the ZeroF of V is left_complementable right_complementable 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

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable complementable Element of the carrier of V
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the addF of V . [u,W] is set
u is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (u,W) is set
[u,W] is set
{u,W} is non empty set
{u} is non empty set
{{u,W},{u}} is non empty set
the Mult of V . [u,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

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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
W is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (W,B) is set
[W,B] is set
{W,B} is non empty set
{W} is non empty set
{{W,B},{W}} is non empty set
the Mult of V . [W,B] 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 left_complementable right_complementable complementable Element of the carrier of V : ( b1 in u & b2 in W ) } is set
B is Element of bool the carrier of V

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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

the addF of V . (c7,x) is left_complementable right_complementable complementable Element of the carrier of V
[c7,x] is set
{c7,x} is non empty set
{c7} is non empty set
{{c7,x},{c7}} is non empty set
the addF of V . [c7,x] is set

the addF of V . (x,z) is left_complementable right_complementable 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
(c7 + x) + x is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((c7 + x),x) is left_complementable right_complementable complementable Element of the carrier of V
[(c7 + x),x] is set
{(c7 + x),x} is non empty set
{(c7 + x)} is non empty set
{{(c7 + x),x},{(c7 + x)}} is non empty set
the addF of V . [(c7 + x),x] is set
((c7 + x) + x) + z is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (((c7 + x) + x),z) is left_complementable right_complementable complementable Element of the carrier of V
[((c7 + x) + x),z] is set
{((c7 + x) + x),z} is non empty set
{((c7 + x) + x)} is non empty set
{{((c7 + x) + x),z},{((c7 + x) + x)}} is non empty set
the addF of V . [((c7 + x) + x),z] is set

the addF of V . (c7,x) is left_complementable right_complementable complementable Element of the carrier of V
[c7,x] is set
{c7,x} is non empty set
{{c7,x},{c7}} is non empty set
the addF of V . [c7,x] is set
(c7 + x) + x is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((c7 + x),x) is left_complementable right_complementable complementable Element of the carrier of V
[(c7 + x),x] is set
{(c7 + x),x} is non empty set
{(c7 + x)} is non empty set
{{(c7 + x),x},{(c7 + x)}} is non empty set
the addF of V . [(c7 + x),x] is set
((c7 + x) + x) + z is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (((c7 + x) + x),z) is left_complementable right_complementable complementable Element of the carrier of V
[((c7 + x) + x),z] is set
{((c7 + x) + x),z} is non empty set
{((c7 + x) + x)} is non empty set
{{((c7 + x) + x),z},{((c7 + x) + x)}} is non empty set
the addF of V . [((c7 + x) + x),z] is set

the addF of V . (x,z) is left_complementable right_complementable 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
(c7 + x) + (x + z) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((c7 + x),(x + z)) is left_complementable right_complementable complementable Element of the carrier of V
[(c7 + x),(x + z)] is set
{(c7 + x),(x + z)} is non empty set
{{(c7 + x),(x + z)},{(c7 + x)}} is non empty set
the addF of V . [(c7 + x),(x + z)] is set
C is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (C,C) is set
[C,C] is set
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the Mult of V . [C,C] is set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the addF of V . (c7,x) is left_complementable right_complementable complementable Element of the carrier of V
[c7,x] is set
{c7,x} is non empty set
{c7} is non empty set
{{c7,x},{c7}} is non empty set
the addF of V . [c7,x] is set

the Mult of V . (C,c7) is set
[C,c7] is set
{C,c7} is non empty set
{{C,c7},{C}} is non empty set
the Mult of V . [C,c7] is set

the Mult of V . (C,x) is set
[C,x] is set
{C,x} is non empty set
{{C,x},{C}} is non empty set
the Mult of V . [C,x] is set
(C * c7) + (C * x) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((C * c7),(C * x)) is left_complementable right_complementable complementable Element of the carrier of V
[(C * c7),(C * x)] is set
{(C * c7),(C * x)} is non empty set
{(C * c7)} is non empty set
{{(C * c7),(C * x)},{(C * c7)}} is non empty set
the addF of V . [(C * c7),(C * x)] 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

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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
B is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (B,C) is set
[B,C] is set
{B,C} is non empty set
{B} is non empty set
{{B,C},{B}} is non empty set
the Mult of V . [B,C] is set

the carrier of V is non empty set

the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the addF of V || the carrier of V is Relation-like Function-like set
the addF of V | [: the carrier of V, the carrier of V:] is Relation-like Function-like set
the Mult of V | [:REAL, the carrier of V:] is Relation-like Function-like set

u is set

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

u is set

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

the carrier of V is non empty set

the carrier of u is non empty set

the carrier of u is non empty set
the ZeroF of u is left_complementable right_complementable complementable Element of the carrier of u

the carrier of V is non empty set
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V

the carrier of u is non empty set
the ZeroF of u is left_complementable right_complementable complementable Element of the carrier of u

the carrier of W is non empty set
the ZeroF of W is left_complementable right_complementable complementable Element of the carrier of W

the carrier of V is non empty set
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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

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

the carrier of V is non empty set

W is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (W,u) is set
[W,u] is set
{W,u} is non empty set
{W} is non empty set
{{W,u},{W}} is non empty set
the Mult of V . [W,u] is set

the carrier of B is non empty set

the Mult of B is Relation-like [:REAL, the carrier of B:] -defined the carrier of B -valued Function-like V18([:REAL, the carrier of B:], the carrier of B) Element of bool [:[:REAL, the carrier of B:], the carrier of B:]
[:REAL, the carrier of B:] is non empty set
[:[:REAL, the carrier of B:], the carrier of B:] is non empty set
bool [:[:REAL, the carrier of B:], the carrier of B:] is non empty set
the Mult of B . (W,C) is set
[W,C] is set
{W,C} is non empty set
{{W,C},{W}} is non empty set
the Mult of B . [W,C] is set
the Mult of V | [:REAL, the carrier of B:] is Relation-like Function-like set
[W,C] is Element of [:REAL, the carrier of B:]
( the Mult of V | [:REAL, the carrier of B:]) . [W,C] is set

the carrier of V is non empty set

the carrier of W is non empty set

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . ((- 1),u) is set
[(- 1),u] is set
{(- 1),u} is non empty set
{(- 1)} is non empty set
{{(- 1),u},{(- 1)}} is non empty set
the Mult of V . [(- 1),u] is set

the Mult of W is Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V18([:REAL, the carrier of W:], the carrier of W) Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . ((- 1),B) is set
[(- 1),B] is set
{(- 1),B} is non empty set
{{(- 1),B},{(- 1)}} is non empty set
the Mult of W . [(- 1),B] is set

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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

the addF of B is Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued 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 non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is 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 left_complementable right_complementable 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

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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,c7) is left_complementable right_complementable complementable Element of the carrier of V
[C,c7] is set
{C,c7} is non empty set
{C} is non empty set
{{C,c7},{C}} is non empty set
the addF of V . [C,c7] is set

the carrier of C is non empty set

the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued 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 non empty set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is 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 left_complementable right_complementable 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

C is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (C,c7) is set
[C,c7] is set
{C,c7} is non empty set
{C} is non empty set
{{C,c7},{C}} is non empty set
the Mult of V . [C,c7] is set

the carrier of C is non empty set

the Mult of C is Relation-like [:REAL, the carrier of C:] -defined the carrier of C -valued Function-like V18([:REAL, the carrier of C:], the carrier of C) Element of bool [:[:REAL, the carrier of C:], the carrier of C:]
[:REAL, the carrier of C:] is non empty set
[:[:REAL, the carrier of C:], the carrier of C:] is non empty set
bool [:[:REAL, the carrier of C:], the carrier of C:] is non empty set
the Mult of C . (C,x) is set
[C,x] is set
{C,x} is non empty set
{{C,x},{C}} is non empty set
the Mult of C . [C,x] is set

the carrier of V is non empty set
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V

the carrier of u is non empty set
the ZeroF of u is left_complementable right_complementable complementable Element of the carrier of u

the carrier of u is non empty set
the ZeroF of u is left_complementable right_complementable complementable Element of the carrier of u

the carrier of V is non empty set
the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V

the carrier of u is non empty set
the ZeroF of u is left_complementable right_complementable complementable Element of the carrier of u

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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 V is non empty set

W is V31() real V33() Element of REAL

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . (W,u) is set
[W,u] is set
{W,u} is non empty set
{W} is non empty set
{{W,u},{W}} is non empty set
the Mult of V . [W,u] 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 V is non empty set

the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
the Mult of V . ((- 1),u) is set
[(- 1),u] is set
{(- 1),u} is non empty set
{(- 1)} is non empty set
{{(- 1),u},{(- 1)}} is non empty set
the Mult of V . [(- 1),u] is set

the carrier of V is non empty set

the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is 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 left_complementable right_complementable 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 V is non empty set
bool the carrier of V is non empty set

the ZeroF of V is left_complementable right_complementable complementable Element of the carrier of V
the addF of V is Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued 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 non empty set
[:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
bool [:[: the carrier of V, the carrier of V:], the carrier of V:] is non empty set
the Mult of V is Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V18([:REAL, the carrier of V:], the carrier of V) Element of bool [:[:REAL, the carrier of V:], the carrier of V:]
[:REAL, the carrier of V:] is non empty set
[:[:REAL, the carrier of V:], the carrier of V:] is non empty set
bool [:[:REAL, the carrier of V:], the carrier of V:] is non empty set
u is Element of bool the carrier of V
the addF of V || u is Relation-like Function-like set
[:u,u:] is set
the addF of V | [:u,u:] is Relation-like Function-like set
[:REAL,u:] is set

W is non empty set
[:W,W:] is non empty set
[:[:W,W:],W:] is non empty set
bool [:[:W,W:],W:] is non empty set
[:REAL,W:] is non empty set
[:[:REAL,W:],W:] is non empty set
bool [:[:REAL,W:],W:] is non empty set
B is Element of W
C is Relation-like [:W,W:] -defined W -valued Function-like V18([:W,W:],W) Element of bool [:[:W,W:],W:]

RLSStruct(# W,B,C,C #) is non empty strict RLSStruct
the carrier of RLSStruct(# W,B,C,C #) is non empty set
x is V31() real V33() Element of REAL
x is Element of the carrier of RLSStruct(# W,B,C,C #)
x * x is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) is Relation-like [:REAL, the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[:REAL, the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the Mult of RLSStruct(# W,B,C,C #) . (x,x) is set
[x,x] is set
{x,x} is non empty set
{x} is non empty set
{{x,x},{x}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [x,x] is set
the Mult of V . (x,x) is set
the Mult of V . [x,x] is set
[x,x] is Element of [:REAL, the carrier of RLSStruct(# W,B,C,C #):]
the Mult of V . [x,x] is set
x is Element of the carrier of RLSStruct(# W,B,C,C #)
x is Element of the carrier of RLSStruct(# W,B,C,C #)
x + x is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (x,x) is Element of the carrier of RLSStruct(# W,B,C,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 RLSStruct(# W,B,C,C #) . [x,x] is set
the addF of V . (x,x) is set
the addF of V . [x,x] is set
[x,x] is Element of [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):]
the addF of V . [x,x] is set
z is Element of the carrier of RLSStruct(# W,B,C,C #)
u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
z + u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (z,u1) is Element of the carrier of RLSStruct(# W,B,C,C #)
[z,u1] is set
{z,u1} is non empty set
{z} is non empty set
{{z,u1},{z}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [z,u1] is set
u1 + z is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) . (u1,z) is Element of the carrier of RLSStruct(# W,B,C,C #)
[u1,z] is set
{u1,z} is non empty set
{u1} is non empty set
{{u1,z},{u1}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [u1,z] is set

the addF of V . (x2,v1) is left_complementable right_complementable complementable Element of the carrier of V
[x2,v1] is set
{x2,v1} is non empty set
{x2} is non empty set
{{x2,v1},{x2}} is non empty set
the addF of V . [x2,v1] is set

the addF of V . (v1,x2) is left_complementable right_complementable complementable Element of the carrier of V
[v1,x2] is set
{v1,x2} is non empty set
{v1} is non empty set
{{v1,x2},{v1}} is non empty set
the addF of V . [v1,x2] is set
z is Element of the carrier of RLSStruct(# W,B,C,C #)
u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
z + u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (z,u1) is Element of the carrier of RLSStruct(# W,B,C,C #)
[z,u1] is set
{z,u1} is non empty set
{z} is non empty set
{{z,u1},{z}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [z,u1] is set
x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
(z + u1) + x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) . ((z + u1),x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
[(z + u1),x2] is set
{(z + u1),x2} is non empty set
{(z + u1)} is non empty set
{{(z + u1),x2},{(z + u1)}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [(z + u1),x2] is set
u1 + x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) . (u1,x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
[u1,x2] is set
{u1,x2} is non empty set
{u1} is non empty set
{{u1,x2},{u1}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [u1,x2] is set
z + (u1 + x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) . (z,(u1 + x2)) is Element of the carrier of RLSStruct(# W,B,C,C #)
[z,(u1 + x2)] is set
{z,(u1 + x2)} is non empty set
{{z,(u1 + x2)},{z}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [z,(u1 + x2)] is set

the addF of V . ((z + u1),b) is set
[(z + u1),b] is set
{(z + u1),b} is non empty set
{{(z + u1),b},{(z + u1)}} is non empty set
the addF of V . [(z + u1),b] is set

the addF of V . (v1,v2) is left_complementable right_complementable complementable Element of the carrier of V
[v1,v2] is set
{v1,v2} is non empty set
{v1} is non empty set
{{v1,v2},{v1}} is non empty set
the addF of V . [v1,v2] is set
(v1 + v2) + b is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . ((v1 + v2),b) is left_complementable right_complementable complementable Element of the carrier of V
[(v1 + v2),b] is set
{(v1 + v2),b} is non empty set
{(v1 + v2)} is non empty set
{{(v1 + v2),b},{(v1 + v2)}} is non empty set
the addF of V . [(v1 + v2),b] is set

the addF of V . (v2,b) is left_complementable right_complementable complementable Element of the carrier of V
[v2,b] is set
{v2,b} is non empty set
{v2} is non empty set
{{v2,b},{v2}} is non empty set
the addF of V . [v2,b] is set
v1 + (v2 + b) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (v1,(v2 + b)) is left_complementable right_complementable complementable Element of the carrier of V
[v1,(v2 + b)] is set
{v1,(v2 + b)} is non empty set
{{v1,(v2 + b)},{v1}} is non empty set
the addF of V . [v1,(v2 + b)] is set
the addF of V . (v1,(u1 + x2)) is set
[v1,(u1 + x2)] is set
{v1,(u1 + x2)} is non empty set
{{v1,(u1 + x2)},{v1}} is non empty set
the addF of V . [v1,(u1 + x2)] is set
z is Element of the carrier of RLSStruct(# W,B,C,C #)
0. RLSStruct(# W,B,C,C #) is V55( RLSStruct(# W,B,C,C #)) Element of the carrier of RLSStruct(# W,B,C,C #)
the ZeroF of RLSStruct(# W,B,C,C #) is Element of the carrier of RLSStruct(# W,B,C,C #)
z + (0. RLSStruct(# W,B,C,C #)) is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (z,(0. RLSStruct(# W,B,C,C #))) is Element of the carrier of RLSStruct(# W,B,C,C #)
[z,(0. RLSStruct(# W,B,C,C #))] is set
{z,(0. RLSStruct(# W,B,C,C #))} is non empty set
{z} is non empty set
{{z,(0. RLSStruct(# W,B,C,C #))},{z}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [z,(0. RLSStruct(# W,B,C,C #))] is set

u1 + (0. V) is left_complementable right_complementable complementable Element of the carrier of V
the addF of V . (u1,(0. V)) is left_complementable right_complementable complementable Element of the carrier of V
[u1,(0. V)] is set
{u1,(0. V)} is non empty set
{u1} is non empty set
{{u1,(0. V)},{u1}} is non empty set
the addF of V . [u1,(0. V)] is set
z is Element of the carrier of RLSStruct(# W,B,C,C #)

the addF of V . (u1,x2) is left_complementable right_complementable complementable Element of the carrier of V
[u1,x2] is set
{u1,x2} is non empty set
{u1} is non empty set
{{u1,x2},{u1}} is non empty set
the addF of V . [u1,x2] is set

(- 1) * u1 is left_complementable right_complementable complementable Element of the carrier of V
the Mult of V . ((- 1),u1) is set
[(- 1),u1] is set
{(- 1),u1} is non empty set
{(- 1)} is non empty set
{{(- 1),u1},{(- 1)}} is non empty set
the Mult of V . [(- 1),u1] is set
(- 1) * z is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) is Relation-like [:REAL, the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[:REAL, the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the Mult of RLSStruct(# W,B,C,C #) . ((- 1),z) is set
[(- 1),z] is set
{(- 1),z} is non empty set
{{(- 1),z},{(- 1)}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [(- 1),z] is set
v1 is Element of the carrier of RLSStruct(# W,B,C,C #)
z + v1 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (z,v1) is Element of the carrier of RLSStruct(# W,B,C,C #)
[z,v1] is set
{z,v1} is non empty set
{z} is non empty set
{{z,v1},{z}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [z,v1] is set
0. RLSStruct(# W,B,C,C #) is V55( RLSStruct(# W,B,C,C #)) Element of the carrier of RLSStruct(# W,B,C,C #)
the ZeroF of RLSStruct(# W,B,C,C #) is Element of the carrier of RLSStruct(# W,B,C,C #)
z is V31() real V33() set
u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
u1 + x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) is Relation-like [: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[: the carrier of RLSStruct(# W,B,C,C #), the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the addF of RLSStruct(# W,B,C,C #) . (u1,x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
[u1,x2] is set
{u1,x2} is non empty set
{u1} is non empty set
{{u1,x2},{u1}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [u1,x2] is set
z * (u1 + x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) is Relation-like [:REAL, the carrier of RLSStruct(# W,B,C,C #):] -defined the carrier of RLSStruct(# W,B,C,C #) -valued Function-like V18([:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #)) Element of bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):]
[:REAL, the carrier of RLSStruct(# W,B,C,C #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# W,B,C,C #):], the carrier of RLSStruct(# W,B,C,C #):] is non empty set
the Mult of RLSStruct(# W,B,C,C #) . (z,(u1 + x2)) is set
[z,(u1 + x2)] is set
{z,(u1 + x2)} is non empty set
{z} is non empty set
{{z,(u1 + x2)},{z}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [z,(u1 + x2)] is set
z * u1 is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) . (z,u1) is set
[z,u1] is set
{z,u1} is non empty set
{{z,u1},{z}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [z,u1] is set
z * x2 is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) . (z,x2) is set
[z,x2] is set
{z,x2} is non empty set
{{z,x2},{z}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [z,x2] is set
(z * u1) + (z * x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
the addF of RLSStruct(# W,B,C,C #) . ((z * u1),(z * x2)) is Element of the carrier of RLSStruct(# W,B,C,C #)
[(z * u1),(z * x2)] is set
{(z * u1),(z * x2)} is non empty set
{(z * u1)} is non empty set
{{(z * u1),(z * x2)},{(z * u1)}} is non empty set
the addF of RLSStruct(# W,B,C,C #) . [(z * u1),(z * x2)] is set
b is V31() real V33() Element of REAL
b * (u1 + x2) is Element of the carrier of RLSStruct(# W,B,C,C #)
the Mult of RLSStruct(# W,B,C,C #) . (b,(u1 + x2)) is set
[b,(u1 + x2)] is set
{b,(u1 + x2)} is non empty set
{b} is non empty set
{{b,(u1 + x2)},{b}} is non empty set
the Mult of RLSStruct(# W,B,C,C #) . [b,(u1 + x2)] is set
the Mult of V