:: 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₁) where b₁ is Element of the carrier of V : b₁ 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
c₅ is set
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₅ is Element of the carrier of V
s + c₅ 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,c₅) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in w ) } is set
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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
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₁ + w) where b₁ is Element of the carrier of V : b₁ in v } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
c₅ is set
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₁ + w) where b₁ is Element of the carrier of V : b₁ 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
c₅ is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ 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 + b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
c₅ is set
U is set
W is Element of the carrier of V
W + w is Element of bool the carrier of V
{ (W + b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in w ) } is set
c₈ is Element of the carrier of V
W + c₈ 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,c₈) 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
(0. V) + v is Element of bool the carrier of V
{ ((0. V) + b₁) where b₁ is Element of the carrier of V : b₁ 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
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₁) where b₁ is Element of the carrier of V : b₁ in w + s } is set
{ (w + b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
{ ((v + w) + b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
c₅ 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
c₅ 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
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₁) where b₁ is Element of the carrier of V : b₁ in w + s } is set
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in w & b₂ in s ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v + w & b₂ in s ) } is set
c₅ 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
c₈ is Element of the carrier of V
v + c₈ is Element of the carrier of V
the addF of V . (v,c₈) is Element of the carrier of V
c₈ + W is Element of the carrier of V
the addF of V . (c₈,W) is Element of the carrier of V
v + (c₈ + W) is Element of the carrier of V
the addF of V . (v,(c₈ + W)) is Element of the carrier of V
c₅ 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
c₈ is Element of the carrier of V
W + c₈ is Element of the carrier of V
the addF of V . (W,c₈) 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) + c₈ is Element of the carrier of V
the addF of V . ((v + W),c₈) 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 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₅ is set
{ (s + b₁) where b₁ is Element of the carrier of V : b₁ 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
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₅ is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in s ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in w & b₂ 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
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₅ is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in s & b₂ in v ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in s & b₂ 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
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₅ is Element of bool the carrier of V
v + w is Element of bool the carrier of V
s + c₅ is Element of bool the carrier of V
U is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in w ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in s & b₂ in c₅ ) } is set
W is Element of the carrier of V
c₈ is Element of the carrier of V
W + c₈ 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,c₈) 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
c₅ is Element of the carrier of V
c₅ + (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 . (c₅,(0. V)) is Element of the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in w ) } 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
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₁) where b₁ is Element of the carrier of V : b₁ in {(0. V)} } is set
w is set
s is Element of the carrier of V
c₅ is Element of the carrier of V
v * c₅ 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,c₅) 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
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₁) where b₁ is Element of the carrier of V : b₁ 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
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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
s * w is Element of bool the carrier of V
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ 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 * b₁) where b₁ is Element of the carrier of V : b₁ in v /\ w } is set
c₅ 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
c₅ 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
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₅ is ext-real complex real Element of REAL
w is Element of the carrier of V
s is Element of the carrier of V
c₅ * 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 . (c₅,w) is set
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * s is Element of the carrier of V
the Mult of V . ((1 - c₅),s) is set
(c₅ * w) + ((1 - c₅) * 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 . ((c₅ * w),((1 - c₅) * s)) is Element of the carrier of V
c₅ * 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 . (c₅,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 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * s is Element of the carrier of V
the Mult of V . ((1 - c₅),s) is set
(c₅ * w) + ((1 - c₅) * 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 . ((c₅ * w),((1 - c₅) * s)) is Element of the carrier of V
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * 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 - c₅),s) is set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
c₅ * w is Element of the carrier of V
the Mult of V . (c₅,w) is set
(c₅ * w) + ((1 - c₅) * 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 . ((c₅ * w),((1 - c₅) * 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₅ is ext-real complex real Element of REAL
c₅ * 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 . (c₅,w) is set
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * s is Element of the carrier of V
the Mult of V . ((1 - c₅),s) is set
(c₅ * w) + ((1 - c₅) * 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 . ((c₅ * w),((1 - c₅) * s)) is Element of 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
{} 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₁) where b₁ is Element of the carrier of V : b₁ in conv v } is set
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ 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
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
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₁) where b₁ is Element of the carrier of V : b₁ in w * v } is set
(w ") * W is Element of bool the carrier of V
{ ((w ") * b₁) where b₁ is Element of the carrier of V : b₁ 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) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 * v is Element of bool the carrier of V
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
c₈ is Element of the carrier of V
(w ") * c₈ is Element of the carrier of V
the Mult of V . ((w "),c₈) is set
w * (w ") is ext-real complex real Element of REAL
(w * (w ")) * c₈ is Element of the carrier of V
the Mult of V . ((w * (w ")),c₈) is set
1 * c₈ is Element of the carrier of V
the Mult of V . (1,c₈) 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
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₅ 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
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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
s is set
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
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₅) + ((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 * c₅),((1 - w) * (0. V))) is Element of the carrier of V
(w * c₅) + (0. V) is Element of the carrier of V
the addF of V . ((w * c₅),(0. V)) is Element of 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
v is Element of the carrier of V
w is Element of the carrier of V
{ (((1 - b₁) * v) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
bool the carrier of V is non empty set
s is set
c₅ is ext-real complex real Element of REAL
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * 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 - c₅),v) is set
c₅ * w is Element of the carrier of V
the Mult of V . (c₅,w) is set
((1 - c₅) * v) + (c₅ * 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 - c₅) * v),(c₅ * w)) is Element of the carrier of V
s is Element of bool the carrier of V
c₅ is Element of the carrier of V
U is Element of the carrier of V
{ (((1 - b₁) * c₅) + (b₁ * U)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{ (((1 - b₁) * U) + (b₁ * c₅)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
W is set
c₈ is ext-real complex real Element of REAL
1 - c₈ is ext-real complex real Element of REAL
(1 - c₈) * c₅ 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 - c₈),c₅) is set
c₈ * U is Element of the carrier of V
the Mult of V . (c₈,U) is set
((1 - c₈) * c₅) + (c₈ * 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 - c₈) * c₅),(c₈ * U)) is Element of the carrier of V
1 - (1 - c₈) 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
c₈ is ext-real complex real Element of REAL
1 - c₈ is ext-real complex real Element of REAL
(1 - c₈) * 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 - c₈),U) is set
c₈ * c₅ is Element of the carrier of V
the Mult of V . (c₈,c₅) is set
((1 - c₈) * U) + (c₈ * c₅) 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 - c₈) * U),(c₈ * c₅)) is Element of the carrier of V
1 - (1 - c₈) is ext-real complex real Element of REAL
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₁) * v) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 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
c₅ is Element of the carrier of V
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₅ is Element of the carrier of V
the Mult of V . ((1 - U),c₅) is set
(U * s) + ((1 - U) * c₅) is Element of the carrier of V
the addF of V . ((U * s),((1 - U) * c₅)) is Element of the carrier of V
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₈ is ext-real complex real Element of REAL
1 - c₈ is ext-real complex real Element of REAL
(1 - c₈) * v is Element of the carrier of V
the Mult of V . ((1 - c₈),v) is set
c₈ * w is Element of the carrier of V
the Mult of V . (c₈,w) is set
((1 - c₈) * v) + (c₈ * w) is Element of the carrier of V
the addF of V . (((1 - c₈) * v),(c₈ * w)) is Element of the carrier of V
(1 - U) * ((1 - c₈) * v) is Element of the carrier of V
the Mult of V . ((1 - U),((1 - c₈) * v)) is set
(1 - U) * (c₈ * w) is Element of the carrier of V
the Mult of V . ((1 - U),(c₈ * w)) is set
((1 - U) * ((1 - c₈) * v)) + ((1 - U) * (c₈ * w)) is Element of the carrier of V
the addF of V . (((1 - U) * ((1 - c₈) * v)),((1 - U) * (c₈ * w))) is Element of the carrier of V
(1 - U) * (1 - c₈) is ext-real complex real Element of REAL
((1 - U) * (1 - c₈)) * v is Element of the carrier of V
the Mult of V . (((1 - U) * (1 - c₈)),v) is set
(((1 - U) * (1 - c₈)) * v) + ((1 - U) * (c₈ * w)) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c₈)) * v),((1 - U) * (c₈ * w))) is Element of the carrier of V
(1 - U) * c₈ is ext-real complex real Element of REAL
((1 - U) * c₈) * w is Element of the carrier of V
the Mult of V . (((1 - U) * c₈),w) is set
(((1 - U) * (1 - c₈)) * v) + (((1 - U) * c₈) * w) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c₈)) * v),(((1 - U) * c₈) * w)) is Element of the carrier of V
((U * W) * w) + ((((1 - U) * (1 - c₈)) * v) + (((1 - U) * c₈) * w)) is Element of the carrier of V
the addF of V . (((U * W) * w),((((1 - U) * (1 - c₈)) * v) + (((1 - U) * c₈) * w))) is Element of the carrier of V
((U * (1 - W)) * v) + (((U * W) * w) + ((((1 - U) * (1 - c₈)) * v) + (((1 - U) * c₈) * w))) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),(((U * W) * w) + ((((1 - U) * (1 - c₈)) * v) + (((1 - U) * c₈) * w)))) is Element of the carrier of V
((U * W) * w) + (((1 - U) * c₈) * w) is Element of the carrier of V
the addF of V . (((U * W) * w),(((1 - U) * c₈) * w)) is Element of the carrier of V
(((1 - U) * (1 - c₈)) * v) + (((U * W) * w) + (((1 - U) * c₈) * w)) is Element of the carrier of V
the addF of V . ((((1 - U) * (1 - c₈)) * v),(((U * W) * w) + (((1 - U) * c₈) * w))) is Element of the carrier of V
((U * (1 - W)) * v) + ((((1 - U) * (1 - c₈)) * v) + (((U * W) * w) + (((1 - U) * c₈) * w))) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),((((1 - U) * (1 - c₈)) * v) + (((U * W) * w) + (((1 - U) * c₈) * w)))) is Element of the carrier of V
((U * (1 - W)) * v) + (((1 - U) * (1 - c₈)) * v) is Element of the carrier of V
the addF of V . (((U * (1 - W)) * v),(((1 - U) * (1 - c₈)) * v)) is Element of the carrier of V
(((U * (1 - W)) * v) + (((1 - U) * (1 - c₈)) * v)) + (((U * W) * w) + (((1 - U) * c₈) * w)) is Element of the carrier of V
the addF of V . ((((U * (1 - W)) * v) + (((1 - U) * (1 - c₈)) * v)),(((U * W) * w) + (((1 - U) * c₈) * w))) is Element of the carrier of V
(U * (1 - W)) + ((1 - U) * (1 - c₈)) is ext-real complex real Element of REAL
((U * (1 - W)) + ((1 - U) * (1 - c₈))) * v is Element of the carrier of V
the Mult of V . (((U * (1 - W)) + ((1 - U) * (1 - c₈))),v) is set
(((U * (1 - W)) + ((1 - U) * (1 - c₈))) * v) + (((U * W) * w) + (((1 - U) * c₈) * w)) is Element of the carrier of V
the addF of V . ((((U * (1 - W)) + ((1 - U) * (1 - c₈))) * v),(((U * W) * w) + (((1 - U) * c₈) * w))) is Element of the carrier of V
(U * W) + ((1 - U) * c₈) is ext-real complex real Element of REAL
1 - ((U * W) + ((1 - U) * c₈)) is ext-real complex real Element of REAL
(1 - ((U * W) + ((1 - U) * c₈))) * v is Element of the carrier of V
the Mult of V . ((1 - ((U * W) + ((1 - U) * c₈))),v) is set
((U * W) + ((1 - U) * c₈)) * w is Element of the carrier of V
the Mult of V . (((U * W) + ((1 - U) * c₈)),w) is set
((1 - ((U * W) + ((1 - U) * c₈))) * v) + (((U * W) + ((1 - U) * c₈)) * w) is Element of the carrier of V
the addF of V . (((1 - ((U * W) + ((1 - U) * c₈))) * v),(((U * W) + ((1 - U) * c₈)) * w)) is Element of the carrier of V
((1 - U) * c₈) + (U * W) is ext-real 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
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₅ is set
(V,w,s) is non empty convex Element of bool the carrier of V
{ (((1 - b₁) * w) + (b₁ * s)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
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₅ is ext-real complex real Element of REAL
c₅ * 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 . (c₅,w) is set
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * s is Element of the carrier of V
the Mult of V . ((1 - c₅),s) is set
(c₅ * w) + ((1 - c₅) * 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 . ((c₅ * w),((1 - c₅) * s)) is Element of the carrier of V
(V,s,w) is non empty convex Element of bool the carrier of V
{ (((1 - b₁) * s) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 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 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₁) where b₁ is Element of the carrier of V : b₁ in 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
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₁) where b₁ is Element of the carrier of V : b₁ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in w & b₂ in (- 1) * v ) } is set
{ (s + b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
c₅ 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
c₅ is Element of the carrier of V
U is Element of the carrier of V
c₅ + U is Element of the carrier of V
the addF of V . (c₅,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
c₅ + (U + W) is Element of the carrier of V
the addF of V . (c₅,(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
c₅ + (U + (- U)) is Element of the carrier of V
the addF of V . (c₅,(U + (- U))) is Element of the carrier of V
c₅ + (0. V) is Element of the carrier of V
the addF of V . (c₅,(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
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₁) where b₁ is Element of the carrier of V : b₁ in 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
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₁) where b₁ is Element of the carrier of V : b₁ 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
{} 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₁) where b₁ is Element of the carrier of V : b₁ in 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
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₁) where b₁ is Element of the carrier of V : b₁ in {(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
{(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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
{(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₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in w ) } is set
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₁) where b₁ is Element of the carrier of V : b₁ in v + w } is set
s * v is Element of bool the carrier of V
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
s * w is Element of bool the carrier of V
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
c₅ 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
c₈ is Element of the carrier of V
W + c₈ 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,c₈) 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 * c₈ is Element of the carrier of V
the Mult of V . (s,c₈) is set
(s * W) + (s * c₈) is Element of the carrier of V
the addF of V . ((s * W),(s * c₈)) is Element of 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
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 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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
s is set
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
- w is ext-real complex real Element of REAL
(- 1) * c₅ is Element of the carrier of V
the Mult of V . ((- 1),c₅) is set
(- 1) * ((- 1) * c₅) is Element of the carrier of V
the Mult of V . ((- 1),((- 1) * c₅)) is set
(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL
((- 1) * (- 1)) * c₅ is Element of the carrier of V
the Mult of V . (((- 1) * (- 1)),c₅) 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 (V) Element of bool the carrier of V
abs (- 1) is ext-real complex real Element of REAL
- (- 1) is non empty ext-real positive non negative complex real Element of REAL
(V,v) is Element of bool the carrier of V
(- 1) * v is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in 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
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 (V) (V) 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
abs w is ext-real complex real Element of REAL
w * (conv v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in conv v } is set
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ 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
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) (V) 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 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 (V) 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)
union v is 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 * (union v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in union v } is set
s is set
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
U is set
W is Element of bool the carrier of V
w * W is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in W } 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 (V) Element of bool (bool the carrier of V)
meet v is 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 * (meet v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in meet v } is set
s is set
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
U is set
W is Element of bool the carrier of V
w * W is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in W } is set
V is non empty set
[:V,V:] is non empty set
[:[:V,V:],V:] is non empty set
bool [:[:V,V:],V:] is non empty set
[:REAL,V:] is non empty set
[:[:REAL,V:],V:] is non empty set
bool [:[:REAL,V:],V:] is non empty set
bool V is non empty set
bool (bool V) is non empty set
v is Element of V
w is non empty Relation-like [:V,V:] -defined V -valued Function-like V17([:V,V:]) quasi_total Element of bool [:[:V,V:],V:]
s is non empty Relation-like [:REAL,V:] -defined V -valued Function-like V17([:REAL,V:]) quasi_total Element of bool [:[:REAL,V:],V:]
c₅ is Element of bool (bool V)
(V,v,w,s,c₅) is () ()
{0} is non empty Element of bool NAT
[:{0},{0}:] is non empty set
[:[:{0},{0}:],{0}:] is non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
the non empty Relation-like [:{0},{0}:] -defined {0} -valued Function-like V17([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:] is non empty Relation-like [:{0},{0}:] -defined {0} -valued Function-like V17([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:]
[:REAL,{0}:] is non empty set
[:[:REAL,{0}:],{0}:] is non empty set
bool [:[:REAL,{0}:],{0}:] is non empty set
the non empty Relation-like [:REAL,{0}:] -defined {0} -valued Function-like V17([:REAL,{0}:]) quasi_total Element of bool [:[:REAL,{0}:],{0}:] is non empty Relation-like [:REAL,{0}:] -defined {0} -valued Function-like V17([:REAL,{0}:]) quasi_total Element of bool [:[:REAL,{0}:],{0}:]
v is Element of {0}
bool {0} is non empty Element of bool (bool {0})
bool {0} is non empty set
bool (bool {0}) is non empty set
{} (bool {0}) 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 (bool {0})
bool (bool {0}) is non empty set
({0},v, the non empty Relation-like [:{0},{0}:] -defined {0} -valued Function-like V17([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:], the non empty Relation-like [:REAL,{0}:] -defined {0} -valued Function-like V17([:REAL,{0}:]) quasi_total Element of bool [:[:REAL,{0}:],{0}:],({} (bool {0}))) is non empty () ()
c₅ is non empty () ()
the carrier of c₅ is non empty set
{0} is non empty Element of bool NAT
{{},{0}} is non empty set
bool {0} is non empty Element of bool (bool {0})
bool {0} is non empty set
bool (bool {0}) is non empty set
w is set
s is Element of {0}
[:{0},{0}:] is non empty set
[:[:{0},{0}:],{0}:] is non empty set
bool [:[:{0},{0}:],{0}:] is non empty set
c₅ is non empty Relation-like [:{0},{0}:] -defined {0} -valued Function-like V17([:{0},{0}:]) quasi_total Element of bool [:[:{0},{0}:],{0}:]
[:REAL,{0}:] is non empty set
[:[:REAL,{0}:],{0}:] is non empty set
bool [:[:REAL,{0}:],{0}:] is non empty set
U is non empty Relation-like [:REAL,{0}:] -defined {0} -valued Function-like V17([:REAL,{0}:]) quasi_total Element of bool [:[:REAL,{0}:],{0}:]
w is Element of bool (bool {0})
({0},s,c₅,U,w) is non empty () ()
W is non empty () ()
the carrier of W is non empty set
bool the carrier of W is non empty set
{s} is non empty Element of bool {0}
a is Element of the carrier of W
a is Element of the carrier of W
a + a is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (a,a) is Element of the carrier of W
v is Element of bool the carrier of W
c₈ is Element of bool the carrier of W
Y is Element of bool the carrier of W
c₈ + Y is Element of bool the carrier of W
the carrier of W is non empty set
bool the carrier of W is non empty set
{s} is non empty Element of bool {0}
Y is ext-real complex real Element of REAL
a is Element of the carrier of W
Y * a is Element of the carrier of W
the Mult of W is non empty Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V17([:REAL, the carrier of W:]) quasi_total Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . (Y,a) is set
a is Element of bool the carrier of W
c₈ is Element of bool the carrier of W
v is ext-real complex real Element of REAL
v - Y is ext-real complex real Element of REAL
abs (v - Y) is ext-real complex real Element of REAL
v * c₈ is Element of bool the carrier of W
{ (v * b₁) where b₁ is Element of the carrier of W : b₁ in c₈ } is set
the carrier of W is non empty set
the topology of W is open Element of bool (bool the carrier of W)
bool the carrier of W is non empty set
bool (bool the carrier of W) is non empty set
c₈ is Element of bool (bool the carrier of W)
{{}} is non empty set
{{0}} is non empty Element of bool (bool NAT)
bool (bool NAT) is non empty set
union c₈ is Element of bool the carrier of W
{} \/ {0} is non empty set
c₈ is Element of bool the carrier of W
Y is Element of bool the carrier of W
c₈ /\ Y is Element of bool the carrier of W
the carrier of W is non empty set
c₈ is Element of the carrier of W
Y is Element of the carrier of W
c₈ + Y is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (c₈,Y) is Element of the carrier of W
Y + c₈ is Element of the carrier of W
the addF of W . (Y,c₈) is Element of the carrier of W
a is Element of {0}
a is Element of {0}
c₈ is Element of the carrier of W
Y is Element of the carrier of W
c₈ + Y is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (c₈,Y) is Element of the carrier of W
a is Element of the carrier of W
(c₈ + Y) + a is Element of the carrier of W
the addF of W . ((c₈ + Y),a) is Element of the carrier of W
Y + a is Element of the carrier of W
the addF of W . (Y,a) is Element of the carrier of W
c₈ + (Y + a) is Element of the carrier of W
the addF of W . (c₈,(Y + a)) is Element of the carrier of W
a is Element of {0}
v is Element of {0}
a is Element of {0}
0. W is zero Element of the carrier of W
the ZeroF of W is Element of the carrier of W
c₈ is Element of the carrier of W
c₈ + (0. W) is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (c₈,(0. W)) is Element of the carrier of W
Y is Element of {0}
Y is Element of the carrier of W
c₈ is Element of the carrier of W
Y + c₈ is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (Y,c₈) is Element of the carrier of W
c₈ is ext-real complex real set
a is Element of the carrier of W
a is Element of the carrier of W
a + a is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . (a,a) is Element of the carrier of W
c₈ * (a + a) is Element of the carrier of W
the Mult of W is non empty Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V17([:REAL, the carrier of W:]) quasi_total Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . (c₈,(a + a)) is set
c₈ * a is Element of the carrier of W
the Mult of W . (c₈,a) is set
c₈ * a is Element of the carrier of W
the Mult of W . (c₈,a) is set
(c₈ * a) + (c₈ * a) is Element of the carrier of W
the addF of W . ((c₈ * a),(c₈ * a)) is Element of the carrier of W
Y is ext-real complex real Element of REAL
Y * a is Element of the carrier of W
the Mult of W . (Y,a) is set
Y * a is Element of the carrier of W
the Mult of W . (Y,a) is set
(Y * a) + (Y * a) is Element of the carrier of W
the addF of W . ((Y * a),(Y * a)) is Element of the carrier of W
v is Element of {0}
a is Element of {0}
U . (Y,H₁(v,a)) is Element of {0}
c₅ . (a,a) is set
U . (Y,(c₅ . (a,a))) is set
c₈ is ext-real complex real set
Y is ext-real complex real set
c₈ + Y is ext-real complex real set
a is Element of the carrier of W
(c₈ + Y) * a is Element of the carrier of W
the Mult of W is non empty Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V17([:REAL, the carrier of W:]) quasi_total Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . ((c₈ + Y),a) is set
c₈ * a is Element of the carrier of W
the Mult of W . (c₈,a) is set
Y * a is Element of the carrier of W
the Mult of W . (Y,a) is set
(c₈ * a) + (Y * a) is Element of the carrier of W
the addF of W is non empty Relation-like [: the carrier of W, the carrier of W:] -defined the carrier of W -valued Function-like V17([: the carrier of W, the carrier of W:]) quasi_total Element of bool [:[: the carrier of W, the carrier of W:], the carrier of W:]
[: the carrier of W, the carrier of W:] is non empty set
[:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
bool [:[: the carrier of W, the carrier of W:], the carrier of W:] is non empty set
the addF of W . ((c₈ * a),(Y * a)) is Element of the carrier of W
a is ext-real complex real Element of REAL
v is ext-real complex real Element of REAL
a + v is ext-real complex real Element of REAL
(a + v) * a is Element of the carrier of W
the Mult of W . ((a + v),a) is set
y is Element of {0}
c₈ is ext-real complex real set
Y is ext-real complex real set
c₈ * Y is ext-real complex real set
a is Element of the carrier of W
(c₈ * Y) * a is Element of the carrier of W
the Mult of W is non empty Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V17([:REAL, the carrier of W:]) quasi_total Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . ((c₈ * Y),a) is set
Y * a is Element of the carrier of W
the Mult of W . (Y,a) is set
c₈ * (Y * a) is Element of the carrier of W
the Mult of W . (c₈,(Y * a)) is set
a is ext-real complex real Element of REAL
v is ext-real complex real Element of REAL
a * v is ext-real complex real Element of REAL
(a * v) * a is Element of the carrier of W
the Mult of W . ((a * v),a) is set
y is Element of {0}
Y is Element of the carrier of W
1 * Y is Element of the carrier of W
the Mult of W is non empty Relation-like [:REAL, the carrier of W:] -defined the carrier of W -valued Function-like V17([:REAL, the carrier of W:]) quasi_total Element of bool [:[:REAL, the carrier of W:], the carrier of W:]
[:REAL, the carrier of W:] is non empty set
[:[:REAL, the carrier of W:], the carrier of W:] is non empty set
bool [:[:REAL, the carrier of W:], the carrier of W:] is non empty set
the Mult of W . (1,Y) is set
c₈ is ext-real complex real Element of REAL
a is Element of {0}
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 non empty a_neighborhood of v + w
Int s is open Element of bool the carrier of V
bool the carrier of V is non empty set
c₅ is Element of bool the carrier of V
U is Element of bool the carrier of V
c₅ + U is Element of bool the carrier of V
Int U is open Element of bool the carrier of V
Int c₅ is open Element of bool the carrier of V
c₈ is non empty a_neighborhood of v
W is non empty a_neighborhood of w
c₈ + W is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is ext-real complex real Element of REAL
w is Element of the carrier of V
v * 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 . (v,w) is set
s is non empty a_neighborhood of v * w
Int s is open Element of bool the carrier of V
bool the carrier of V is non empty set
U is Element of bool the carrier of V
c₅ is non empty ext-real positive non negative complex real Element of REAL
Int U is open Element of bool the carrier of V
W is non empty a_neighborhood of w
c₈ is ext-real complex real Element of REAL
c₈ - v is ext-real complex real Element of REAL
abs (c₈ - v) is ext-real complex real Element of REAL
c₈ * W is Element of bool the carrier of V
{ (c₈ * b₁) where b₁ is Element of the carrier of V : b₁ in W } is set
V is non empty ()
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
v is Element of the carrier of V
w is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
s is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
c₅ is Element of the carrier of V
s . c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
w is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
s is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
c₅ is Element of the carrier of V
w . c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
s . c₅ is Element of the carrier of V
V is non empty ()
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
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
w is Element of bool the carrier of V
(V,v) .: w is Element of bool the carrier of V
v + w is Element of bool the carrier of V
s is set
c₅ is Element of the carrier of V
(V,v) . c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
s is set
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
(V,v) . c₅ is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
bool the carrier of V is non empty set
v is Element of the carrier of V
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
rng (V,v) is Element of bool the carrier of V
w is set
- v is Element of the carrier of V
s is Element of the carrier of V
(- 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:], 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),s) is Element of the carrier of V
(V,v) . ((- v) + s) is Element of the carrier of V
v + ((- v) + s) is Element of the carrier of V
the addF of V . (v,((- v) + s)) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
(v + (- v)) + s is Element of the carrier of V
the addF of V . ((v + (- v)),s) 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
(0. V) + s is Element of the carrier of V
the addF of V . ((0. V),s) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
w is set
s is set
(V,v) . w is set
(V,v) . s is set
c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
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
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
(V,v) " is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
- v is Element of the carrier of V
(V,(- v)) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
rng (V,v) is Element of bool the carrier of V
bool the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
dom (V,v) is Element of bool the carrier of V
w is Element of the carrier of V
s is set
(V,v) . s is set
c₅ is Element of the carrier of V
v + c₅ 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:], 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,c₅) is Element of the carrier of V
((V,v) ") . w is Element of the carrier of V
(V,v) " is Relation-like Function-like set
((V,v) ") . w 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) + c₅ is Element of the carrier of V
the addF of V . ((0. V),c₅) is Element of the carrier of V
(- v) + v is Element of the carrier of V
the addF of V . ((- v),v) is Element of the carrier of V
((- v) + v) + c₅ is Element of the carrier of V
the addF of V . (((- v) + v),c₅) 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,(- v)) . w is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
bool the carrier of V is non empty set
w is TopStruct
the carrier of w is set
bool the carrier of w is non empty set
s is Element of bool the carrier of V
bool (bool the carrier of w) is non empty set
c₅ is Element of bool (bool the carrier of w)
bool (bool the carrier of V) is non empty set
U is Element of bool (bool the carrier of V)
union U is Element of bool the carrier of V
(V,v) " s is Element of bool the carrier of V
W is set
c₈ is set
Y is Element of the carrier of V
(V,v) . Y is Element of the carrier of V
v + Y 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:], 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,Y) is Element of the carrier of V
a is Element of bool the carrier of V
v + a is Element of bool the carrier of V
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in a } is set
W is set
c₈ is Element of the carrier of V
(V,v) . c₈ is Element of the carrier of V
v + c₈ 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:], 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,c₈) is Element of the carrier of V
Y is Element of bool the carrier of V
a is Element of bool the carrier of V
Y + a is Element of bool the carrier of V
{v} is non empty compact Element of bool the carrier of V
{v} + a is Element of bool the carrier of V
v + a is Element of bool the carrier of V
W is Element of bool the carrier of V
c₈ is Element of bool the carrier of V
v + c₈ is Element of bool the carrier of V
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
dom (V,v) is Element of bool the carrier of V
bool the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
rng (V,v) is Element of bool the carrier of V
(V,v) " is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
- v is Element of the carrier of V
(V,(- v)) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
w + v is Element of bool the carrier of V
(V,w) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like one-to-one V17( the carrier of V) quasi_total onto bijective continuous being_homeomorphism Element of bool [: the carrier of V, 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:] is non empty set
(V,w) .: v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is open Element of bool the carrier of V
w is Element of the carrier of V
w + v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is open Element of bool the carrier of V
w is Element of bool the carrier of V
w + v is Element of bool the carrier of V
bool (bool the carrier of V) is non empty set
{ (b₁ + v) where b₁ is Element of the carrier of V : b₁ in w } is set
s is Element of bool (bool the carrier of V)
c₅ is Element of bool the carrier of V
U is Element of the carrier of V
U + v is open Element of bool the carrier of V
union s is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
w is Element of bool the carrier of V
v is open Element of bool the carrier of V
w + v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is closed Element of bool the carrier of V
w is Element of the carrier of V
w + v is Element of bool the carrier of V
(V,w) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like one-to-one V17( the carrier of V) quasi_total onto bijective continuous being_homeomorphism Element of bool [: the carrier of V, 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:] is non empty set
(V,w) .: v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is closed Element of bool the carrier of V
w is Element of the carrier of V
w + v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 bool the carrier of V
Int v is open Element of bool the carrier of V
Int w is open Element of bool the carrier of V
(Int 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 TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Int w is open Element of bool the carrier of V
v + (Int w) is open Element of bool the carrier of V
v + w is Element of bool the carrier of V
Int (v + w) is open Element of bool the carrier of V
s is set
c₅ is Element of the carrier of V
U is Element of bool the carrier of V
- v is Element of the carrier of V
(- v) + U is Element of bool the carrier of V
(- v) + (v + w) is Element of bool the carrier of V
(- v) + 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),v) is Element of the carrier of V
((- v) + v) + w is Element of bool 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
(0. V) + w is Element of bool the carrier of V
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
(- v) + c₅ is Element of the carrier of V
the addF of V . ((- v),c₅) is Element of the carrier of V
v + ((- v) + c₅) is Element of the carrier of V
the addF of V . (v,((- v) + c₅)) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
(v + (- v)) + c₅ is Element of the carrier of V
the addF of V . ((v + (- v)),c₅) is Element of the carrier of V
(0. V) + c₅ is Element of the carrier of V
the addF of V . ((0. V),c₅) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl w is closed Element of bool the carrier of V
v + (Cl w) is closed Element of bool the carrier of V
v + w is Element of bool the carrier of V
Cl (v + w) is closed Element of bool the carrier of V
s is set
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in Cl w } is set
{ (v + b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
U is Element of bool the carrier of V
c₅ is Element of the carrier of V
- v is Element of the carrier of V
(- v) + U is Element of bool the carrier of V
{ ((- v) + b₁) where b₁ is Element of the carrier of V : b₁ in U } is set
(- v) + c₅ 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),c₅) 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 . (v,W) is Element of the carrier of V
(- v) + v is Element of the carrier of V
the addF of V . ((- v),v) is Element of the carrier of V
((- v) + v) + W is Element of the carrier of V
the addF of V . (((- v) + v),W) 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
(0. V) + W is Element of the carrier of V
the addF of V . ((0. V),W) is Element of the carrier of V
c₈ is set
Y is Element of the carrier of V
a is Element of the carrier of V
(- v) + a is Element of the carrier of V
the addF of V . ((- v),a) is Element of the carrier of V
v + Y is Element of the carrier of V
the addF of V . (v,Y) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
(v + (- v)) + a is Element of the carrier of V
the addF of V . ((v + (- v)),a) is Element of the carrier of V
(0. V) + a is Element of the carrier of V
the addF of V . ((0. V),a) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
w + 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,v) is Element of the carrier of V
s is non empty a_neighborhood of v
w + s is Element of bool the carrier of V
bool the carrier of V is non empty set
Int s is open Element of bool the carrier of V
w + (Int s) is open Element of bool the carrier of V
{ (w + b₁) where b₁ is Element of the carrier of V : b₁ in Int s } is set
Int (w + s) is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 the carrier of V
- v is Element of the carrier of V
w is non empty a_neighborhood of v
(- v) + w is Element of bool the carrier of V
bool the carrier of V is non empty set
Int w is open Element of bool the carrier of V
(- v) + (Int w) is open Element of bool the carrier of V
{ ((- v) + b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
(- v) + 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),v) is Element of the carrier of V
Int ((- v) + w) is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 open closed boundary nowhere_dense compact (V) (V) Element of bool 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
w is non empty a_neighborhood of 0. V
s is ext-real complex real Element of REAL
s * w is Element of bool the carrier of V
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 open closed boundary nowhere_dense compact (V) (V) (V) Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
s is non empty a_neighborhood of 0. V
c₅ is ext-real complex real Element of REAL
U is ext-real complex real Element of REAL
W is ext-real complex real Element of REAL
W * s is Element of bool the carrier of V
{ (W * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
W is ext-real complex real Element of REAL
W * s is Element of bool the carrier of V
{ (W * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 bool 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 is non empty a_neighborhood of 0. V
c₅ is ext-real complex real Element of REAL
U is ext-real complex real Element of REAL
U * s is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
{ b₁ where b₁ is (V) Element of bool the carrier of V : verum } is set
v is Element of bool (bool the carrier of V)
union v is Element of bool the carrier of V
w is Element of bool the carrier of V
s is (V) Element of bool the carrier of V
w is set
s is set
union s is set
{w} is non empty set
s \/ {w} is non empty set
union (s \/ {w}) is set
c₅ is Element of bool the carrier of V
c₅ is Element of bool the carrier of V
U is Element of bool the carrier of V
{U} is non empty Element of bool (bool the carrier of V)
s \/ {U} is non empty set
union (s \/ {U}) is set
union {U} is Element of bool the carrier of V
(union s) \/ (union {U}) is set
(union s) \/ U is set
c₅ \/ U is Element of bool the carrier of V
W 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 open closed boundary nowhere_dense compact (V) (V) (V) Element of bool the carrier of V
union v is set
w is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
{ b₁ where b₁ is non empty a_neighborhood of 0. V : verum } is set
v is Element of bool (bool the carrier of V)
w is non empty a_neighborhood of 0. V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
v is basis of 0. V
{ (b₁ + b₂) where b₁ is Element of the carrier of V, b₂ is Element of bool the carrier of V : b₂ in v } is set
w is Element of bool (bool the carrier of V)
s is Element of the carrier of V
c₅ is non empty a_neighborhood of s
Int c₅ is open Element of bool the carrier of V
- s is Element of the carrier of V
(- s) + (Int c₅) is open Element of bool the carrier of V
U is non empty a_neighborhood of 0. V
s + U is Element of bool the carrier of V
W is Element of bool the carrier of V
Int U is open Element of bool the carrier of V
s + (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 . (s,(0. V)) is Element of the carrier of V
s + (Int U) is open Element of bool the carrier of V
Int W is open Element of bool the carrier of V
s + ((- s) + (Int c₅)) is open Element of bool the carrier of V
s + (- s) is Element of the carrier of V
the addF of V . (s,(- s)) is Element of the carrier of V
(s + (- s)) + (Int c₅) is open Element of bool the carrier of V
(0. V) + (Int c₅) is open Element of bool the carrier of V
V is non empty ()
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
v is ext-real complex real Element of REAL
w is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
s is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
c₅ is Element of the carrier of V
s . c₅ is Element of the carrier of V
v * c₅ 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,c₅) is set
w is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
s is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
c₅ is Element of the carrier of V
w . c₅ is Element of the carrier of V
v * c₅ 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,c₅) is set
s . c₅ is Element of the carrier of V
V is non empty ()
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 non empty ext-real complex real Element of REAL
(V,w) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
(V,w) .: v is Element of bool the carrier of V
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
s is set
c₅ is Element of the carrier of V
(V,w) . c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
s is set
c₅ is Element of the carrier of V
w * c₅ 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,c₅) is set
(V,w) . c₅ is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
bool the carrier of V is non empty set
v is non empty ext-real complex real Element of REAL
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
rng (V,v) is Element of bool the carrier of V
w is set
s is Element of the carrier of V
v " is non empty ext-real complex real Element of REAL
(v ") * 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 . ((v "),s) is set
(V,v) . ((v ") * s) is Element of the carrier of V
v * ((v ") * s) is Element of the carrier of V
the Mult of V . (v,((v ") * s)) is set
v * (v ") is non empty ext-real complex real Element of REAL
(v * (v ")) * s is Element of the carrier of V
the Mult of V . ((v * (v ")),s) is set
1 * s is Element of the carrier of V
the Mult of V . (1,s) is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
v is non empty ext-real complex real Element of REAL
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
w is set
s is set
(V,v) . w is set
(V,v) . s is set
c₅ is Element of the carrier of V
v * c₅ 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,c₅) is set
U is Element of the carrier of V
v * U is Element of the carrier of V
the Mult of V . (v,U) is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is non empty ext-real complex real Element of REAL
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( 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:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
(V,v) " is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
v " is non empty ext-real complex real Element of REAL
(V,(v ")) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
rng (V,v) is Element of bool the carrier of V
bool the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
dom (V,v) is Element of bool the carrier of V
w is Element of the carrier of V
s is set
(V,v) . s is set
c₅ is Element of the carrier of V
v * c₅ 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,c₅) is set
((V,v) ") . w is Element of the carrier of V
(V,v) " is Relation-like Function-like set
((V,v) ") . w is set
1 * c₅ is Element of the carrier of V
the Mult of V . (1,c₅) is set
v * (v ") is non empty ext-real complex real Element of REAL
(v * (v ")) * c₅ is Element of the carrier of V
the Mult of V . ((v * (v ")),c₅) is set
(v ") * w is Element of the carrier of V
the Mult of V . ((v "),w) is set
(V,(v ")) . w is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
v is non empty ext-real complex real Element of REAL
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
bool the carrier of V is non empty set
w is Element of bool the carrier of V
bool (bool the carrier of V) is non empty set
s is Element of bool (bool the carrier of V)
c₅ is Element of bool (bool the carrier of V)
union c₅ is Element of bool the carrier of V
(V,v) " w is Element of bool the carrier of V
U is set
W is set
c₈ is Element of bool the carrier of V
Y is Element of the carrier of V
(V,v) . Y is Element of the carrier of V
v * Y 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,Y) is set
v * c₈ is Element of bool the carrier of V
{ (v * b₁) where b₁ is Element of the carrier of V : b₁ in c₈ } is set
U is set
W is Element of the carrier of V
(V,v) . W is Element of the carrier of V
v * 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 . (v,W) is set
Y is Element of bool the carrier of V
c₈ is non empty ext-real positive non negative complex real Element of REAL
v - v is ext-real complex real Element of REAL
abs (v - v) is ext-real complex real Element of REAL
v * Y is Element of bool the carrier of V
{ (v * b₁) where b₁ is Element of the carrier of V : b₁ in Y } is set
U is Element of bool the carrier of V
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
v is non empty ext-real complex real Element of REAL
(V,v) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
the carrier of V is non empty set
[: the carrier of V, the carrier of V:] is non empty set
bool [: the carrier of V, the carrier of V:] is non empty set
dom (V,v) is Element of bool the carrier of V
bool the carrier of V is non empty set
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
rng (V,v) is Element of bool the carrier of V
(V,v) " is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
v " is non empty ext-real complex real Element of REAL
(V,(v ")) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like V17( the carrier of V) quasi_total Element of bool [: the carrier of V, the carrier of V:]
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is open 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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(V,w) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like one-to-one V17( the carrier of V) quasi_total onto bijective continuous being_homeomorphism Element of bool [: the carrier of V, 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:] is non empty set
(V,w) .: v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is closed 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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(V,w) is non empty Relation-like the carrier of V -defined the carrier of V -valued Function-like one-to-one V17( the carrier of V) quasi_total onto bijective continuous being_homeomorphism Element of bool [: the carrier of V, 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:] is non empty set
(V,w) .: v is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Int v is open Element of bool the carrier of V
w is non empty ext-real complex real Element of REAL
w * (Int v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Int v } is set
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
Int (w * v) is open Element of bool the carrier of V
s is set
c₅ is Element of the carrier of V
U is Element of bool the carrier of V
w " is non empty ext-real complex real Element of REAL
(w ") * U is Element of bool the carrier of V
{ ((w ") * b₁) where b₁ is Element of the carrier of V : b₁ in U } is set
(w ") * (w * v) is Element of bool the carrier of V
{ ((w ") * b₁) where b₁ is Element of the carrier of V : b₁ in w * v } is set
(w ") * w is non empty ext-real complex real Element of REAL
((w ") * w) * v is Element of bool the carrier of V
{ (((w ") * w) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 * v is Element of bool the carrier of V
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(w ") * c₅ 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 "),c₅) is set
w * ((w ") * c₅) is Element of the carrier of V
the Mult of V . (w,((w ") * c₅)) is set
w * (w ") is non empty ext-real complex real Element of REAL
(w * (w ")) * c₅ is Element of the carrier of V
the Mult of V . ((w * (w ")),c₅) is set
1 * c₅ is Element of the carrier of V
the Mult of V . (1,c₅) is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
w is non empty ext-real complex real Element of REAL
w * (Cl v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Cl v } is set
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
Cl (w * v) is closed Element of bool the carrier of V
s is set
U is Element of bool the carrier of V
c₅ is Element of the carrier of V
w " is non empty ext-real complex real Element of REAL
(w ") * c₅ 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 "),c₅) is set
(w ") * U is Element of bool the carrier of V
{ ((w ") * b₁) where b₁ is Element of the carrier of V : b₁ in U } is set
W is Element of the carrier of V
w * W is Element of the carrier of V
the Mult of V . (w,W) is set
(w ") * w is non empty ext-real complex real Element of REAL
((w ") * w) * W is Element of the carrier of V
the Mult of V . (((w ") * w),W) is set
1 * W is Element of the carrier of V
the Mult of V . (1,W) is set
c₈ is set
Y is Element of the carrier of V
a is Element of the carrier of V
(w ") * a is Element of the carrier of V
the Mult of V . ((w "),a) is set
w * Y is Element of the carrier of V
the Mult of V . (w,Y) is set
w * (w ") is non empty ext-real complex real Element of REAL
(w * (w ")) * a is Element of the carrier of V
the Mult of V . ((w * (w ")),a) is set
1 * a is Element of the carrier of V
the Mult of V . (1,a) is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
0 * (Cl v) is Element of bool the carrier of V
{ (0 * b₁) where b₁ is Element of the carrier of V : b₁ in Cl v } is set
0 * v is Element of bool the carrier of V
{ (0 * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
Cl (0 * v) is closed 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 open closed boundary nowhere_dense compact (V) (V) (V) Element of bool 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
{(0. V)} is non empty compact Element of bool the carrier of V
Cl {(0. V)} is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 non empty ext-real complex real Element of REAL
s * w is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
s * 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 . (s,v) is set
Int w is open Element of bool the carrier of V
s * (Int w) is Element of bool the carrier of V
{ (s * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
Int (s * w) is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is non empty a_neighborhood of 0. V
w is non empty ext-real complex real Element of REAL
w * v is Element of bool the carrier of V
bool the carrier of V is non empty set
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ 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
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 ext-real complex real Element of REAL
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
s is non empty a_neighborhood of 0. V
c₅ is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural complex real Element of NAT
U is ext-real complex real Element of REAL
U * s is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
{(0. V)} is non empty compact Element of bool 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 is non empty a_neighborhood of 0. V
1 / w is ext-real complex real Element of REAL
(1 / w) * s is Element of bool the carrier of V
{ ((1 / w) * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
c₅ is ext-real complex real Element of REAL
U is ext-real complex real Element of REAL
U * s is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
U * ((1 / w) * s) is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in (1 / w) * s } is set
w * (U * ((1 / w) * s)) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in U * ((1 / w) * s) } is set
U * (1 / w) is ext-real complex real Element of REAL
(U * (1 / w)) * s is Element of bool the carrier of V
{ ((U * (1 / w)) * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
w * ((U * (1 / w)) * s) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in (U * (1 / w)) * s } is set
(1 / w) * (U * s) is Element of bool the carrier of V
{ ((1 / w) * b₁) where b₁ is Element of the carrier of V : b₁ in U * s } is set
w * ((1 / w) * (U * s)) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in (1 / w) * (U * s) } is set
w * (1 / w) is ext-real complex real Element of REAL
(w * (1 / w)) * (U * s) is Element of bool the carrier of V
{ ((w * (1 / w)) * b₁) where b₁ is Element of the carrier of V : b₁ in U * s } is set
1 * (U * s) is Element of bool the carrier of V
{ (1 * b₁) where b₁ is Element of the carrier of V : b₁ in U * s } is set
W is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 ext-real complex real Element of REAL
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is non empty a_neighborhood of 0. V
(0. 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 . ((0. V),(0. V)) is Element of the carrier of V
w is non empty a_neighborhood of 0. V
s is non empty a_neighborhood of 0. V
w + s is Element of bool the carrier of V
bool the carrier of V is non empty set
Int w is open Element of bool the carrier of V
Int s is open Element of bool the carrier of V
(Int w) /\ (Int s) is open Element of bool the carrier of V
(- 1) * (Int w) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
((Int w) /\ (Int s)) /\ ((- 1) * (Int w)) is Element of bool the carrier of V
(- 1) * (Int s) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Int s } is set
(((Int w) /\ (Int s)) /\ ((- 1) * (Int w))) /\ ((- 1) * (Int s)) is Element of bool the carrier of V
(- 1) * s is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
Int ((- 1) * s) is open Element of bool the carrier of V
(- 1) * w is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
Int ((- 1) * w) is open Element of bool the carrier of V
Int ((((Int w) /\ (Int s)) /\ ((- 1) * (Int w))) /\ ((- 1) * (Int s))) is open Element of bool the carrier of V
U is non empty open a_neighborhood of 0. V
U + U is open Element of bool the carrier of V
(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL
((- 1) * (- 1)) * (Int w) is Element of bool the carrier of V
{ (((- 1) * (- 1)) * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
(- 1) * ((- 1) * (Int w)) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in (- 1) * (Int w) } is set
((- 1) * (- 1)) * (Int s) is Element of bool the carrier of V
{ (((- 1) * (- 1)) * b₁) where b₁ is Element of the carrier of V : b₁ in Int s } is set
(- 1) * ((- 1) * (Int s)) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in (- 1) * (Int s) } is set
((- 1) * (Int w)) /\ ((- 1) * (Int s)) is Element of bool the carrier of V
((Int w) /\ (Int s)) /\ (((- 1) * (Int w)) /\ ((- 1) * (Int s))) is Element of bool the carrier of V
(- 1) * ((Int w) /\ (Int s)) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in (Int w) /\ (Int s) } is set
((- 1) * ((Int w) /\ (Int s))) /\ ((Int w) /\ (Int s)) is Element of bool the carrier of V
(- 1) * (((- 1) * (Int w)) /\ ((- 1) * (Int s))) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in ((- 1) * (Int w)) /\ ((- 1) * (Int s)) } is set
((- 1) * ((Int w) /\ (Int s))) /\ ((- 1) * (((- 1) * (Int w)) /\ ((- 1) * (Int s)))) is Element of bool the carrier of V
(- 1) * (((Int w) /\ (Int s)) /\ (((- 1) * (Int w)) /\ ((- 1) * (Int s)))) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in ((Int w) /\ (Int s)) /\ (((- 1) * (Int w)) /\ ((- 1) * (Int s))) } is set
(V,U) is Element of bool the carrier of V
(- 1) * U is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in U } is set
W is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in U & b₂ in U ) } is set
c₈ is Element of the carrier of V
Y is Element of the carrier of V
c₈ + Y is Element of the carrier of V
the addF of V . (c₈,Y) is Element of the carrier of V
(Int w) + (Int s) is open Element of bool the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in Int w & b₂ in Int s ) } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 compact Element of bool the carrier of V
w is closed Element of bool the carrier of V
[#] V is non empty non proper open closed dense non boundary Element of bool the carrier of V
s is non empty non proper open closed dense non boundary Element of bool the carrier of V
v + s is open Element of bool the carrier of V
w + s is open Element of bool the carrier of V
{ [b₁,b₂] where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ in v & b₂ is (V) & ((b₁ + b₂) + b₂) + b₂ misses w ) } is set
c₅ is Element of the carrier of V
w ` is open Element of bool the carrier of V
the carrier of V \ w is set
- c₅ is Element of the carrier of V
(- c₅) + (w `) is open Element of bool the carrier of V
{ ((- c<sub>5</sub>) + b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of V : b<sub>1</sub> in w ` } is set
(- c₅) + c₅ 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 . ((- c₅),c₅) is Element of the carrier of V
U is non empty open a_neighborhood of 0. V
U + U is open Element of bool the carrier of V
W is non empty open a_neighborhood of 0. V
W + W is open Element of bool the carrier of V
c₈ is non empty open a_neighborhood of 0. V
Y is set
a is Element of the carrier of V
a + (0. V) is Element of the carrier of V
the addF of V . (a,(0. V)) is Element of the carrier of V
c₈ + c₈ is open Element of bool the carrier of V
c₈ + c₈ is open Element of bool the carrier of V
c₈ + (c₈ + c₈) is open Element of bool the carrier of V
(c₈ + c₈) + c₈ is open Element of bool the carrier of V
c₅ + ((c₈ + c₈) + c₈) is open Element of bool the carrier of V
c₅ + ((- c₅) + (w `)) is open Element of bool the carrier of V
c<sub>5</sub> + c<sub>8</sub> is open Element of bool the carrier of V
(c<sub>5</sub> + c<sub>8</sub>) + (c<sub>8</sub> + c<sub>8</sub>) is open Element of bool the carrier of V
(c<sub>5</sub> + c<sub>8</sub>) + c<sub>8</sub> is open Element of bool the carrier of V
((c<sub>5</sub> + c<sub>8</sub>) + c<sub>8</sub>) + c<sub>8</sub> is open Element of bool the carrier of V
c<sub>5</sub> + (- c<sub>5</sub>) is Element of the carrier of V
the addF of V . (c<sub>5</sub>,(- c<sub>5</sub>)) is Element of the carrier of V
(c<sub>5</sub> + (- c<sub>5</sub>)) + (w `) is open Element of bool the carrier of V
(0. V) + (w `) is open Element of bool the carrier of V
c₅ is set
U is Element of the carrier of V
W is non empty open a_neighborhood of 0. V
U + W is open Element of bool the carrier of V
(U + W) + W is open Element of bool the carrier of V
((U + W) + W) + W is open Element of bool the carrier of V
[: the carrier of V,(bool the carrier of V):] is non empty set
[U,W] is Element of [: the carrier of V,(bool the carrier of V):]
{U,W} is non empty set
{U} is non empty set
{{U,W},{U}} is non empty set
c₈ is Element of [: the carrier of V,(bool the carrier of V):]
c₅ is set
U is set
W is set
c₈ is Element of the carrier of V
a is non empty open a_neighborhood of 0. V
[c₈,a] is Element of [: the carrier of V,(bool the carrier of V):]
{c₈,a} is non empty set
{c₈} is non empty set
{{c₈,a},{c₈}} is non empty set
Y is Element of the carrier of V
a is non empty open a_neighborhood of 0. V
[Y,a] is Element of [: the carrier of V,(bool the carrier of V):]
{Y,a} is non empty set
{Y} is non empty set
{{Y,a},{Y}} is non empty set
c₈ + a is open Element of bool the carrier of V
Y + a is open Element of bool the carrier of V
v is Element of the carrier of V
y is non empty open a_neighborhood of 0. V
[v,y] is Element of [: the carrier of V,(bool the carrier of V):]
{v,y} is non empty set
{v} is non empty set
{{v,y},{v}} is non empty set
a is Element of the carrier of V
FxVxVx is non empty open a_neighborhood of 0. V
[a,FxVxVx] is Element of [: the carrier of V,(bool the carrier of V):]
{a,FxVxVx} is non empty set
{a} is non empty set
{{a,FxVxVx},{a}} is non empty set
v + y is open Element of bool the carrier of V
a + FxVxVx is open Element of bool the carrier of V
U is Element of [: the carrier of V,(bool the carrier of V):]
c₅ is non empty set
U is set
W is Element of the carrier of V
c₈ is non empty open a_neighborhood of 0. V
[W,c₈] is Element of [: the carrier of V,(bool the carrier of V):]
{W,c₈} is non empty set
{W} is non empty set
{{W,c₈},{W}} is non empty set
W + c₈ is open Element of bool the carrier of V
(W + c₈) + c₈ is open Element of bool the carrier of V
((W + c₈) + c₈) + c₈ is open Element of bool the carrier of V
U is set
c₈ is Element of the carrier of V
a is non empty open a_neighborhood of 0. V
[c₈,a] is Element of [: the carrier of V,(bool the carrier of V):]
{c₈,a} is non empty set
{c₈} is non empty set
{{c₈,a},{c₈}} is non empty set
W is set
Y is Element of the carrier of V
a is non empty open a_neighborhood of 0. V
[Y,a] is Element of [: the carrier of V,(bool the carrier of V):]
{Y,a} is non empty set
{Y} is non empty set
{{Y,a},{Y}} is non empty set
c₈ + a is open Element of bool the carrier of V
Y + a is open Element of bool the carrier of V
[:c₅,c₅:] is non empty set
bool [:c₅,c₅:] is non empty set
U is Relation-like c₅ -defined c₅ -valued V17(c₅) quasi_total V39() V41() V46() Element of bool [:c₅,c₅:]
W is set
Class U is non empty with_non-empty_elements a_partition of c₅
c₈ is set
Class (U,c₈) is Element of bool c₅
bool c₅ is non empty set
W is Relation-like Function-like set
dom W is set
rng W is set
{ (b₁ + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : [b₁,b₂] in rng W } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
a is set
v is non empty open a_neighborhood of 0. V
a is Element of the carrier of V
a + v is open Element of bool the carrier of V
[a,v] is Element of [: the carrier of V,(bool the carrier of V):]
{a,v} is non empty set
{a} is non empty set
{{a,v},{a}} is non empty set
a is Element of bool (bool the carrier of V)
a is set
union a is set
v is Element of the carrier of V
a is non empty open a_neighborhood of 0. V
v + a is open Element of bool the carrier of V
(v + a) + a is open Element of bool the carrier of V
((v + a) + a) + a is open Element of bool the carrier of V
[v,a] is Element of [: the carrier of V,(bool the carrier of V):]
{v,a} is non empty set
{v} is non empty set
{{v,a},{v}} is non empty set
Class (U,[v,a]) is Element of bool c₅
bool c₅ is non empty set
W . (Class (U,[v,a])) is set
v + (0. V) is Element of the carrier of V
the addF of V . (v,(0. V)) is Element of the carrier of V
[(W . (Class (U,[v,a]))),[v,a]] is set
{(W . (Class (U,[v,a]))),[v,a]} is non empty set
{(W . (Class (U,[v,a])))} is non empty set
{{(W . (Class (U,[v,a]))),[v,a]},{(W . (Class (U,[v,a])))}} is non empty set
y is Element of the carrier of V
V is non empty open a_neighborhood of 0. V
[y,V] is Element of [: the carrier of V,(bool the carrier of V):]
{y,V} is non empty set
{y} is non empty set
{{y,V},{y}} is non empty set
FxVxVx is Element of the carrier of V
FxVxV is non empty open a_neighborhood of 0. V
[FxVxVx,FxVxV] is Element of [: the carrier of V,(bool the carrier of V):]
{FxVxVx,FxVxV} is non empty set
{FxVxVx} is non empty set
{{FxVxVx,FxVxV},{FxVxVx}} is non empty set
y + V is open Element of bool the carrier of V
FxVxVx + FxVxV is open Element of bool the carrier of V
a is Element of bool the carrier of V
a is non empty open a_neighborhood of 0. V
v is Element of the carrier of V
v + a is open Element of bool the carrier of V
[v,a] is Element of [: the carrier of V,(bool the carrier of V):]
{v,a} is non empty set
{v} is non empty set
{{v,a},{v}} is non empty set
a is Element of bool (bool the carrier of V)
{ b₁ where b₁ is non empty open a_neighborhood of 0. V : ex b₂ being Element of the carrier of V st
( b₂ + b₁ in a & [b₂,b₁] in rng W ) } is set
a is set
y is non empty open a_neighborhood of 0. V
FxVxVx is Element of the carrier of V
FxVxVx + y is open Element of bool the carrier of V
[FxVxVx,y] is Element of [: the carrier of V,(bool the carrier of V):]
{FxVxVx,y} is non empty set
{FxVxVx} is non empty set
{{FxVxVx,y},{FxVxVx}} is non empty set
a is Element of bool (bool the carrier of V)
y is set
V is non empty open a_neighborhood of 0. V
FxVxVx is Element of the carrier of V
FxVxVx + V is open Element of bool the carrier of V
[FxVxVx,V] is Element of [: the carrier of V,(bool the carrier of V):]
{FxVxVx,V} is non empty set
{FxVxVx} is non empty set
{{FxVxVx,V},{FxVxVx}} is non empty set
[:a,a:] is set
bool [:a,a:] is non empty set
y is Relation-like a -defined a -valued Function-like quasi_total Element of bool [:a,a:]
{ ((b₁ + b₂) + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } is set
meet a is Element of bool the carrier of V
V is Element of bool the carrier of V
v + V is Element of bool the carrier of V
w + V is Element of bool the carrier of V
FxVxV is set
z is set
W . z is set
FxVxV is Element of bool the carrier of V
FxVxV is Element of the carrier of V
z is Element of bool the carrier of V
v is non empty open a_neighborhood of 0. V
u is Element of the carrier of V
u + v is open Element of bool the carrier of V
[u,v] is Element of [: the carrier of V,(bool the carrier of V):]
{u,v} is non empty set
{u} is non empty set
{{u,v},{u}} is non empty set
dom y is Element of bool a
bool a is non empty set
FxVxV is set
rng y is Element of bool a
bool a is non empty set
FxVxV is set
z is non empty open a_neighborhood of 0. V
u is Element of the carrier of V
u + z is open Element of bool the carrier of V
[u,z] is Element of [: the carrier of V,(bool the carrier of V):]
{u,z} is non empty set
{u} is non empty set
{{u,z},{u}} is non empty set
u is Element of the carrier of V
u + z is open Element of bool the carrier of V
[u,z] is Element of [: the carrier of V,(bool the carrier of V):]
{u,z} is non empty set
{u} is non empty set
{{u,z},{u}} is non empty set
y . (u + z) is set
Vu is non empty open a_neighborhood of 0. V
v is Element of the carrier of V
v + Vu is open Element of bool the carrier of V
[v,Vu] is Element of [: the carrier of V,(bool the carrier of V):]
{v,Vu} is non empty set
{v} is non empty set
{{v,Vu},{v}} is non empty set
[[u,z],[v,Vu]] is Element of [:[: the carrier of V,(bool the carrier of V):],[: the carrier of V,(bool the carrier of V):]:]
[:[: the carrier of V,(bool the carrier of V):],[: the carrier of V,(bool the carrier of V):]:] is non empty set
{[u,z],[v,Vu]} is non empty set
{[u,z]} is non empty set
{{[u,z],[v,Vu]},{[u,z]}} is non empty set
Class (U,[v,Vu]) is Element of bool c₅
bool c₅ is non empty set
Class (U,[u,z]) is Element of bool c₅
x is set
W . x is set
Vx is set
Class (U,Vx) is Element of bool c₅
u is set
W . u is set
v is set
Class (U,v) is Element of bool c₅
FxVxV is Element of the carrier of V
z is non empty open a_neighborhood of 0. V
FxVxV + z is open Element of bool the carrier of V
[FxVxV,z] is Element of [: the carrier of V,(bool the carrier of V):]
{FxVxV,z} is non empty set
{FxVxV} is non empty set
{{FxVxV,z},{FxVxV}} is non empty set
(FxVxV + z) + z is open Element of bool the carrier of V
((FxVxV + z) + z) + z is open Element of bool the carrier of V
u is set
W . u is set
v is set
Class (U,v) is Element of bool c₅
bool c₅ is non empty set
Class (U,[FxVxV,z]) is Element of bool c₅
x is non empty open a_neighborhood of 0. V
Vu is Element of the carrier of V
Vu + x is open Element of bool the carrier of V
[Vu,x] is Element of [: the carrier of V,(bool the carrier of V):]
{Vu,x} is non empty set
{Vu} is non empty set
{{Vu,x},{Vu}} is non empty set
[[FxVxV,z],[Vu,x]] is Element of [:[: the carrier of V,(bool the carrier of V):],[: the carrier of V,(bool the carrier of V):]:]
[:[: the carrier of V,(bool the carrier of V):],[: the carrier of V,(bool the carrier of V):]:] is non empty set
{[FxVxV,z],[Vu,x]} is non empty set
{[FxVxV,z]} is non empty set
{{[FxVxV,z],[Vu,x]},{[FxVxV,z]}} is non empty set
Class (U,[Vu,x]) is Element of bool c₅
Vx is set
W . Vx is set
u is set
Class (U,u) is Element of bool c₅
v is Element of the carrier of V
z is non empty open a_neighborhood of 0. V
[v,z] is Element of [: the carrier of V,(bool the carrier of V):]
{v,z} is non empty set
{v} is non empty set
{{v,z},{v}} is non empty set
v + z is open Element of bool the carrier of V
(v + z) + z is open Element of bool the carrier of V
((v + z) + z) + z is open Element of bool the carrier of V
FxVxV is set
{{}} is non empty set
u is Element of the carrier of V
v is Element of bool the carrier of V
x is non empty open a_neighborhood of 0. V
Vu is Element of the carrier of V
Vu + x is open Element of bool the carrier of V
[Vu,x] is Element of [: the carrier of V,(bool the carrier of V):]
{Vu,x} is non empty set
{Vu} is non empty set
{{Vu,x},{Vu}} is non empty set
(Vu + x) + x is open Element of bool the carrier of V
((Vu + x) + x) + x is open Element of bool the carrier of V
z is set
Vx is set
u is set
{(w + V)} is non empty Element of bool (bool the carrier of V)
v is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in w & b₂ in V ) } is set
z is set
z is Element of the carrier of V
u is Element of the carrier of V
v is Element of the carrier of V
u + v is Element of the carrier of V
the addF of V . (u,v) is Element of the carrier of V
- v is Element of the carrier of V
z + (- v) is Element of the carrier of V
the addF of V . (z,(- v)) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
u + (v + (- v)) is Element of the carrier of V
the addF of V . (u,(v + (- v))) is Element of the carrier of V
u + (0. V) is Element of the carrier of V
the addF of V . (u,(0. V)) is Element of the carrier of V
u /\ v is set
z is set
u is set
z /\ u is set
Vu is non empty open a_neighborhood of 0. V
v is Element of the carrier of V
v + Vu is open Element of bool the carrier of V
(v + Vu) + Vu is open Element of bool the carrier of V
[v,Vu] is Element of [: the carrier of V,(bool the carrier of V):]
{v,Vu} is non empty set
{v} is non empty set
{{v,Vu},{v}} is non empty set
((v + Vu) + Vu) + Vu is open Element of bool the carrier of V
x is set
Vx is Element of the carrier of V
u is Element of the carrier of V
v is Element of the carrier of V
u + v is Element of the carrier of V
the addF of V . (u,v) is Element of the carrier of V
- v is Element of the carrier of V
Vx + (- v) is Element of the carrier of V
the addF of V . (Vx,(- v)) is Element of the carrier of V
v + (- v) is Element of the carrier of V
the addF of V . (v,(- v)) is Element of the carrier of V
u + (v + (- v)) is Element of the carrier of V
the addF of V . (u,(v + (- v))) is Element of the carrier of V
u + (0. V) is Element of the carrier of V
the addF of V . (u,(0. V)) is Element of the carrier of V
INTERSECTION ({(w + V)}, { ((b₁ + b₂) + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } ) is set
union (INTERSECTION ({(w + V)}, { ((b₁ + b₂) + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } )) is set
union { ((b₁ + b₂) + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } is set
(w + V) /\ (union { ((b₁ + b₂) + b₂) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } ) is Element of bool the carrier of V
FxVxV is Element of bool the carrier of V
z is non empty open a_neighborhood of 0. V
u is Element of the carrier of V
u + z is open Element of bool the carrier of V
[u,z] is Element of [: the carrier of V,(bool the carrier of V):]
{u,z} is non empty set
{u} is non empty set
{{u,z},{u}} is non empty set
y " a is Element of bool a
Int V is open Element of bool the carrier of V
FxVxV is set
z is Element of bool the carrier of V
Int z is open Element of bool the carrier of V
u is non empty open a_neighborhood of 0. V
v is Element of the carrier of V
v + u is open Element of bool the carrier of V
[v,u] is Element of [: the carrier of V,(bool the carrier of V):]
{v,u} is non empty set
{v} is non empty set
{{v,u},{v}} is non empty set
FxVxV is set
{ ((b₁ + b₂) + V) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } is set
union { ((b₁ + b₂) + V) where b₁ is Element of the carrier of V, b₂ is non empty open a_neighborhood of 0. V : ( b₁ + b₂ in a & [b₁,b₂] in rng W ) } is set
z is set
u is set
Vu is non empty open a_neighborhood of 0. V
v is Element of the carrier of V
v + Vu is open Element of bool the carrier of V
(v + Vu) + V is open Element of bool the carrier of V
[v,Vu] is Element of [: the carrier of V,(bool the carrier of V):]
{v,Vu} is non empty set
{v} is non empty set
{{v,Vu},{v}} is non empty set
(v + Vu) + Vu is open Element of bool the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v + Vu & b₂ in V ) } is set
x is Element of the carrier of V
Vx is Element of the carrier of V
x + Vx is Element of the carrier of V
the addF of V . (x,Vx) is Element of the carrier of V
z is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in V ) } is set
u is Element of the carrier of V
v is Element of the carrier of V
u + v is Element of the carrier of V
the addF of V . (u,v) is Element of the carrier of V
Vu is Element of bool the carrier of V
Vx is non empty open a_neighborhood of 0. V
x is Element of the carrier of V
x + Vx is open Element of bool the carrier of V
[x,Vx] is Element of [: the carrier of V,(bool the carrier of V):]
{x,Vx} is non empty set
{x} is non empty set
{{x,Vx},{x}} is non empty set
(x + Vx) + V is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is basis of 0. V
w is non empty a_neighborhood of 0. V
Int w is open Element of bool the carrier of V
bool the carrier of V is non empty set
(Int w) ` is closed Element of bool the carrier of V
the carrier of V \ (Int w) is set
{(0. V)} is non empty compact Element of bool the carrier of V
U is non empty a_neighborhood of 0. V
{(0. V)} + U is Element of bool the carrier of V
((Int w) `) + U is Element of bool the carrier of V
Int U is open Element of bool the carrier of V
W is non empty open a_neighborhood of 0. V
{(0. V)} + W is open Element of bool the carrier of V
((Int w) `) + W is open Element of bool the carrier of V
Cl ({(0. V)} + W) is closed Element of bool the carrier of V
Cl W is closed Element of bool the carrier of V
c₈ is non empty a_neighborhood of 0. V
Cl c₈ is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is non empty a_neighborhood of 0. V
{ b₁ where b₁ is non empty a_neighborhood of 0. V : verum } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
s is set
c₅ is non empty a_neighborhood of 0. V
s is non empty a_neighborhood of 0. V
Cl s is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
v is Element of the carrier of V
w is Element of the carrier of V
bool the carrier of V is non empty set
{w} is non empty compact Element of bool 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
{v} is non empty compact Element of bool the carrier of V
s is non empty a_neighborhood of 0. V
{v} + s is Element of bool the carrier of V
{w} + s is Element of bool the carrier of V
Int s is open Element of bool the carrier of V
v + (Int s) is open Element of bool the carrier of V
w + (Int s) is open 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
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
w + (0. V) is Element of the carrier of V
the addF of V . (w,(0. V)) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
{ (v + b₁) where b₁ is non empty a_neighborhood of 0. V : verum } is set
meet { (v + b₁) where b₁ is non empty a_neighborhood of 0. V : verum } is set
the non empty a_neighborhood of 0. V is non empty a_neighborhood of 0. V
c₅ is Element of the carrier of V
U is non empty a_neighborhood of 0. V
Int U is open Element of bool the carrier of V
c₅ + (Int U) is open Element of bool the carrier of V
(- 1) * (Int U) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Int U } is set
v + ((- 1) * (Int U)) is Element of bool the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in (- 1) * (Int U) ) } is set
(V,(Int U)) is Element of bool the carrier of V
v + (V,(Int U)) is Element of bool the carrier of V
W is Element of the carrier of V
c₈ is Element of the carrier of V
W + c₈ 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,c₈) is Element of the carrier of V
Y is Element of the carrier of V
(- 1) * Y 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),Y) is set
- c₈ is Element of the carrier of V
(- 1) * c₈ is Element of the carrier of V
the Mult of V . ((- 1),c₈) is set
(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL
((- 1) * (- 1)) * Y is Element of the carrier of V
the Mult of V . (((- 1) * (- 1)),Y) is set
c₅ + Y is Element of the carrier of V
the addF of V . (c₅,Y) is Element of the carrier of V
c₈ + (- c₈) is Element of the carrier of V
the addF of V . (c₈,(- c₈)) is Element of the carrier of V
W + (c₈ + (- c₈)) is Element of the carrier of V
the addF of V . (W,(c₈ + (- c₈))) is Element of the carrier of V
W + (0. V) is Element of the carrier of V
the addF of V . (W,(0. V)) is Element of the carrier of V
{ (c₅ + b₁) where b₁ is Element of the carrier of V : b₁ in Int U } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
bool (bool the carrier of V) is non empty set
c₅ is set
U is non empty a_neighborhood of 0. V
v + U is Element of bool the carrier of V
U is Element of the carrier of V
W is non empty a_neighborhood of 0. V
Int W is open Element of bool the carrier of V
U + (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 . (U,(0. V)) is Element of the carrier of V
U + (Int W) is open Element of bool the carrier of V
W is Element of bool the carrier of V
- U is Element of the carrier of V
(- U) + W is Element of bool the carrier of V
Int ((- U) + W) is open Element of bool 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
U + ((- U) + W) is Element of bool 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
(U + (- U)) + W is Element of bool the carrier of V
(0. V) + W is Element of bool the carrier of V
v + the non empty a_neighborhood of 0. V is Element of bool the carrier of V
U is set
c₈ is set
Y is non empty a_neighborhood of 0. V
v + Y is Element of bool the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in Y ) } is set
(- 1) * Y is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Y } is set
Int ((- 1) * Y) is open Element of bool the carrier of V
W is Element of the carrier of V
W + (Int ((- 1) * Y)) is open Element of bool the carrier of V
(- 1) * (Int ((- 1) * Y)) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Int ((- 1) * Y) } is set
v + ((- 1) * (Int ((- 1) * Y))) is Element of bool the carrier of V
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in v & b₂ in (- 1) * (Int ((- 1) * Y)) ) } is set
a is Element of the carrier of V
a is Element of the carrier of V
a + a 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 . (a,a) is Element of the carrier of V
v is Element of the carrier of V
(- 1) * 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),v) is set
a is Element of the carrier of V
(- 1) * a is Element of the carrier of V
the Mult of V . ((- 1),a) is set
(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL
((- 1) * (- 1)) * a is Element of the carrier of V
the Mult of V . (((- 1) * (- 1)),a) is set
U is set
c₅ is Element of bool (bool the carrier of V)
meet c₅ is Element of bool the carrier of V
c₈ is non empty a_neighborhood of 0. V
Int c₈ is open Element of bool the carrier of V
(- 1) * (Int c₈) is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in Int c₈ } is set
v + ((- 1) * (Int c₈)) is Element of bool the carrier of V
W is Element of the carrier of V
W + (Int c₈) is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Int v is open Element of bool the carrier of V
w is Element of bool the carrier of V
Int w is open Element of bool the carrier of V
(Int v) + (Int w) is open Element of bool the carrier of V
v + w is Element of bool the carrier of V
Int (v + w) is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
w is Element of bool the carrier of V
Cl w is closed Element of bool the carrier of V
(Cl v) + (Cl w) is Element of bool the carrier of V
v + w is Element of bool the carrier of V
Cl (v + w) is closed Element of bool the carrier of V
s is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in Cl v & b₂ in Cl w ) } is set
c₅ is Element of the carrier of V
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₈ is Element of bool the carrier of V
Y is non empty a_neighborhood of U
a is non empty a_neighborhood of W
Y + a is Element of bool the carrier of V
Int Y is open Element of bool the carrier of V
a is set
Int a is open Element of bool the carrier of V
(Int Y) + (Int a) is open Element of bool the carrier of V
Int c₈ is open Element of bool the carrier of V
a is set
v is Element of the carrier of V
y is Element of the carrier of V
v + y is Element of the carrier of V
the addF of V . (v,y) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed 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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 - w is ext-real complex real Element of REAL
(1 - w) * v is Element of bool the carrier of V
{ ((1 - w) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(w * v) + ((1 - w) * v) is Element of bool the carrier of V
Cl ((w * v) + ((1 - w) * v)) is closed Element of bool the carrier of V
0 + w is ext-real complex real Element of REAL
(1 - w) * (Cl v) is Element of bool the carrier of V
{ ((1 - w) * b₁) where b₁ is Element of the carrier of V : b₁ in Cl v } is set
Cl ((1 - w) * v) is closed Element of bool the carrier of V
Cl (w * v) is closed Element of bool the carrier of V
(Cl (w * v)) + (Cl ((1 - w) * v)) is Element of bool the carrier of V
w * (Cl v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Cl v } is set
(w * (Cl v)) + ((1 - w) * (Cl v)) is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Int v is open 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₁) where b₁ is Element of the carrier of V : b₁ in v } is set
1 - w is ext-real complex real Element of REAL
(1 - w) * v is Element of bool the carrier of V
{ ((1 - w) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
(w * v) + ((1 - w) * v) is Element of bool the carrier of V
Int ((w * v) + ((1 - w) * v)) is open Element of bool the carrier of V
0 + w is ext-real complex real Element of REAL
(1 - w) * (Int v) is Element of bool the carrier of V
{ ((1 - w) * b₁) where b₁ is Element of the carrier of V : b₁ in Int v } is set
Int ((1 - w) * v) is open Element of bool the carrier of V
Int (w * v) is open Element of bool the carrier of V
(Int (w * v)) + (Int ((1 - w) * v)) is open Element of bool the carrier of V
w * (Int v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Int v } is set
(w * (Int v)) + ((1 - w) * (Int v)) is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Int v is open Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is (V) (V) Element of bool the carrier of V
Cl v is closed 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 * (Cl v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Cl v } is set
{} V is empty proper ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real open closed boundary nowhere_dense compact (V) (V) (V) 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 open closed boundary nowhere_dense compact (V) (V) (V) Element of bool 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
{(0. V)} is non empty compact 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 open closed boundary nowhere_dense compact (V) (V) (V) Element of bool the carrier of V
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
Cl (w * v) is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
the carrier of V is non empty set
bool the carrier of V is non empty set
v is (V) (V) Element of bool the carrier of V
Cl v is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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 (V) (V) Element of bool the carrier of V
Int v is open 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 * (Int v) is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in Int v } is set
w * v is Element of bool the carrier of V
{ (w * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
Int (w * v) is open Element of bool the carrier of V
{(0. V)} is non empty compact Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool 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
w is non empty a_neighborhood of 0. V
s is non empty a_neighborhood of 0. V
Cl s is closed Element of bool the carrier of V
c₅ is ext-real complex real Element of REAL
U is ext-real complex real Element of REAL
U * w is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
U * s is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
Cl (U * s) is closed Element of bool the carrier of V
U * (Cl s) is Element of bool the carrier of V
{ (U * b₁) where b₁ is Element of the carrier of V : b₁ in Cl s } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
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
Cl v is closed Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
w is non empty a_neighborhood of 0. V
v is non empty a_neighborhood of 0. V
s is Element of bool (bool the carrier of V)
union s is Element of bool the carrier of V
c₅ is non empty ext-real positive non negative complex real Element of REAL
{ (b₁ * w) where b₁ is ext-real complex real Element of REAL : not c₅ <= abs b₁ } is set
Int w is open Element of bool the carrier of V
{ (b₁ * (Int w)) where b₁ is non empty ext-real complex real Element of REAL : not c₅ <= abs b₁ } is set
c₈ is ext-real complex real set
Y is ext-real complex real Element of REAL
Y * (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 . (Y,(0. V)) is set
Y * (Int w) is Element of bool the carrier of V
{ (Y * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
a is set
a is non empty ext-real complex real Element of REAL
a * (Int w) is Element of bool the carrier of V
{ (a * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
abs a is ext-real complex real Element of REAL
abs Y is ext-real complex real Element of REAL
union { (b₁ * (Int w)) where b₁ is non empty ext-real complex real Element of REAL : not c₅ <= abs b₁ } is set
a is Element of bool (bool the carrier of V)
union a is Element of bool the carrier of V
a is set
v is set
a is non empty ext-real complex real Element of REAL
a * (Int w) is Element of bool the carrier of V
{ (a * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
abs a is ext-real complex real Element of REAL
a * w is Element of bool the carrier of V
{ (a * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
y is Element of the carrier of V
a * y is Element of the carrier of V
the Mult of V . (a,y) is set
Int (union a) is open Element of bool the carrier of V
Int (union s) is open Element of bool the carrier of V
a is Element of bool the carrier of V
v is non empty ext-real complex real Element of REAL
v * (Int w) is Element of bool the carrier of V
{ (v * b₁) where b₁ is Element of the carrier of V : b₁ in Int w } is set
abs v is ext-real complex real Element of REAL
W is ext-real complex real Element of REAL
abs W is ext-real complex real Element of REAL
W * (union s) is Element of bool the carrier of V
{ (W * b₁) where b₁ is Element of the carrier of V : b₁ in union s } is set
(abs W) * c₅ is ext-real complex real Element of REAL
c₈ is set
Y is Element of the carrier of V
W * Y 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,Y) is set
a is set
a is ext-real complex real Element of REAL
a * w is Element of bool the carrier of V
{ (a * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
abs a is ext-real complex real Element of REAL
v is Element of the carrier of V
a * v is Element of the carrier of V
the Mult of V . (a,v) is set
W * a is ext-real complex real Element of REAL
(W * a) * v is Element of the carrier of V
the Mult of V . ((W * a),v) is set
(W * a) * w is Element of bool the carrier of V
{ ((W * a) * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
(abs W) * (abs a) is ext-real complex real Element of REAL
abs (W * a) is ext-real complex real Element of REAL
abs (W * a) is ext-real complex real Element of REAL
W is set
c₈ is Element of the carrier of V
Y is set
a is ext-real complex real Element of REAL
a * w is Element of bool the carrier of V
{ (a * b₁) where b₁ is Element of the carrier of V : b₁ in w } is set
abs a is ext-real complex real Element of REAL
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is non empty a_neighborhood of 0. V
0 * (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 . (0,(0. V)) is set
w is non empty ext-real positive non negative complex real Element of REAL
s is non empty a_neighborhood of 0. V
{ (b₁ * s) where b₁ is ext-real complex real Element of REAL : not w <= abs b₁ } is set
bool the carrier of V is non empty Element of bool (bool the carrier of V)
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
U is set
W is ext-real complex real Element of REAL
W * s is Element of bool the carrier of V
{ (W * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
abs W is ext-real complex real Element of REAL
U is Element of bool (bool the carrier of V)
union U is 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 - 0 is ext-real complex real Element of REAL
abs (W - 0) is ext-real complex real Element of REAL
W * s is Element of bool the carrier of V
{ (W * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
v is non empty a_neighborhood of 0. V
(V,v) is Element of bool the carrier of V
bool the carrier of V is non empty set
(- 1) * v is Element of bool the carrier of V
{ ((- 1) * b₁) where b₁ is Element of the carrier of V : b₁ in v } is set
v /\ (V,v) is Element of bool the carrier of V
s is non empty a_neighborhood of 0. V
c₅ is ext-real complex real Element of REAL
abs c₅ is ext-real complex real Element of REAL
c₅ * s is Element of bool the carrier of V
{ (c₅ * b₁) where b₁ is Element of the carrier of V : b₁ in s } is set
U is set
W is Element of the carrier of V
c₅ * 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 . (c₅,W) is set
- c₅ is ext-real complex real Element of REAL
(- c₅) * W is Element of the carrier of V
the Mult of V . ((- c₅),W) is set
1 - (- c₅) is ext-real complex real Element of REAL
(1 - (- c₅)) * (0. V) is Element of the carrier of V
the Mult of V . ((1 - (- c₅)),(0. V)) is set
((- c₅) * W) + ((1 - (- c₅)) * (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 . (((- c₅) * W),((1 - (- c₅)) * (0. V))) is Element of the carrier of V
((- c₅) * W) + (0. V) is Element of the carrier of V
the addF of V . (((- c₅) * W),(0. V)) is Element of the carrier of V
c₈ is Element of the carrier of V
(- 1) * c₈ is Element of the carrier of V
the Mult of V . ((- 1),c₈) is set
(- 1) * c₅ is ext-real complex real Element of REAL
((- 1) * c₅) * W is Element of the carrier of V
the Mult of V . (((- 1) * c₅),W) is set
(- 1) * (((- 1) * c₅) * W) is Element of the carrier of V
the Mult of V . ((- 1),(((- 1) * c₅) * W)) is set
(- 1) * ((- 1) * c₅) is ext-real complex real Element of REAL
((- 1) * ((- 1) * c₅)) * W is Element of the carrier of V
the Mult of V . (((- 1) * ((- 1) * c₅)),W) is set
(- 1) * (- 1) is non empty ext-real positive non negative complex real Element of REAL
((- 1) * (- 1)) * c₈ is Element of the carrier of V
the Mult of V . (((- 1) * (- 1)),c₈) is set
(- 1) * ((- 1) * c₈) is Element of the carrier of V
the Mult of V . ((- 1),((- 1) * c₈)) is set
(- c₅) * (- 1) is ext-real complex real Element of REAL
((- c₅) * (- 1)) * W is Element of the carrier of V
the Mult of V . (((- c₅) * (- 1)),W) is set
1 - c₅ is ext-real complex real Element of REAL
(1 - c₅) * (0. V) is Element of the carrier of V
the Mult of V . ((1 - c₅),(0. V)) is set
(c₅ * W) + ((1 - c₅) * (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 . ((c₅ * W),((1 - c₅) * (0. V))) is Element of the carrier of V
(c₅ * W) + (0. V) is Element of the carrier of V
the addF of V . ((c₅ * W),(0. V)) is Element of the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
v is Element of bool (bool the carrier of V)
w is Element of bool (bool the carrier of V)
s is non empty a_neighborhood of 0. V
c₅ is non empty a_neighborhood of 0. V
s is Element of bool the carrier of V
V is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V141() () () ()
0. V is zero Element of the carrier of V
the carrier of V is non empty set
the ZeroF of V is Element of the carrier of V
bool the carrier of V is non empty set
bool (bool the carrier of V) is non empty set
v is Element of bool (bool the carrier of V)
w is Element of bool (bool the carrier of V)
s is non empty a_neighborhood of 0. V
c₅ is basis of 0. V
U is non empty a_neighborhood of 0. V
W is non empty a_neighborhood of 0. V
s 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
v is Element of the carrier of V
w is Element of the carrier of V
(V,v,w) is non empty convex Element of bool the carrier of V
bool the carrier of V is non empty set
{ (((1 - b₁) * v) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
1 - 0 is non empty ext-real positive non negative complex real Element of REAL
(1 - 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 . ((1 - 0),v) is set
0. V is zero Element of the carrier of V
the ZeroF of V is Element of the carrier of V
((1 - 0) * 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 . (((1 - 0) * v),(0. V)) is Element of the carrier of V
0 * w is Element of the carrier of V
the Mult of V . (0,w) is set
((1 - 0) * v) + (0 * w) is Element of the carrier of V
the addF of V . (((1 - 0) * v),(0 * w)) is Element of the carrier of V
1 / 2 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 + 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
(1 / 2) * (v + 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 / 2),(v + w)) is set
(V,v,w) is non empty convex Element of bool the carrier of V
bool the carrier of V is non empty set
{ (((1 - b₁) * v) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
1 - (1 / 2) is ext-real complex real Element of REAL
(1 - (1 / 2)) * v is Element of the carrier of V
the Mult of V . ((1 - (1 / 2)),v) is set
(1 / 2) * w is Element of the carrier of V
the Mult of V . ((1 / 2),w) is set
((1 - (1 / 2)) * v) + ((1 / 2) * w) is Element of the carrier of V
the addF of V . (((1 - (1 / 2)) * v),((1 / 2) * w)) is Element of 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
v is Element of the carrier of V
(V,v,v) is non empty convex Element of bool the carrier of V
bool the carrier of V is non empty set
{ (((1 - b₁) * v) + (b₁ * v)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
{v} is non empty Element of bool the carrier of V
w is set
s is ext-real complex real Element of REAL
1 - s is ext-real complex real Element of REAL
(1 - s) * 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 - s),v) is set
s * v is Element of the carrier of V
the Mult of V . (s,v) is set
((1 - s) * v) + (s * 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 . (((1 - s) * v),(s * v)) is Element of the carrier of V
(1 - s) + s is ext-real complex real Element of REAL
((1 - s) + s) * v is Element of the carrier of V
the Mult of V . (((1 - s) + s),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
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 the carrier of V
w is Element of the carrier of V
(V,v,w) is non empty convex Element of bool the carrier of V
bool the carrier of V is non empty set
{ (((1 - b₁) * v) + (b₁ * w)) where b₁ is ext-real complex real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
s is ext-real complex real Element of REAL
1 - s is ext-real complex real Element of REAL
(1 - s) * 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 - s),v) is set
s * w is Element of the carrier of V
the Mult of V . (s,w) is set
((1 - s) * 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 . (((1 - s) * v),(s * w)) is Element of the carrier of V
- (s * w) is Element of 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 . ((- s),w) is set
(- s) " is ext-real complex real Element of REAL
((- s) ") * (1 - s) is ext-real complex real Element of REAL
c₅ is ext-real complex real Element of REAL
c₅ * w is Element of the carrier of V
the Mult of V . (c₅,w) is set
c₅ * v is Element of the carrier of V
the Mult of V . (c₅,v) is set
1 * w is Element of the carrier of V
the Mult of V . (1,w) is set
((- s) ") * (- s) is ext-real complex real Element of REAL
(((- s) ") * (- s)) * w is Element of the carrier of V
the Mult of V . ((((- s) ") * (- s)),w) is set
((- s) ") * ((- s) * w) is Element of the carrier of V
the Mult of V . (((- s) "),((- s) * w)) is set
(- s) * v is Element of the carrier of V
the Mult of V . ((- s),v) is set