:: RUSUB_1 semantic presentation

REAL is non empty V36() V129() V130() V131() V135() set
NAT is V129() V130() V131() V132() V133() V134() V135() Element of bool REAL
bool REAL is non empty set
omega is V129() V130() V131() V132() V133() V134() V135() set
bool omega is non empty set
bool NAT is non empty set
is V119() V120() V121() set
bool is non empty set
COMPLEX is non empty V36() V129() V135() set
RAT is non empty V36() V129() V130() V131() V132() V135() set
INT is non empty V36() V129() V130() V131() V132() V133() V135() set
{} is Function-like functional empty V129() V130() V131() V132() V133() V134() V135() set
the Function-like functional empty V129() V130() V131() V132() V133() V134() V135() set is Function-like functional empty V129() V130() V131() V132() V133() V134() V135() set
1 is non empty ext-real natural V34() real V117() V118() V129() V130() V131() V132() V133() V134() Element of NAT

- 1 is ext-real V34() real Element of REAL

the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
the addF of V is Relation-like [: 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 scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like V18([: the carrier of V, the carrier of V:], REAL ) V119() V120() V121() Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of V, the carrier of V:],REAL:] 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
the scalar of V || the carrier of V is Relation-like Function-like set
the scalar of V | [: the carrier of V, the carrier of V:] is Relation-like Function-like V119() V120() V121() set
dom the scalar of V is Relation-like set
dom the addF of V is Relation-like set
dom the Mult of V is Relation-like set

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

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

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

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

the carrier of V is non empty set

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

the carrier of V is non empty set

the carrier of W is non empty set
u is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of W
C is ext-real V34() real Element of REAL
C * B is right_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 . (C,B) is set
[C,B] is set
{C,B} is non empty set
{C} is non empty V129() V130() V131() set
{{C,B},{C}} is non empty set
the Mult of W . [C,B] is set
C * u is right_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,u) is set
[C,u] is set
{C,u} is non empty set
{{C,u},{C}} is non empty set
the Mult of V . [C,u] is set
the Mult of V | [:REAL, the carrier of W:] is Relation-like Function-like set
[C,B] is Element of [:REAL, the carrier of W:]
( the Mult of V | [:REAL, the carrier of W:]) . [C,B] is set

the carrier of V is non empty set

the carrier of W is non empty set
u is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of V
u .|. B is ext-real V34() real Element of REAL
C is right_complementable Element of the carrier of W
C is right_complementable Element of the carrier of W
C .|. C is ext-real V34() real Element of REAL
[: the carrier of V, the carrier of V:] is non empty set
the scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like V18([: the carrier of V, the carrier of V:], REAL ) V119() V120() V121() Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty set
c7 is right_complementable Element of the carrier of V
x is right_complementable Element of the carrier of V
[c7,x] is Element of [: the carrier of V, the carrier of V:]
{c7,x} is non empty set
{c7} is non empty set
{{c7,x},{c7}} is non empty set
the scalar of V . [c7,x] is ext-real V34() real Element of REAL
[: the carrier of W, the carrier of W:] is non empty set
the scalar of W is Relation-like [: the carrier of W, the carrier of W:] -defined REAL -valued Function-like V18([: the carrier of W, the carrier of W:], REAL ) V119() V120() V121() Element of bool [:[: the carrier of W, the carrier of W:],REAL:]
[:[: the carrier of W, the carrier of W:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of W, the carrier of W:],REAL:] is non empty set
[C,C] is Element of [: the carrier of W, the carrier of W:]
{C,C} is non empty set
{C} is non empty set
{{C,C},{C}} is non empty set
the scalar of W . [C,C] is ext-real V34() real Element of REAL
the scalar of V || the carrier of W is Relation-like Function-like set
the scalar of V | [: the carrier of W, the carrier of W:] is Relation-like Function-like V119() V120() V121() set
( the scalar of V || the carrier of W) . [C,C] is set

the carrier of V is non empty set

the carrier of W is non empty set
u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
B is right_complementable Element of the carrier of W
- B is right_complementable Element of the carrier of W
(- 1) * u is right_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 V129() V130() V131() set
{{(- 1),u},{(- 1)}} is non empty set
the Mult of V . [(- 1),u] is set
(- 1) * B is right_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

the carrier of V is non empty set

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

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

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

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

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

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

