:: RLTOPSP1 semantic presentation

REAL is non empty non finite set

bool REAL is non empty set
COMPLEX is non empty non finite set

bool NAT is non empty set
bool NAT is non empty set
is non empty set
bool is non empty set
RAT is non empty non finite set
INT is non empty non finite set

- 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 * 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 * b1) where b1 is Element of the carrier of V : b1 in v } 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
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
c5 is set
U is Element of bool the carrier of V
the carrier of V is non empty set
bool the carrier of V is non empty set
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
c5 is Element of the carrier of V
s + c5 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,c5) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set
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 + b1) where b1 is Element of the carrier of V : b1 in v } is set
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
{ (b1 + w) where b1 is Element of the carrier of V : b1 in v } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
c5 is set
U is Element of the carrier of V
U + w is Element of bool the carrier of V
the carrier of V is non empty set
bool the carrier of V is non empty set
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
{ (b1 + w) where b1 is Element of the carrier of V : b1 in v } is set
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
c5 is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set
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 + b1) where b1 is Element of the carrier of V : b1 in w } is set
c5 is set
U is set
W is Element of the carrier of V
W + w is Element of bool the carrier of V
{ (W + b1) where b1 is Element of the carrier of V : b1 in w } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set
c8 is Element of the carrier of V
W + c8 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,c8) is Element of the carrier of V

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) + b1) where b1 is Element of the carrier of V : b1 in v } is set
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
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 + b1) where b1 is Element of the carrier of V : b1 in w + s } is set
{ (w + b1) where b1 is Element of the carrier of V : b1 in s } is set
{ ((v + w) + b1) where b1 is Element of the carrier of V : b1 in s } is set
c5 is set
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
c5 is set
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
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 + b1) where b1 is Element of the carrier of V : b1 in w + s } is set
{ (v + b1) where b1 is Element of the carrier of V : b1 in w } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in w & b2 in s ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v + w & b2 in s ) } is set
c5 is set
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
c8 is Element of the carrier of V
v + c8 is Element of the carrier of V
the addF of V . (v,c8) is Element of the carrier of V
c8 + W is Element of the carrier of V
the addF of V . (c8,W) is Element of the carrier of V
v + (c8 + W) is Element of the carrier of V
the addF of V . (v,(c8 + W)) is Element of the carrier of V
c5 is set
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
c8 is Element of the carrier of V
W + c8 is Element of the carrier of V
the addF of V . (W,c8) is Element of the carrier of V
v + W is Element of the carrier of V
the addF of V . (v,W) is Element of the carrier of V
(v + W) + c8 is Element of the carrier of V
the addF of V . ((v + W),c8) is Element of the carrier of V
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
c5 is set
{ (s + b1) where b1 is Element of the carrier of V : b1 in v } is set
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

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
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
c5 is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in s ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in w & b2 in s ) } is set
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
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
c5 is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in s & b2 in v ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in s & b2 in w ) } is set
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
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
c5 is Element of bool the carrier of V
v + w is Element of bool the carrier of V
s + c5 is Element of bool the carrier of V
U is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in s & b2 in c5 ) } is set
W is Element of the carrier of V
c8 is Element of the carrier of V
W + c8 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,c8) is Element of the carrier of V
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
c5 is Element of the carrier of V
c5 + (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 . (c5,(0. V)) is Element of the carrier of V
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set

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 * {(0. V)} is Element of bool the carrier of V
{ (v * b1) where b1 is Element of the carrier of V : b1 in {(0. V)} } is set
w is set
s is Element of the carrier of V
c5 is Element of the carrier of V
v * c5 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,c5) is set
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

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 * b1) where b1 is Element of the carrier of V : b1 in v } is set
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

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 * b1) where b1 is Element of the carrier of V : b1 in v } is set
s * w is Element of bool the carrier of V
{ (s * b1) where b1 is Element of the carrier of V : b1 in w } is set
(s * v) /\ (s * w) is Element of bool the carrier of V
s * (v /\ w) is Element of bool the carrier of V
{ (s * b1) where b1 is Element of the carrier of V : b1 in v /\ w } is set
c5 is set
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
c5 is set
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

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
c5 * 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 . (c5,w) is set

