:: RLSUB_1 semantic presentation

REAL is non empty V36() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

bool NAT is non empty set

bool NAT is non empty set

{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() set

the Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() set is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V31() real V33() Element of NAT

0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V33() Element of NAT

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

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

B is left_complementable right_complementable complementable Element of the carrier of V

0 * B is left_complementable right_complementable complementable Element of 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 . (0,B) is set

[0,B] is set

{0,B} is non empty set

{0} is non empty set

{{0,B},{0}} is non empty set

the Mult of V . [0,B] is set

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Element of the carrier of V

- W is left_complementable right_complementable complementable Element of the carrier of V

(- 1) * W is left_complementable right_complementable complementable Element of 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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Element of the carrier of V

B is left_complementable right_complementable complementable Element of the carrier of V

W - B is left_complementable right_complementable complementable Element of the carrier of V

- B is left_complementable right_complementable complementable Element of the carrier of V

W + (- B) 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 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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

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

u is left_complementable right_complementable complementable Element of the carrier of V

W is left_complementable right_complementable complementable Element of the carrier of V

u + W 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 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

W is left_complementable right_complementable complementable Element of the carrier of V

u * W is left_complementable right_complementable complementable Element of 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 . (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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Element of the carrier of V

B is left_complementable right_complementable complementable Element of the carrier of V

W + B 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 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

B is left_complementable right_complementable complementable Element of the carrier of V

W * B is left_complementable right_complementable complementable Element of 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 . (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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Element of the carrier of V

C is left_complementable right_complementable complementable Element of the carrier of V

C + C 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 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

c

x is left_complementable right_complementable complementable Element of the carrier of V

c

the addF of V . (c

[c

{c

{c

{{c

the addF of V . [c

x is left_complementable right_complementable complementable Element of the carrier of V

z is left_complementable right_complementable complementable Element of the carrier of V

x + z is left_complementable right_complementable complementable Element of the carrier of V

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

(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 left_complementable right_complementable complementable Element of the carrier of V

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

(c

the addF of V . ((c

[(c

{(c

{{(c

the addF of V . [(c

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

C is left_complementable right_complementable complementable Element of the carrier of V

C * C is left_complementable right_complementable complementable Element of 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 . (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

c

x is left_complementable right_complementable complementable Element of the carrier of V

c

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

{c

{c

{{c

the addF of V . [c

C * c

the Mult of V . (C,c

[C,c

{C,c

{{C,c

the Mult of V . [C,c

C * x is left_complementable right_complementable complementable Element of the carrier of V

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

the addF of V . ((C * c

[(C * c

{(C * c

{(C * c

{{(C * c

the addF of V . [(C * c

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Element of the carrier of V

C is left_complementable right_complementable complementable Element of the carrier of V

B + C 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 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

C is left_complementable right_complementable complementable Element of the carrier of V

B * C is left_complementable right_complementable complementable Element of 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 . (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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is set

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of W is non empty set

the carrier of B is non empty set

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is set

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of W is non empty set

the carrier of V is non empty set

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of u is non empty set

W is left_complementable right_complementable complementable Element of the carrier of u

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. u is V55(u) 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

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

the carrier of V is non empty set

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. u is V55(u) 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

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. W is V55(W) left_complementable right_complementable complementable Element of the carrier of W

the carrier of W is non empty set

the ZeroF of W is left_complementable right_complementable complementable Element of the carrier of W

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

the carrier of V is non empty set

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

W is left_complementable right_complementable complementable Element of the carrier of V

u + W 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 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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of B is non empty set

C is left_complementable right_complementable complementable Element of the carrier of B

C is left_complementable right_complementable complementable Element of the carrier of B

C + C is left_complementable right_complementable complementable Element of the carrier of B

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

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

W * u is left_complementable right_complementable complementable Element of 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 . (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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of B is non empty set

C is left_complementable right_complementable complementable Element of the carrier of B

W * C is left_complementable right_complementable complementable Element of the carrier of B

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

- u is left_complementable right_complementable complementable Element of the carrier of V

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of W is non empty set

B is left_complementable right_complementable complementable Element of the carrier of W

- B is left_complementable right_complementable complementable Element of the carrier of W

(- 1) * u is left_complementable right_complementable complementable Element of 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),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

(- 1) * B is left_complementable right_complementable complementable Element of the carrier of W

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

W is left_complementable right_complementable complementable Element of the carrier of V

u - W is left_complementable right_complementable complementable Element of the carrier of V

- W is left_complementable right_complementable complementable Element of the carrier of V

u + (- W) 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 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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of B is non empty set

C is left_complementable right_complementable complementable Element of the carrier of B

C is left_complementable right_complementable complementable Element of the carrier of B

C - C is left_complementable right_complementable complementable Element of the carrier of B

- C is left_complementable right_complementable complementable Element of the carrier of B

C + (- C) is left_complementable right_complementable complementable Element of the carrier of B

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

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 left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

the carrier of W is non empty set

C is left_complementable right_complementable complementable Element of the carrier of V

c

C + c

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

[C,c

{C,c

{C} is non empty set

{{C,c

the addF of V . [C,c

C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of C is non empty set

x is left_complementable right_complementable complementable Element of the carrier of C

x is left_complementable right_complementable complementable Element of the carrier of C

x + x is left_complementable right_complementable complementable Element of the carrier of C

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

z is left_complementable right_complementable complementable Element of the carrier of W

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

c

C * c

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

[C,c

{C,c

{C} is non empty set

{{C,c

the Mult of V . [C,c

C is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of C is non empty set

x is left_complementable right_complementable complementable Element of the carrier of C

C * x is left_complementable right_complementable complementable Element of the carrier of C

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

x is left_complementable right_complementable complementable Element of the carrier of W

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

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 non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. u is V55(u) 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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. u is V55(u) 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

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

the carrier of V is non empty set

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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

u is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

0. u is V55(u) 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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

W is left_complementable right_complementable complementable Element of the carrier of V

u + W 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 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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

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

W * u is left_complementable right_complementable complementable Element of 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 . (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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

- u is left_complementable right_complementable complementable Element of the carrier of V

W is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

(- 1) * u is left_complementable right_complementable complementable Element of 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),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

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

u is left_complementable right_complementable complementable Element of the carrier of V

W is left_complementable right_complementable complementable Element of the carrier of V

u - W is left_complementable right_complementable complementable Element of the carrier of V

- W is left_complementable right_complementable complementable Element of the carrier of V

u + (- W) 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 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

B is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() (V)

V is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is V55(V) left_complementable right_complementable complementable Element of the carrier of V

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

the Mult of V | [:REAL,u:] is Relation-like Function-like 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:]

C is Relation-like [:REAL,W:] -defined W -valued Function-like V18([:REAL,W:],W) Element of bool [:[:REAL,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

x2 is left_complementable right_complementable complementable Element of the carrier of V

v1 is left_complementable right_complementable complementable Element of the carrier of V

x2 + v1 is left_complementable right_complementable complementable Element of the carrier of V

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

v1 + x2 is left_complementable right_complementable complementable Element of the carrier of V

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

b is left_complementable right_complementable complementable Element of the carrier of V

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

v1 is left_complementable right_complementable complementable Element of the carrier of V

v2 is left_complementable right_complementable complementable Element of the carrier of V

v1 + v2 is left_complementable right_complementable complementable Element of the carrier of V

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

v2 + b is left_complementable right_complementable complementable Element of the carrier of V

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 is left_complementable right_complementable complementable Element of the carrier of V

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

u1 is left_complementable right_complementable complementable Element of the carrier of V

x2 is left_complementable right_complementable complementable Element of the carrier of V

u1 + x2 is left_complementable right_complementable complementable Element of the carrier of V

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

- u1 is left_complementable right_complementable complementable Element of the carrier of V

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