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

[:NAT,REAL:] is V119() V120() V121() set

bool [:NAT,REAL:] 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

0 is Function-like functional empty ext-real natural V34() real V117() V118() V129() V130() V131() V132() V133() V134() V135() Element of NAT

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

u is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

B is set

the carrier of W is non empty set

the carrier of u is non empty set

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

u is set

the carrier of W is non empty set

the carrier of V is non empty set

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

the carrier of W is non empty set

u is right_complementable Element of the carrier of W

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (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. 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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (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

u is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

c

x is right_complementable Element of the carrier of V

[c

{c

{c

{{c

the scalar of V . [c

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

u is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (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. 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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

bool the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

the carrier of W is non empty set

u is Element of bool the carrier of V

c

x is right_complementable Element of the carrier of V

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

the Mult of V . [c

C is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of C is non empty set

x is right_complementable Element of the carrier of C

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

[c

{c

{{c

the Mult of C . [c

z is right_complementable Element of the carrier of W

c

x is right_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 is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

W is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like (V)

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

V is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RealUnitarySpace-like UNITSTR

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

the scalar of V || W is Relation-like Function-like 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:]

C is Relation-like [:REAL,u:] -defined u -valued Function-like V18([:REAL,u:],u) Element of bool [:[:REAL,u:],u:]

c

UNITSTR(# u,B,C,C,c

the carrier of UNITSTR(# u,B,C,C,c

z is Element of the carrier of UNITSTR(# u,B,C,C,c

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

x * z is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[x,z] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c

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

x is Element of the carrier of UNITSTR(# u,B,C,C,c

z is Element of the carrier of UNITSTR(# u,B,C,C,c

x .|. z is ext-real V34() real Element of REAL

[x,z] is Element of [: the carrier of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

{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,c

the scalar of V | [: the carrier of UNITSTR(# u,B,C,C,c

( the scalar of V || the carrier of UNITSTR(# u,B,C,C,c

x is Element of the carrier of UNITSTR(# u,B,C,C,c

z is Element of the carrier of UNITSTR(# u,B,C,C,c

x + z is Element of the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

[:[: the carrier of UNITSTR(# u,B,C,C,c

bool [:[: the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,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 UNITSTR(# u,B,C,C,c

[x,z] is Element of [: the carrier of UNITSTR(# u,B,C,C,c

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

W is Element of the carrier of UNITSTR(# u,B,C,C,c

1 * W is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

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

(W * x1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[(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,c

x1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

W * (x1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

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

the Mult of UNITSTR(# u,B,C,C,c

[(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,c

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

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[v2,(z1 * x2)] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c

{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,c

the Mult of UNITSTR(# u,B,C,C,c

[v2,(z1 * x2)] is set

the Mult of UNITSTR(# u,B,C,C,c

W is ext-real V34() real set

x1 is Element of the carrier of UNITSTR(# u,B,C,C,c

x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

x1 + x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

[:[: the carrier of UNITSTR(# u,B,C,C,c

bool [:[: the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[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,c

W * (x1 + x2) is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

W * x1 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

W * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

(W * x1) + (W * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[(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,c

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

z1 * (x1 + x2) is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[z1,(x1 + x2)] is Element of [:REAL, the carrier of UNITSTR(# u,B,C,C,c

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

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[( the Mult of V . [z1,v1]),(z1 * x2)] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c

[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c

{( 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,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[(z1 * x1),(z1 * x2)] is Element of [: the carrier of UNITSTR(# u,B,C,C,c

{(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,c

the addF of UNITSTR(# u,B,C,C,c

[(z1 * x1),(z1 * x2)] is set

the addF of UNITSTR(# u,B,C,C,c

0. UNITSTR(# u,B,C,C,c

the ZeroF of UNITSTR(# u,B,C,C,c

W is Element of the carrier of UNITSTR(# u,B,C,C,c

W + (0. UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

[:[: the carrier of UNITSTR(# u,B,C,C,c

bool [:[: the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[W,(0. UNITSTR(# u,B,C,C,c

{W,(0. UNITSTR(# u,B,C,C,c

{W} is non empty set

{{W,(0. UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

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

W .|. W is ext-real V34() real Element of REAL

x1 is Element of the carrier of UNITSTR(# u,B,C,C,c

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

the addF of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

[:[: the carrier of UNITSTR(# u,B,C,C,c

bool [:[: the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[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,c

x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

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

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

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

{(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,c

[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c

{(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,c

{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,c

{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,c

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

{(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,c

{(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,c

(W + x1) * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[:REAL, the carrier of UNITSTR(# u,B,C,C,c

[:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

bool [:[:REAL, the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[(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,c

W * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

x1 * x2 is Element of the carrier of UNITSTR(# u,B,C,C,c

the Mult of UNITSTR(# u,B,C,C,c

[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,c

(W * x2) + (x1 * x2) is Element of the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[: the carrier of UNITSTR(# u,B,C,C,c

[:[: the carrier of UNITSTR(# u,B,C,C,c

bool [:[: the carrier of UNITSTR(# u,B,C,C,c

the addF of UNITSTR(# u,B,C,C,c

[(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,c

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

the Mult of UNITSTR(# u,B,C,C,c

[(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,c

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

the Mult of UNITSTR(# u,B,C,C,c

[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,c

[( the Mult of V . [v2,v1]),(z1 * x2)] is Element of [: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c

[: the carrier of V, the carrier of UNITSTR(# u,B,C,C,c

{( the Mult of V . [v2,v1]),(z1 * x2)} is non empty set

{( the Mult of V .