(1 - c5) * s is Element of the carrier of V
the Mult of V . ((1 - c5),s) is set
(c5 * w) + ((1 - c5) * 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 . ((c5 * w),((1 - c5) * s)) is Element of the carrier of V
c5 * 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 . (c5,w) is set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V

(1 - c5) * s is Element of the carrier of V
the Mult of V . ((1 - c5),s) is set
(c5 * w) + ((1 - c5) * 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 . ((c5 * w),((1 - c5) * s)) is Element of the carrier of V

(1 - c5) * 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 - c5),s) is set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
c5 * w is Element of the carrier of V
the Mult of V . (c5,w) is set
(c5 * w) + ((1 - c5) * 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 . ((c5 * w),((1 - c5) * s)) is Element of the carrier of V
w is Element of the carrier of V
s is Element of the carrier of V

c5 * 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 . (c5,w) is set

(1 - c5) * s is Element of the carrier of V
the Mult of V . ((1 - c5),s) is set
(c5 * w) + ((1 - c5) * 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 . ((c5 * w),((1 - c5) * s)) is Element of 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

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 () is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
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 () is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
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 () is Element of bool the carrier of V

w * (conv v) is Element of bool the carrier of V
{ (w * b1) where b1 is Element of the carrier of V : b1 in conv v } is set
w * v is Element of bool the carrier of V
{ (w * b1) where b1 is Element of the carrier of V : b1 in v } is set
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
c5 is Element of the carrier of V
w * c5 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,c5) is set
U is set
W is Element of bool the carrier of V

(w ") * (w * v) is Element of bool the carrier of V
{ ((w ") * b1) where b1 is Element of the carrier of V : b1 in w * v } is set
(w ") * W is Element of bool the carrier of V
{ ((w ") * b1) where b1 is Element of the carrier of V : b1 in W } is set
(w ") * w is ext-real complex real Element of REAL
((w ") * w) * v is Element of bool the carrier of V
{ (((w ") * w) * b1) where b1 is Element of the carrier of V : b1 in v } is set
1 * v is Element of bool the carrier of V
{ (1 * b1) where b1 is Element of the carrier of V : b1 in v } is set
c8 is Element of the carrier of V
(w ") * c8 is Element of the carrier of V
the Mult of V . ((w "),c8) is set
w * (w ") is ext-real complex real Element of REAL
(w * (w ")) * c8 is Element of the carrier of V
the Mult of V . ((w * (w ")),c8) is set
1 * c8 is Element of the carrier of V
the Mult of V . (1,c8) is set

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
c5 is Element of bool the carrier of V

the carrier of V is non empty set
bool the carrier of V is non empty set
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 () 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 () is Element of bool the carrier of V
s is set

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 * v is Element of bool the carrier of V
{ (w * b1) where b1 is Element of the carrier of V : b1 in v } is set
s is set
c5 is Element of the carrier of V
w * c5 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,c5) is set

(1 - w) * (0. V) is Element of the carrier of V
the Mult of V . ((1 - w),(0. V)) is set
(w * c5) + ((1 - w) * (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 . ((w * c5),((1 - w) * (0. V))) is Element of the carrier of V
(w * c5) + (0. V) is Element of the carrier of V
the addF of V . ((w * c5),(0. V)) is Element of the carrier of V

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 - b1) * v) + (b1 * w)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
bool the carrier of V is non empty set
s is set

(1 - c5) * 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 . ((1 - c5),v) is set
c5 * w is Element of the carrier of V
the Mult of V . (c5,w) is set
((1 - c5) * v) + (c5 * 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 . (((1 - c5) * v),(c5 * w)) is Element of the carrier of V
s is Element of bool the carrier of V
c5 is Element of the carrier of V
U is Element of the carrier of V
{ (((1 - b1) * c5) + (b1 * U)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
{ (((1 - b1) * U) + (b1 * c5)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
W is set

(1 - c8) * c5 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 - c8),c5) is set
c8 * U is Element of the carrier of V
the Mult of V . (c8,U) is set
((1 - c8) * c5) + (c8 * 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 . (((1 - c8) * c5),(c8 * U)) is Element of the carrier of V
1 - (1 - c8) is ext-real complex real Element of REAL
1 - 0 is non empty ext-real positive non negative complex real Element of REAL
W is set

(1 - c8) * 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 - c8),U) is set
c8 * c5 is Element of the carrier of V
the Mult of V . (c8,c5) is set
((1 - c8) * U) + (c8 * c5) 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 - c8) * U),(c8 * c5)) is Element of the carrier of V
1 - (1 - c8) is ext-real complex real Element of REAL
1 - 0 is non empty ext-real positive non negative complex real Element of REAL

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 - b1) * v) + (b1 * w)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set
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
c5 is Element of the carrier of V

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

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

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

(1 - c8) * v is Element of the carrier of V
the Mult of V . ((1 - c8),v) is set
c8 * w is Element of the carrier of V
the Mult of V . (c8,w) is set
((1 - c8) * v) + (c8 * w) is Element of the carrier of V
the addF of V . (((1 - c8) * v),(c8 * w)) is Element of the carrier of V
(1 - U) * ((1 - c8) * v) is Element of the carrier of V
the Mult of V . ((1 - U),((1 - c8) * v)) is set
(1 - U) * (c8 * w) is Element of the carrier of V
the Mult of V . ((1 - U),(c8 * w)) is set
((1 - U) * ((1 - c8) * v)) + ((1 - U) * (c8 * w)) is Element of the carrier of V
the addF of V . (((1 - U) * ((1 - c8) * v)),((1 - U) * (c8 * w))) is Element of the carrier of V
(1 - U) * (1 - c8) is ext-real complex real Element of REAL
((1 - U) * (1 - c8)) * v is Element of the carrier of V
the Mult of V . (((1 - U) * (1 - c8)),v) is set
(((1 - U) * (1 - c8)) * v) + ((1 - U) * (c8 * w)) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c8)) * v),((1 - U) * (c8 * w))) is Element of the carrier of V
(1 - U) * c8 is ext-real complex real Element of REAL
((1 - U) * c8) * w is Element of the carrier of V
the Mult of V . (((1 - U) * c8),w) is set
(((1 - U) * (1 - c8)) * v) + (((1 - U) * c8) * w) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c8)) * v),(((1 - U) * c8) * w)) is Element of the carrier of V
((U * W) * w) + ((((1 - U) * (1 - c8)) * v) + (((1 - U) * c8) * w)) is Element of the carrier of V
the addF of V . (((U * W) * w),((((1 - U) * (1 - c8)) * v) + (((1 - U) * c8) * w))) is Element of the carrier of V
((U * (1 - W)) * v) + (((U * W) * w) + ((((1 - U) * (1 - c8)) * v) + (((1 - U) * c8) * w))) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),(((U * W) * w) + ((((1 - U) * (1 - c8)) * v) + (((1 - U) * c8) * w)))) is Element of the carrier of V
((U * W) * w) + (((1 - U) * c8) * w) is Element of the carrier of V
the addF of V . (((U * W) * w),(((1 - U) * c8) * w)) is Element of the carrier of V
(((1 - U) * (1 - c8)) * v) + (((U * W) * w) + (((1 - U) * c8) * w)) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c8)) * v),(((U * W) * w) + (((1 - U) * c8) * w))) is Element of the carrier of V
((U * (1 - W)) * v) + ((((1 - U) * (1 - c8)) * v) + (((U * W) * w) + (((1 - U) * c8) * w))) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),((((1 - U) * (1 - c8)) * v) + (((U * W) * w) + (((1 - U) * c8) * w)))) is Element of the carrier of V
((U * (1 - W)) * v) + (((1 - U) * (1 - c8)) * v) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),(((1 - U) * (1 - c8)) * v)) is Element of the carrier of V
(((U * (1 - W)) * v) + (((1 - U) * (1 - c8)) * v)) + (((U * W) * w) + (((1 - U) * c8) * w)) is Element of the carrier of V
the addF of V . ((((U * (1 - W)) * v) + (((1 - U) * (1 - c8)) * v)),(((U * W) * w) + (((1 - U) * c8) * w))) is Element of the carrier of V
(U * (1 - W)) + ((1 - U) * (1 - c8)) is ext-real complex real Element of REAL
((U * (1 - W)) + ((1 - U) * (1 - c8))) * v is Element of the carrier of V
the Mult of V . (((U * (1 - W)) + ((1 - U) * (1 - c8))),v) is set
(((U * (1 - W)) + ((1 - U) * (1 - c8))) * v) + (((U * W) * w) + (((1 - U) * c8) * w)) is Element of the carrier of V
the addF of V . ((((U * (1 - W)) + ((1 - U) * (1 - c8))) * v),(((U * W) * w) + (((1 - U) * c8) * w))) is Element of the carrier of V
(U * W) + ((1 - U) * c8) is ext-real complex real Element of REAL
1 - ((U * W) + ((1 - U) * c8)) is ext-real complex real Element of REAL
(1 - ((U * W) + ((1 - U) * c8))) * v is Element of the carrier of V
the Mult of V . ((1 - ((U * W) + ((1 - U) * c8))),v) is set
((U * W) + ((1 - U) * c8)) * w is Element of the carrier of V
the Mult of V . (((U * W) + ((1 - U) * c8)),w) is set
((1 - ((U * W) + ((1 - U) * c8))) * v) + (((U * W) + ((1 - U) * c8)) * w) is Element of the carrier of V
the addF of V . (((1 - ((U * W) + ((1 - U) * c8))) * v),(((U * W) + ((1 - U) * c8)) * w)) is Element of the carrier of V
((1 - U) * c8) + (U * W) is ext-real complex real Element of REAL

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
c5 is set
(V,w,s) is non empty convex Element of bool the carrier of V
{ (((1 - b1) * w) + (b1 * s)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is set

(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

c5 * 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 . (c5,w) is set

(1 - c5) * s is Element of the carrier of V
the Mult of V . ((1 - c5),s) is set
(c5 * w) + ((1 - c5) * 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 . ((c5 * w),((1 - c5) * s)) is Element of the carrier of V
(V,s,w) is non empty convex Element of bool the carrier of V
{ (((1 - b1) * s) + (b1 * w)) where b1 is ext-real complex real Element of REAL : ( 0 <= b1 & b1 <= 1 ) } is 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 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 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) * b1) where b1 is Element of the carrier of V : b1 in v } is set

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) * b1) where b1 is Element of the carrier of V : b1 in v } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in w & b2 in (- 1) * v ) } is set
{ (s + b1) where b1 is Element of the carrier of V : b1 in v } is set
c5 is set
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
c5 is Element of the carrier of V
U is Element of the carrier of V
c5 + U is Element of the carrier of V
the addF of V . (c5,U) is Element of the carrier of V
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
c5 + (U + W) is Element of the carrier of V
the addF of V . (c5,(U + W)) 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
c5 + (U + (- U)) is Element of the carrier of V
the addF of V . (c5,(U + (- U))) is Element of the carrier of V
c5 + (0. V) is Element of the carrier of V
the addF of V . (c5,(0. V)) is Element of 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

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) * b1) where b1 is Element of the carrier of V : b1 in v } is set

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) * b1) where b1 is Element of the carrier of V : b1 in v } is set
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