the carrier of W is non empty set
u is Element of bool the carrier of V
c7 is ext-real V34() real Element of REAL
x is right_complementable Element of the carrier of V
c7 * x is right_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 . (c7,x) is set
[c7,x] is set
{c7,x} is non empty set
{c7} is non empty V129() V130() V131() set
{{c7,x},{c7}} is non empty set
the Mult of V . [c7,x] is set

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

the carrier of V is non empty set

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

the carrier of V is non empty set

bool the carrier of V is non empty set
the carrier of W is non empty set
B is right_complementable Element of the carrier of V
C is ext-real V34() real Element of REAL
C * B is right_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,B) is set
[C,B] is set
{C,B} is non empty set
{C} is non empty V129() V130() V131() set
{{C,B},{C}} is non empty set
the Mult of V . [C,B] is set
u is Element of bool the carrier of V

the carrier of V is non empty set

u is right_complementable Element of the carrier of V
- u is right_complementable Element of the carrier of V
(- 1) * u is right_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 V129() V130() V131() set
{{(- 1),u},{(- 1)}} is non empty set
the Mult of V . [(- 1),u] is set

the carrier of V is non empty set

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

the carrier of V is non empty set
bool the carrier of V is non empty set
0. V is V55(V) right_complementable Element of the carrier of V
the ZeroF of V is right_complementable Element of the carrier of V
the addF of V is Relation-like [: 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 scalar of V is Relation-like [: the carrier of V, the carrier of V:] -defined REAL -valued Function-like V18([: the carrier of V, the carrier of V:], REAL ) V119() V120() V121() Element of bool [:[: the carrier of V, the carrier of V:],REAL:]
[:[: the carrier of V, the carrier of V:],REAL:] is non empty V119() V120() V121() set
bool [:[: the carrier of V, the carrier of V:],REAL:] is non empty set
W is Element of bool the carrier of V
the addF of V || W is Relation-like Function-like set
[:W,W:] is set
the addF of V | [:W,W:] is Relation-like Function-like set
[:REAL,W:] is set

the scalar of V | [:W,W:] is Relation-like Function-like V119() V120() V121() set
u is non empty set
[:u,u:] is non empty set
[:[:u,u:],u:] is non empty set
bool [:[:u,u:],u:] is non empty set
[:REAL,u:] is non empty set
[:[:REAL,u:],u:] is non empty set
bool [:[:REAL,u:],u:] is non empty set
[:[:u,u:],REAL:] is non empty V119() V120() V121() set
bool [:[:u,u:],REAL:] is non empty set
B is Element of u
C is Relation-like [:u,u:] -defined u -valued Function-like V18([:u,u:],u) Element of bool [:[:u,u:],u:]

c7 is Relation-like [:u,u:] -defined REAL -valued Function-like V18([:u,u:], REAL ) V119() V120() V121() Element of bool [:[:u,u:],REAL:]
UNITSTR(# u,B,C,C,c7 #) is non empty strict UNITSTR
the carrier of UNITSTR(# u,B,C,C,c7 #) is non empty set
z is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
x is ext-real V34() real Element of REAL
x * z is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . (x,z) is set
[x,z] is set
{x,z} is non empty set
{x} is non empty V129() V130() V131() set
{{x,z},{x}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [x,z] is set
[x,z] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):]
the Mult of V . [x,z] is set
x is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
z is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
x .|. z is ext-real V34() real Element of REAL
[x,z] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
{x,z} is non empty set
{x} is non empty set
{{x,z},{x}} is non empty set
the scalar of V . [x,z] is ext-real V34() real set
the scalar of V || the carrier of UNITSTR(# u,B,C,C,c7 #) is Relation-like Function-like set
the scalar of V | [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is Relation-like Function-like V119() V120() V121() set
( the scalar of V || the carrier of UNITSTR(# u,B,C,C,c7 #)) . [x,z] is set
x is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
z is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
x + z is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) is Relation-like [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . (x,z) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[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 UNITSTR(# u,B,C,C,c7 #) . [x,z] is set
[x,z] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
the addF of V . [x,z] is set
W is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
1 * W is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . (1,W) is set
[1,W] is set
{1,W} is non empty set
{1} is non empty V129() V130() V131() V132() V133() V134() set
{{1,W},{1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [1,W] is set
x1 is right_complementable Element of the carrier of V
1 * x1 is right_complementable Element of the carrier of V
the Mult of V . (1,x1) is set
[1,x1] is set
{1,x1} is non empty set
{{1,x1},{1}} is non empty set
the Mult of V . [1,x1] is set
W is ext-real V34() real set
x1 is ext-real V34() real set
W * x1 is ext-real V34() real set
x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
(W * x1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . ((W * x1),x2) is set
[(W * x1),x2] is set
{(W * x1),x2} is non empty set
{(W * x1)} is non empty V129() V130() V131() set
{{(W * x1),x2},{(W * x1)}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [(W * x1),x2] is set
x1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (x1,x2) is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty V129() V130() V131() set
{{x1,x2},{x1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [x1,x2] is set
W * (x1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (W,(x1 * x2)) is set
[W,(x1 * x2)] is set
{W,(x1 * x2)} is non empty set
{W} is non empty V129() V130() V131() set
{{W,(x1 * x2)},{W}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [W,(x1 * x2)] is set
v2 is ext-real V34() real Element of REAL
z1 is ext-real V34() real Element of REAL
v2 * z1 is ext-real V34() real Element of REAL
(v2 * z1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . ((v2 * z1),x2) is set
[(v2 * z1),x2] is set
{(v2 * z1),x2} is non empty set
{(v2 * z1)} is non empty V129() V130() V131() set
{{(v2 * z1),x2},{(v2 * z1)}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [(v2 * z1),x2] is set
v1 is right_complementable Element of the carrier of V
(v2 * z1) * v1 is right_complementable Element of the carrier of V
the Mult of V . ((v2 * z1),v1) is set
[(v2 * z1),v1] is set
{(v2 * z1),v1} is non empty set
{{(v2 * z1),v1},{(v2 * z1)}} is non empty set
the Mult of V . [(v2 * z1),v1] is set
z1 * v1 is right_complementable Element of the carrier of V
the Mult of V . (z1,v1) is set
[z1,v1] is set
{z1,v1} is non empty set
{z1} is non empty V129() V130() V131() set
{{z1,v1},{z1}} is non empty set
the Mult of V . [z1,v1] is set
v2 * (z1 * v1) is right_complementable Element of the carrier of V
the Mult of V . (v2,(z1 * v1)) is set
[v2,(z1 * v1)] is set
{v2,(z1 * v1)} is non empty set
{v2} is non empty V129() V130() V131() set
{{v2,(z1 * v1)},{v2}} is non empty set
the Mult of V . [v2,(z1 * v1)] is set
z1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (z1,x2) is set
[z1,x2] is set
{z1,x2} is non empty set
{{z1,x2},{z1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [z1,x2] is set
[v2,(z1 * x2)] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):]
{v2,(z1 * x2)} is non empty set
{{v2,(z1 * x2)},{v2}} is non empty set
the Mult of V . [v2,(z1 * x2)] is set
v2 * (z1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (v2,(z1 * x2)) is set
[v2,(z1 * x2)] is set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [v2,(z1 * x2)] is set
W is ext-real V34() real set
x1 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
x1 + x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) is Relation-like [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . (x1,x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . [x1,x2] is set
W * (x1 + x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . (W,(x1 + x2)) is set
[W,(x1 + x2)] is set
{W,(x1 + x2)} is non empty set
{W} is non empty V129() V130() V131() set
{{W,(x1 + x2)},{W}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [W,(x1 + x2)] is set
W * x1 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (W,x1) is set
[W,x1] is set
{W,x1} is non empty set
{{W,x1},{W}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [W,x1] is set
W * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (W,x2) is set
[W,x2] is set
{W,x2} is non empty set
{{W,x2},{W}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [W,x2] is set
(W * x1) + (W * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) . ((W * x1),(W * x2)) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[(W * x1),(W * x2)] is set
{(W * x1),(W * x2)} is non empty set
{(W * x1)} is non empty set
{{(W * x1),(W * x2)},{(W * x1)}} is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . [(W * x1),(W * x2)] is set
z1 is ext-real V34() real Element of REAL
z1 * (x1 + x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (z1,(x1 + x2)) is set
[z1,(x1 + x2)] is set
{z1,(x1 + x2)} is non empty set
{z1} is non empty V129() V130() V131() set
{{z1,(x1 + x2)},{z1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [z1,(x1 + x2)] is set
[z1,(x1 + x2)] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):]
the Mult of V . [z1,(x1 + x2)] is set
v1 is right_complementable Element of the carrier of V
v2 is right_complementable Element of the carrier of V
v1 + v2 is right_complementable Element of the carrier of V
the addF of V . (v1,v2) is right_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
z1 * (v1 + v2) is right_complementable Element of the carrier of V
the Mult of V . (z1,(v1 + v2)) is set
[z1,(v1 + v2)] is set
{z1,(v1 + v2)} is non empty set
{{z1,(v1 + v2)},{z1}} is non empty set
the Mult of V . [z1,(v1 + v2)] is set
z1 * v1 is right_complementable Element of the carrier of V
the Mult of V . (z1,v1) is set
[z1,v1] is set
{z1,v1} is non empty set
{{z1,v1},{z1}} is non empty set
the Mult of V . [z1,v1] is set
z1 * v2 is right_complementable Element of the carrier of V
the Mult of V . (z1,v2) is set
[z1,v2] is set
{z1,v2} is non empty set
{{z1,v2},{z1}} is non empty set
the Mult of V . [z1,v2] is set
(z1 * v1) + (z1 * v2) is right_complementable Element of the carrier of V
the addF of V . ((z1 * v1),(z1 * v2)) is right_complementable Element of the carrier of V
[(z1 * v1),(z1 * v2)] is set
{(z1 * v1),(z1 * v2)} is non empty set
{(z1 * v1)} is non empty set
{{(z1 * v1),(z1 * v2)},{(z1 * v1)}} is non empty set
the addF of V . [(z1 * v1),(z1 * v2)] is set
[z1,v1] is Element of [:REAL, the carrier of V:]
the Mult of V . [z1,v1] is right_complementable Element of the carrier of V
z1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (z1,x2) is set
[z1,x2] is set
{z1,x2} is non empty set
{{z1,x2},{z1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [z1,x2] is set
[( the Mult of V . [z1,v1]),(z1 * x2)] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
{( the Mult of V . [z1,v1]),(z1 * x2)} is non empty set
{( the Mult of V . [z1,v1])} is non empty set
{{( the Mult of V . [z1,v1]),(z1 * x2)},{( the Mult of V . [z1,v1])}} is non empty set
the addF of V . [( the Mult of V . [z1,v1]),(z1 * x2)] is set
z1 * x1 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (z1,x1) is set
[z1,x1] is set
{z1,x1} is non empty set
{{z1,x1},{z1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [z1,x1] is set
[(z1 * x1),(z1 * x2)] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
{(z1 * x1),(z1 * x2)} is non empty set
{(z1 * x1)} is non empty set
{{(z1 * x1),(z1 * x2)},{(z1 * x1)}} is non empty set
the addF of V . [(z1 * x1),(z1 * x2)] is set
(z1 * x1) + (z1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) . ((z1 * x1),(z1 * x2)) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[(z1 * x1),(z1 * x2)] is set
the addF of UNITSTR(# u,B,C,C,c7 #) . [(z1 * x1),(z1 * x2)] is set
0. UNITSTR(# u,B,C,C,c7 #) is V55( UNITSTR(# u,B,C,C,c7 #)) Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the ZeroF of UNITSTR(# u,B,C,C,c7 #) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
W is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
W + (0. UNITSTR(# u,B,C,C,c7 #)) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) is Relation-like [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . (W,(0. UNITSTR(# u,B,C,C,c7 #))) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[W,(0. UNITSTR(# u,B,C,C,c7 #))] is set
{W,(0. UNITSTR(# u,B,C,C,c7 #))} is non empty set
{W} is non empty set
{{W,(0. UNITSTR(# u,B,C,C,c7 #))},{W}} is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . [W,(0. UNITSTR(# u,B,C,C,c7 #))] is set
x1 is right_complementable Element of the carrier of V
x1 + (0. V) is right_complementable Element of the carrier of V
the addF of V . (x1,(0. V)) is right_complementable Element of the carrier of V
[x1,(0. V)] is set
{x1,(0. V)} is non empty set
{x1} is non empty set
{{x1,(0. V)},{x1}} is non empty set
the addF of V . [x1,(0. V)] is set
W is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
W .|. W is ext-real V34() real Element of REAL
x1 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
W .|. x1 is ext-real V34() real Element of REAL
x1 .|. W is ext-real V34() real Element of REAL
W + x1 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) is Relation-like [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . (W,x1) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[W,x1] is set
{W,x1} is non empty set
{W} is non empty set
{{W,x1},{W}} is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . [W,x1] is set
x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
(W + x1) .|. x2 is ext-real V34() real Element of REAL
W .|. x2 is ext-real V34() real Element of REAL
x1 .|. x2 is ext-real V34() real Element of REAL
(W .|. x2) + (x1 .|. x2) is ext-real V34() real Element of REAL
a is ext-real V34() real Element of REAL
a * W is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . (a,W) is set
[a,W] is set
{a,W} is non empty set
{a} is non empty V129() V130() V131() set
{{a,W},{a}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [a,W] is set
(a * W) .|. x1 is ext-real V34() real Element of REAL
a * (W .|. x1) is ext-real V34() real Element of REAL
v2 is right_complementable Element of the carrier of V
v1 is right_complementable Element of the carrier of V
[v2,v1] is Element of [: the carrier of V, the carrier of V:]
{v2,v1} is non empty set
{v2} is non empty set
{{v2,v1},{v2}} is non empty set
the scalar of V . [v2,v1] is ext-real V34() real Element of REAL
v2 .|. v1 is ext-real V34() real Element of REAL
z1 is right_complementable Element of the carrier of V
z1 .|. z1 is ext-real V34() real Element of REAL
[z1,z1] is Element of [: the carrier of V, the carrier of V:]
{z1,z1} is non empty set
{z1} is non empty set
{{z1,z1},{z1}} is non empty set
the scalar of V . [z1,z1] is ext-real V34() real Element of REAL
z1 is right_complementable Element of the carrier of V
[z1,z1] is Element of [: the carrier of V, the carrier of V:]
{z1,z1} is non empty set
{z1} is non empty set
{{z1,z1},{z1}} is non empty set
the scalar of V . [z1,z1] is ext-real V34() real Element of REAL
z1 .|. z1 is ext-real V34() real Element of REAL
z1 is right_complementable Element of the carrier of V
z1 .|. z1 is ext-real V34() real Element of REAL
[z1,z1] is Element of [: the carrier of V, the carrier of V:]
{z1,z1} is non empty set
{z1} is non empty set
{{z1,z1},{z1}} is non empty set
the scalar of V . [z1,z1] is ext-real V34() real Element of REAL
[z1,v2] is Element of [: the carrier of V, the carrier of V:]
{z1,v2} is non empty set
{{z1,v2},{z1}} is non empty set
the scalar of V . [z1,v2] is ext-real V34() real Element of REAL
v2 .|. z1 is ext-real V34() real Element of REAL
[v2,z1] is Element of [: the carrier of V, the carrier of V:]
{v2,z1} is non empty set
{{v2,z1},{v2}} is non empty set
the scalar of V . [v2,z1] is ext-real V34() real Element of REAL
[(W + x1),x2] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
{(W + x1),x2} is non empty set
{(W + x1)} is non empty set
{{(W + x1),x2},{(W + x1)}} is non empty set
the scalar of V . [(W + x1),x2] is ext-real V34() real set
z1 + v2 is right_complementable Element of the carrier of V
the addF of V . (z1,v2) is right_complementable Element of the carrier of V
[z1,v2] is set
the addF of V . [z1,v2] is set
[(z1 + v2),x2] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
{(z1 + v2),x2} is non empty set
{(z1 + v2)} is non empty set
{{(z1 + v2),x2},{(z1 + v2)}} is non empty set
the scalar of V . [(z1 + v2),x2] is ext-real V34() real set
(z1 + v2) .|. v1 is ext-real V34() real Element of REAL
z1 .|. v1 is ext-real V34() real Element of REAL
(z1 .|. v1) + (v2 .|. v1) is ext-real V34() real Element of REAL
[W,x2] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
{W,x2} is non empty set
{{W,x2},{W}} is non empty set
the scalar of V . [W,x2] is ext-real V34() real set
( the scalar of V . [W,x2]) + (x1 .|. x2) is ext-real V34() real Element of REAL
[x1,x2] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
{x1,x2} is non empty set
{x1} is non empty set
{{x1,x2},{x1}} is non empty set
the scalar of V . [x1,x2] is ext-real V34() real set
( the scalar of V . [W,x2]) + ( the scalar of V . [x1,x2]) is ext-real V34() real set
[W,x1] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
the scalar of V . [W,x1] is ext-real V34() real set
a * ( the scalar of V . [W,x1]) is ext-real V34() real Element of REAL
z1 .|. v2 is ext-real V34() real Element of REAL
a * (z1 .|. v2) is ext-real V34() real Element of REAL
[(a * W),x1] is Element of [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):]
{(a * W),x1} is non empty set
{(a * W)} is non empty set
{{(a * W),x1},{(a * W)}} is non empty set
the scalar of V . [(a * W),x1] is ext-real V34() real set
a * z1 is right_complementable Element of the carrier of V
the Mult of V . (a,z1) is set
[a,z1] is set
{a,z1} is non empty set
{{a,z1},{a}} is non empty set
the Mult of V . [a,z1] is set
[(a * z1),x1] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):]
{(a * z1),x1} is non empty set
{(a * z1)} is non empty set
{{(a * z1),x1},{(a * z1)}} is non empty set
the scalar of V . [(a * z1),x1] is ext-real V34() real set
(a * z1) .|. v2 is ext-real V34() real Element of REAL
W is ext-real V34() real set
x1 is ext-real V34() real set
W + x1 is ext-real V34() real set
x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
(W + x1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) is Relation-like [:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . ((W + x1),x2) is set
[(W + x1),x2] is set
{(W + x1),x2} is non empty set
{(W + x1)} is non empty V129() V130() V131() set
{{(W + x1),x2},{(W + x1)}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [(W + x1),x2] is set
W * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (W,x2) is set
[W,x2] is set
{W,x2} is non empty set
{W} is non empty V129() V130() V131() set
{{W,x2},{W}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [W,x2] is set
x1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (x1,x2) is set
[x1,x2] is set
{x1,x2} is non empty set
{x1} is non empty V129() V130() V131() set
{{x1,x2},{x1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [x1,x2] is set
(W * x2) + (x1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the addF of UNITSTR(# u,B,C,C,c7 #) is Relation-like [: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] -defined the carrier of UNITSTR(# u,B,C,C,c7 #) -valued Function-like V18([: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #)) Element of bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
[:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
bool [:[: the carrier of UNITSTR(# u,B,C,C,c7 #), the carrier of UNITSTR(# u,B,C,C,c7 #):], the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . ((W * x2),(x1 * x2)) is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
[(W * x2),(x1 * x2)] is set
{(W * x2),(x1 * x2)} is non empty set
{(W * x2)} is non empty set
{{(W * x2),(x1 * x2)},{(W * x2)}} is non empty set
the addF of UNITSTR(# u,B,C,C,c7 #) . [(W * x2),(x1 * x2)] is set
v2 is ext-real V34() real Element of REAL
z1 is ext-real V34() real Element of REAL
v2 + z1 is ext-real V34() real Element of REAL
(v2 + z1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . ((v2 + z1),x2) is set
[(v2 + z1),x2] is set
{(v2 + z1),x2} is non empty set
{(v2 + z1)} is non empty V129() V130() V131() set
{{(v2 + z1),x2},{(v2 + z1)}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [(v2 + z1),x2] is set
v1 is right_complementable Element of the carrier of V
(v2 + z1) * v1 is right_complementable Element of the carrier of V
the Mult of V . ((v2 + z1),v1) is set
[(v2 + z1),v1] is set
{(v2 + z1),v1} is non empty set
{{(v2 + z1),v1},{(v2 + z1)}} is non empty set
the Mult of V . [(v2 + z1),v1] is set
v2 * v1 is right_complementable Element of the carrier of V
the Mult of V . (v2,v1) is set
[v2,v1] is set
{v2,v1} is non empty set
{v2} is non empty V129() V130() V131() set
{{v2,v1},{v2}} is non empty set
the Mult of V . [v2,v1] is set
z1 * v1 is right_complementable Element of the carrier of V
the Mult of V . (z1,v1) is set
[z1,v1] is set
{z1,v1} is non empty set
{z1} is non empty V129() V130() V131() set
{{z1,v1},{z1}} is non empty set
the Mult of V . [z1,v1] is set
(v2 * v1) + (z1 * v1) is right_complementable Element of the carrier of V
the addF of V . ((v2 * v1),(z1 * v1)) is right_complementable Element of the carrier of V
[(v2 * v1),(z1 * v1)] is set
{(v2 * v1),(z1 * v1)} is non empty set
{(v2 * v1)} is non empty set
{{(v2 * v1),(z1 * v1)},{(v2 * v1)}} is non empty set
the addF of V . [(v2 * v1),(z1 * v1)] is set
[v2,v1] is Element of [:REAL, the carrier of V:]
the Mult of V . [v2,v1] is right_complementable Element of the carrier of V
z1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c7 #)
the Mult of UNITSTR(# u,B,C,C,c7 #) . (z1,x2) is set
[z1,x2] is set
{z1,x2} is non empty set
{{z1,x2},{z1}} is non empty set
the Mult of UNITSTR(# u,B,C,C,c7 #) . [z1,x2] is set
[( the Mult of V . [v2,v1]),(z1 * x2)] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):]
[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c7 #):] is non empty set
{( the Mult of V . [v2,v1]),(z1 * x2)} is non empty set
{( the Mult of V .