:: RLTOPSP1 semantic presentation

REAL is non empty non finite set

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

bool REAL is non empty set

COMPLEX is non empty non finite set

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

bool NAT is non empty set

bool NAT is non empty set

[:NAT,REAL:] is non empty set

bool [:NAT,REAL:] is non empty set

RAT is non empty non finite set

INT is non empty non finite set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real Element of NAT

{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real set

the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real Element of NAT

union {} is epsilon-transitive epsilon-connected ordinal set

0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of NAT

- 1 is non empty ext-real non positive negative complex real Element of REAL

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

w is Element of the carrier of V

v is Element of bool the carrier of V

s is ext-real complex real Element of REAL

s * w is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (s,w) is set

s * v is Element of bool the carrier of V

{ (s * b

V is non empty TopSpace-like TopStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

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

v is non empty Element of bool the carrier of V

w is Element of bool (bool the carrier of V)

union w is Element of bool the carrier of V

s is Element of the carrier of V

c

U is Element of bool the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

v + w is Element of bool the carrier of V

s is Element of the carrier of V

c

s + c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (s,c

{ (b

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

s is Element of the carrier of V

w is Element of the carrier of V

w + s is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (w,s) is Element of the carrier of V

w + v is Element of bool the carrier of V

{ (w + b

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

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

w is Element of bool the carrier of V

v is Element of bool the carrier of V

{ (b

bool the carrier of V is non empty Element of bool (bool the carrier of V)

c

U is Element of the carrier of V

U + w is Element of bool the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

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

w is Element of bool the carrier of V

v is Element of bool the carrier of V

{ (b

v + w is Element of bool the carrier of V

s is Element of bool (bool the carrier of V)

union s is Element of bool the carrier of V

c

{ (b

U is Element of the carrier of V

W is Element of the carrier of V

U + W is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (U,W) is Element of the carrier of V

U + w is Element of bool the carrier of V

{ (U + b

c

U is set

W is Element of the carrier of V

W + w is Element of bool the carrier of V

{ (W + b

{ (b

c

W + c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (W,c

V is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v is Element of bool the carrier of V

(0. V) + v is Element of bool the carrier of V

{ ((0. V) + b

w is set

s is Element of the carrier of V

(0. V) + s is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . ((0. V),s) is Element of the carrier of V

w is set

s is Element of the carrier of V

(0. V) + s is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . ((0. V),s) is Element of the carrier of V

V is non empty add-associative addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

v + w is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (v,w) is Element of the carrier of V

s is Element of bool the carrier of V

(v + w) + s is Element of bool the carrier of V

w + s is Element of bool the carrier of V

v + (w + s) is Element of bool the carrier of V

{ (v + b

{ (w + b

{ ((v + w) + b

c

U is Element of the carrier of V

(v + w) + U is Element of the carrier of V

the addF of V . ((v + w),U) is Element of the carrier of V

w + U is Element of the carrier of V

the addF of V . (w,U) is Element of the carrier of V

v + (w + U) is Element of the carrier of V

the addF of V . (v,(w + U)) is Element of the carrier of V

c

U is Element of the carrier of V

v + U is Element of the carrier of V

the addF of V . (v,U) is Element of the carrier of V

W is Element of the carrier of V

w + W is Element of the carrier of V

the addF of V . (w,W) is Element of the carrier of V

(v + w) + W is Element of the carrier of V

the addF of V . ((v + w),W) is Element of the carrier of V

V is non empty add-associative addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of the carrier of V

w is Element of bool the carrier of V

v + w is Element of bool the carrier of V

s is Element of bool the carrier of V

(v + w) + s is Element of bool the carrier of V

w + s is Element of bool the carrier of V

v + (w + s) is Element of bool the carrier of V

{ (v + b

{ (v + b

{ (b

{ (b

c

U is Element of the carrier of V

W is Element of the carrier of V

U + W is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (U,W) is Element of the carrier of V

c

v + c

the addF of V . (v,c

c

the addF of V . (c

v + (c

the addF of V . (v,(c

c

U is Element of the carrier of V

v + U is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (v,U) is Element of the carrier of V

W is Element of the carrier of V

c

W + c

the addF of V . (W,c

v + W is Element of the carrier of V

the addF of V . (v,W) is Element of the carrier of V

(v + W) + c

the addF of V . ((v + W),c

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

s is Element of the carrier of V

s + v is Element of bool the carrier of V

s + w is Element of bool the carrier of V

c

{ (s + b

U is Element of the carrier of V

W is Element of the carrier of V

s + W is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (s,W) is Element of the carrier of V

V is non empty right_complementable add-associative right_zeroed addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v is Element of bool the carrier of V

w is Element of the carrier of V

- w is Element of the carrier of V

(- w) + v is Element of bool the carrier of V

(- w) + w is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . ((- w),w) is Element of the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

s is Element of bool the carrier of V

v + s is Element of bool the carrier of V

w + s is Element of bool the carrier of V

c

{ (b

{ (b

U is Element of the carrier of V

W is Element of the carrier of V

U + W is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (U,W) is Element of the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

s is Element of bool the carrier of V

s + v is Element of bool the carrier of V

s + w is Element of bool the carrier of V

c

{ (b

{ (b

U is Element of the carrier of V

W is Element of the carrier of V

U + W is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (U,W) is Element of the carrier of V

V is non empty addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

s is Element of bool the carrier of V

w is Element of bool the carrier of V

c

v + w is Element of bool the carrier of V

s + c

U is set

{ (b

{ (b

W is Element of the carrier of V

c

W + c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (W,c

V is non empty right_zeroed addLoopStr

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

w is Element of bool the carrier of V

v is Element of bool the carrier of V

v + w is Element of bool the carrier of V

s is set

c

c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

{ (b

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

the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty Element of bool the carrier of V

bool the carrier of V is non empty set

v is ext-real complex real Element of REAL

v * {(0. V)} is Element of bool the carrier of V

{ (v * b

w is set

s is Element of the carrier of V

c

v * c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (v,c

v * (0. V) is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (v,(0. V)) is set

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

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v is Element of bool the carrier of V

w is non empty ext-real complex real Element of REAL

w * v is Element of bool the carrier of V

{ (w * b

w * (0. V) is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]

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

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

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

the Mult of V . (w,(0. V)) is set

s is Element of the carrier of V

w * s is Element of the carrier of V

the Mult of V . (w,s) is set

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

v /\ w is Element of bool the carrier of V

s is non empty ext-real complex real Element of REAL

s * v is Element of bool the carrier of V

{ (s * b

s * w is Element of bool the carrier of V

{ (s * b

(s * v) /\ (s * w) is Element of bool the carrier of V

s * (v /\ w) is Element of bool the carrier of V

{ (s * b

c

U is Element of the carrier of V

s * U is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (s,U) is set

W is Element of the carrier of V

s * W is Element of the carrier of V

the Mult of V . (s,W) is set

c

U is Element of the carrier of V

s * U is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (s,U) is set

V is non empty TopSpace-like TopStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of the carrier of V

w is non empty a_neighborhood of v

s is Element of bool the carrier of V

Int w is open Element of bool the carrier of V

Int s is open Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

c

w is Element of the carrier of V

s is Element of the carrier of V

c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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

1 - c

(1 - c

the Mult of V . ((1 - c

(c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

1 - c

(1 - c

the Mult of V . ((1 - c

(c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

1 - c

(1 - c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 - c

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

c

the Mult of V . (c

(c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

w is Element of the carrier of V

s is Element of the carrier of V

c

c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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

1 - c

(1 - c

the Mult of V . ((1 - c

(c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

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

{} V is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of bool the carrier of V

the carrier of V is non empty set

bool the carrier of V is non empty set

conv ({} V) is convex Element of bool the carrier of V

Convex-Family ({} V) is non empty Element of bool (bool the carrier of V)

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

meet (Convex-Family ({} V)) is Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of bool the carrier of V

conv v is convex Element of bool the carrier of V

Convex-Family v is non empty Element of bool (bool the carrier of V)

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

meet (Convex-Family v) is Element of bool the carrier of V

{} V is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is convex Element of bool the carrier of V

conv v is convex Element of bool the carrier of V

Convex-Family v is non empty Element of bool (bool the carrier of V)

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

meet (Convex-Family v) is Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

conv v is convex Element of bool the carrier of V

Convex-Family v is non empty Element of bool (bool the carrier of V)

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

meet (Convex-Family v) is Element of bool the carrier of V

w is ext-real complex real Element of REAL

w * (conv v) is Element of bool the carrier of V

{ (w * b

w * v is Element of bool the carrier of V

{ (w * b

conv (w * v) is convex Element of bool the carrier of V

Convex-Family (w * v) is non empty Element of bool (bool the carrier of V)

meet (Convex-Family (w * v)) is Element of bool the carrier of V

s is set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty Element of bool the carrier of V

c

w * c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]

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

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

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

the Mult of V . (w,c

U is set

W is Element of bool the carrier of V

w " is ext-real complex real Element of REAL

(w ") * (w * v) is Element of bool the carrier of V

{ ((w ") * b

(w ") * W is Element of bool the carrier of V

{ ((w ") * b

(w ") * w is ext-real complex real Element of REAL

((w ") * w) * v is Element of bool the carrier of V

{ (((w ") * w) * b

1 * v is Element of bool the carrier of V

{ (1 * b

c

(w ") * c

the Mult of V . ((w "),c

w * (w ") is ext-real complex real Element of REAL

(w * (w ")) * c

the Mult of V . ((w * (w ")),c

1 * c

the Mult of V . (1,c

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

Convex-Family w is non empty Element of bool (bool the carrier of V)

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

Convex-Family v is non empty Element of bool (bool the carrier of V)

s is set

c

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

conv v is convex Element of bool the carrier of V

Convex-Family v is non empty Element of bool (bool the carrier of V)

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

meet (Convex-Family v) is Element of bool the carrier of V

conv w is convex Element of bool the carrier of V

Convex-Family w is non empty Element of bool (bool the carrier of V)

meet (Convex-Family w) is Element of bool the carrier of V

s is set

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

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v is convex Element of bool the carrier of V

w is ext-real complex real Element of REAL

w * v is Element of bool the carrier of V

{ (w * b

s is set

c

w * c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]

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

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

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

the Mult of V . (w,c

1 - w is ext-real complex real Element of REAL

(1 - w) * (0. V) is Element of the carrier of V

the Mult of V . ((1 - w),(0. V)) is set

(w * c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . ((w * c

(w * c

the addF of V . ((w * c

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

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

{ (((1 - b

bool the carrier of V is non empty set

s is set

c

1 - c

(1 - c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 - c

c

the Mult of V . (c

((1 - c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (((1 - c

s is Element of bool the carrier of V

c

U is Element of the carrier of V

{ (((1 - b

{ (((1 - b

W is set

c

1 - c

(1 - c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 - c

c

the Mult of V . (c

((1 - c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (((1 - c

1 - (1 - c

1 - 0 is non empty ext-real positive non negative complex real Element of REAL

W is set

c

1 - c

(1 - c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 - c

c

the Mult of V . (c

((1 - c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (((1 - c

1 - (1 - c

1 - 0 is non empty ext-real positive non negative complex real Element of REAL

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

the carrier of V is non empty set

v is Element of the carrier of V

w is Element of the carrier of V

(V,v,w) is Element of bool the carrier of V

bool the carrier of V is non empty set

{ (((1 - b

0 * w is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total Element of bool [:[:REAL, the carrier of V:], the carrier of V:]

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

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

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

the Mult of V . (0,w) is set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v + (0. V) is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (v,(0. V)) is Element of the carrier of V

1 - 0 is non empty ext-real positive non negative complex real Element of REAL

1 * v is Element of the carrier of V

the Mult of V . (1,v) is set

s is Element of the carrier of V

c

U is ext-real complex real Element of REAL

U * s is Element of the carrier of V

the Mult of V . (U,s) is set

1 - U is ext-real complex real Element of REAL

(1 - U) * c

the Mult of V . ((1 - U),c

(U * s) + ((1 - U) * c

the addF of V . ((U * s),((1 - U) * c

W is ext-real complex real Element of REAL

1 - W is ext-real complex real Element of REAL

(1 - W) * v is Element of the carrier of V

the Mult of V . ((1 - W),v) is set

W * w is Element of the carrier of V

the Mult of V . (W,w) is set

((1 - W) * v) + (W * w) is Element of the carrier of V

the addF of V . (((1 - W) * v),(W * w)) is Element of the carrier of V

U * ((1 - W) * v) is Element of the carrier of V

the Mult of V . (U,((1 - W) * v)) is set

U * (W * w) is Element of the carrier of V

the Mult of V . (U,(W * w)) is set

(U * ((1 - W) * v)) + (U * (W * w)) is Element of the carrier of V

the addF of V . ((U * ((1 - W) * v)),(U * (W * w))) is Element of the carrier of V

U * (1 - W) is ext-real complex real Element of REAL

(U * (1 - W)) * v is Element of the carrier of V

the Mult of V . ((U * (1 - W)),v) is set

((U * (1 - W)) * v) + (U * (W * w)) is Element of the carrier of V

the addF of V . (((U * (1 - W)) * v),(U * (W * w))) is Element of the carrier of V

U * W is ext-real complex real Element of REAL

(U * W) * w is Element of the carrier of V

the Mult of V . ((U * W),w) is set

((U * (1 - W)) * v) + ((U * W) * w) is Element of the carrier of V

the addF of V . (((U * (1 - W)) * v),((U * W) * w)) is Element of the carrier of V

c

1 - c

(1 - c

the Mult of V . ((1 - c

c

the Mult of V . (c

((1 - c

the addF of V . (((1 - c

(1 - U) * ((1 - c

the Mult of V . ((1 - U),((1 - c

(1 - U) * (c

the Mult of V . ((1 - U),(c

((1 - U) * ((1 - c

the addF of V . (((1 - U) * ((1 - c

(1 - U) * (1 - c

((1 - U) * (1 - c

the Mult of V . (((1 - U) * (1 - c

(((1 - U) * (1 - c

the addF of V . ((((1 - U) * (1 - c

(1 - U) * c

((1 - U) * c

the Mult of V . (((1 - U) * c

(((1 - U) * (1 - c

the addF of V . ((((1 - U) * (1 - c

((U * W) * w) + ((((1 - U) * (1 - c

the addF of V . (((U * W) * w),((((1 - U) * (1 - c

((U * (1 - W)) * v) + (((U * W) * w) + ((((1 - U) * (1 - c

the addF of V . (((U * (1 - W)) * v),(((U * W) * w) + ((((1 - U) * (1 - c

((U * W) * w) + (((1 - U) * c

the addF of V . (((U * W) * w),(((1 - U) * c

(((1 - U) * (1 - c

the addF of V . ((((1 - U) * (1 - c

((U * (1 - W)) * v) + ((((1 - U) * (1 - c

the addF of V . (((U * (1 - W)) * v),((((1 - U) * (1 - c

((U * (1 - W)) * v) + (((1 - U) * (1 - c

the addF of V . (((U * (1 - W)) * v),(((1 - U) * (1 - c

(((U * (1 - W)) * v) + (((1 - U) * (1 - c

the addF of V . ((((U * (1 - W)) * v) + (((1 - U) * (1 - c

(U * (1 - W)) + ((1 - U) * (1 - c

((U * (1 - W)) + ((1 - U) * (1 - c

the Mult of V . (((U * (1 - W)) + ((1 - U) * (1 - c

(((U * (1 - W)) + ((1 - U) * (1 - c

the addF of V . ((((U * (1 - W)) + ((1 - U) * (1 - c

(U * W) + ((1 - U) * c

1 - ((U * W) + ((1 - U) * c

(1 - ((U * W) + ((1 - U) * c

the Mult of V . ((1 - ((U * W) + ((1 - U) * c

((U * W) + ((1 - U) * c

the Mult of V . (((U * W) + ((1 - U) * c

((1 - ((U * W) + ((1 - U) * c

the addF of V . (((1 - ((U * W) + ((1 - U) * c

((1 - U) * c

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of the carrier of V

s is Element of the carrier of V

c

(V,w,s) is non empty convex Element of bool the carrier of V

{ (((1 - b

U is ext-real complex real Element of REAL

1 - U is ext-real complex real Element of REAL

(1 - U) * w is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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),w) is set

U * s is Element of the carrier of V

the Mult of V . (U,s) is set

((1 - U) * w) + (U * s) is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (((1 - U) * w),(U * s)) is Element of the carrier of V

w is Element of the carrier of V

s is Element of the carrier of V

c

c

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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

1 - c

(1 - c

the Mult of V . ((1 - c

(c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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

(V,s,w) is non empty convex Element of bool the carrier of V

{ (((1 - b

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

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

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

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

{} V is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of bool the carrier of V

{({} V)} is non empty Element of bool (bool the carrier of V)

v is Element of bool (bool the carrier of V)

w is Element of bool the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

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

v is (V) Element of bool (bool the carrier of V)

meet v is Element of bool the carrier of V

w is Element of bool the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

(- 1) * v is Element of bool the carrier of V

{ ((- 1) * b

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

w is Element of bool the carrier of V

(V,v) is Element of bool the carrier of V

(- 1) * v is Element of bool the carrier of V

{ ((- 1) * b

w + (V,v) is Element of bool the carrier of V

s is Element of the carrier of V

s + v is Element of bool the carrier of V

w + ((- 1) * v) is Element of bool the carrier of V

{ (b

{ (s + b

c

U is Element of the carrier of V

s + U is Element of the carrier of V

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total 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 . (s,U) is Element of the carrier of V

(- 1) * U is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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

W is Element of the carrier of V

W + ((- 1) * U) is Element of the carrier of V

the addF of V . (W,((- 1) * U)) is Element of the carrier of V

U + ((- 1) * U) is Element of the carrier of V

the addF of V . (U,((- 1) * U)) is Element of the carrier of V

s + (U + ((- 1) * U)) is Element of the carrier of V

the addF of V . (s,(U + ((- 1) * U))) is Element of the carrier of V

- U is Element of the carrier of V

U + (- U) is Element of the carrier of V

the addF of V . (U,(- U)) is Element of the carrier of V

s + (U + (- U)) is Element of the carrier of V

the addF of V . (s,(U + (- U))) is Element of the carrier of V

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

s + (0. V) is Element of the carrier of V

the addF of V . (s,(0. V)) is Element of the carrier of V

c

U is Element of the carrier of V

c

the addF of V . (c

W is Element of the carrier of V

(- 1) * W is Element of the carrier of V

the Mult of V . ((- 1),W) is set

(- 1) * U is Element of the carrier of V

the Mult of V . ((- 1),U) is set

(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL

((- 1) * (- 1)) * W is Element of the carrier of V

the Mult of V . (((- 1) * (- 1)),W) is set

s + W is Element of the carrier of V

the addF of V . (s,W) is Element of the carrier of V

U + W is Element of the carrier of V

the addF of V . (U,W) is Element of the carrier of V

c

the addF of V . (c

- U is Element of the carrier of V

U + (- U) is Element of the carrier of V

the addF of V . (U,(- U)) is Element of the carrier of V

c

the addF of V . (c

c

the addF of V . (c

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

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

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty Element of bool the carrier of V

v is non empty Element of bool the carrier of V

(V,v) is Element of bool the carrier of V

(- 1) * v is Element of bool the carrier of V

{ ((- 1) * b

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is (V) Element of bool the carrier of V

w is Element of the carrier of V

- w is Element of the carrier of V

(V,v) is Element of bool the carrier of V

(- 1) * v is Element of bool the carrier of V

{ ((- 1) * b

s is Element of the carrier of V

(- 1) * s is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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),s) is set

(- 1) * w is Element of the carrier of V

the Mult of V . ((- 1),w) is set

(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL

((- 1) * (- 1)) * s is Element of the carrier of V

the Mult of V . (((- 1) * (- 1)),s) is set

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

V is non empty RLSStruct

the carrier of V is non empty set

bool the carrier of V is non empty set

v is Element of bool the carrier of V

{} V is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real Element of bool the carrier of V

w is ext-real complex real Element of REAL

abs w is ext-real complex real Element of REAL

w * v is Element of bool the carrier of V

{ (w * b

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

the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty Element of bool the carrier of V

bool the carrier of V is non empty set

v is ext-real complex real Element of REAL

abs v is ext-real complex real Element of REAL

v * {(0. V)} is Element of bool the carrier of V

{ (v * b

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

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

{(0. V)} is non empty Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

0. V is zero Element of the carrier of V

the ZeroF of V is Element of the carrier of V

v is non empty (V) Element of bool the carrier of V

abs 0 is ext-real complex real Element of REAL

0 * v is Element of bool the carrier of V

{ (0 * b

{(0. V)} is non empty Element of bool the carrier of V

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

the carrier of V is non empty set

bool the carrier of V is non empty set

v is (V) Element of bool the carrier of V

w is (V) Element of bool the carrier of V

v + w is Element of bool the carrier of V

{ (b

s is ext-real complex real Element of REAL

abs s is ext-real complex real Element of REAL

s * (v + w) is Element of bool the carrier of V

{ (s * b

s * v is Element of bool the carrier of V

{ (s * b

s * w is Element of bool the carrier of V

{ (s * b

c

U is Element of the carrier of V

s * U is Element of the carrier of V

the Mult of V is non empty Relation-like [:REAL, the carrier of V:] -defined the carrier of V -valued Function-like V17([:REAL, the carrier of V:]) quasi_total 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 . (s,U) is set

W is Element of the carrier of V

c

W + c

the addF of V is non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of V -valued Function-like V17([: the carrier of V, the carrier of V:]) quasi_total Element of bool [:[: the carrier of V, the carrier of V:], the carrier of V:]

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

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

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

the addF of V . (W,c

s * W is Element of the carrier of V

the Mult of V . (s,W) is set

s * c

the Mult of V . (s,c

(s * W) + (s * c

the addF of V . ((s * W),(s * c

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

the carrier of V is non empty set

bool the carrier of V is non empty