w * v is Element of bool the carrier of V
{ (w * b1) where b1 is Element of the carrier of V : b1 in v } is set

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 * {(0. V)} is Element of bool the carrier of V
{ (v * b1) where b1 is Element of the carrier of V : b1 in {(0. V)} } is set

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

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

0 * v is Element of bool the carrier of V
{ (0 * b1) where b1 is Element of the carrier of V : b1 in v } is set
{(0. V)} is non empty Element of bool the carrier of V

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
{ (b1 + b2) where b1, b2 is Element of the carrier of V : ( b1 in v & b2 in w ) } is set

s * (v + w) is Element of bool the carrier of V
{ (s * b1) where b1 is Element of the carrier of V : b1 in v + w } is set
s * v is Element of bool the carrier of V
{ (s * b1) where b1 is Element of the carrier of V : b1 in v } is set
s * w is Element of bool the carrier of V
{ (s * b1) where b1 is Element of the carrier of V : b1 in w } is set
c5 is set
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
c8 is Element of the carrier of V
W + c8 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,c8) is Element of the carrier of V
s * W is Element of the carrier of V
the Mult of V . (s,W) is set
s * c8 is Element of the carrier of V
the Mult of V . (s,c8) is set
(s * W) + (s * c8) is Element of the carrier of V
the addF of V . ((s * W),(s * c8)) is Element of the carrier of V

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