REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V66() non empty-membered V273() V274() V276() set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() non empty-membered V271() V273() Element of bool REAL
bool REAL is non empty non trivial non finite non empty-membered set
1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of NAT
K495(1) is ext-real set
COMPLEX is non empty non trivial non finite complex-membered V66() non empty-membered set
RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V66() non empty-membered set
INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V66() non empty-membered set
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial non finite V50() non empty-membered set
bool [:COMPLEX,COMPLEX:] is non empty non trivial non finite non empty-membered set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial non finite V50() non empty-membered set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial non finite non empty-membered set
[:REAL,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:REAL,REAL:] is non empty non trivial non finite non empty-membered set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial non finite non empty-membered set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:RAT,RAT:] is non empty non trivial non finite non empty-membered set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial non finite non empty-membered set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:INT,INT:] is non empty non trivial non finite non empty-membered set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:[:INT,INT:],INT:] is non empty non trivial non finite non empty-membered set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() V53() non empty-membered set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial non finite V50() V51() V52() V53() non empty-membered set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial non finite non empty-membered set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() non empty-membered V271() V273() set
bool omega is non empty non trivial non finite non empty-membered set
bool NAT is non empty non trivial non finite non empty-membered set
{} is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set
the Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() set
2 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of NAT
[:NAT,REAL:] is Relation-like non empty non trivial non finite V50() V51() V52() non empty-membered set
bool [:NAT,REAL:] is non empty non trivial non finite non empty-membered set
K541() is set
{{}} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() set
{{}} * is functional FinSequence-membered FinSequenceSet of {{}}
[:({{}} *),{{}}:] is Relation-like RAT -valued INT -valued V50() V51() V52() V53() set
bool [:({{}} *),{{}}:] is non empty set
PFuncs (({{}} *),{{}}) is set
0 is Relation-like non-empty empty-yielding RAT -valued empty V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real V30() V31() ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() Element of NAT
Seg 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
{1} is non empty trivial finite V39() 1 -element complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered with_non-empty_elements non empty-membered V271() V272() V273() V274() V275() set
Seg 2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
{1,2} is non empty finite V39() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered with_non-empty_elements non empty-membered V271() V272() V273() V274() V275() set
union {} is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
1 / (1 - V) is V21() real ext-real Element of REAL
1 - (1 / (1 - V)) is V21() real ext-real Element of REAL
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
S is Element of the carrier of B
V * S is Element of the carrier of B
(1 - (1 / (1 - V))) * S is Element of the carrier of B
BS is Element of the carrier of B
(1 - V) * BS is Element of the carrier of B
(V * S) + ((1 - V) * BS) is Element of the carrier of B
U is Element of the carrier of B
(1 / (1 - V)) * U is Element of the carrier of B
((1 / (1 - V)) * U) + ((1 - (1 / (1 - V))) * S) is Element of the carrier of B
U - (V * S) is Element of the carrier of B
1 - 1 is V21() real ext-real Element of REAL
(1 / (1 - V)) * (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) * (V * S) is Element of the carrier of B
(1 / (1 - V)) * V is V21() real ext-real Element of REAL
((1 / (1 - V)) * V) * S is Element of the carrier of B
1 - (1 - V) is V21() real ext-real Element of REAL
(1 - (1 - V)) / (1 - V) is V21() real ext-real Element of REAL
((1 - (1 - V)) / (1 - V)) * S is Element of the carrier of B
(1 - V) / (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) - ((1 - V) / (1 - V)) is V21() real ext-real Element of REAL
((1 / (1 - V)) - ((1 - V) / (1 - V))) * S is Element of the carrier of B
(1 / (1 - V)) - 1 is V21() real ext-real Element of REAL
((1 / (1 - V)) - 1) * S is Element of the carrier of B
1 * BS is Element of the carrier of B
(1 / (1 - V)) * ((1 - V) * BS) is Element of the carrier of B
((1 / (1 - V)) * U) - ((1 / (1 - V)) * (V * S)) is Element of the carrier of B
- (((1 / (1 - V)) - 1) * S) is Element of the carrier of B
((1 / (1 - V)) * U) + (- (((1 / (1 - V)) - 1) * S)) is Element of the carrier of B
- S is Element of the carrier of B
((1 / (1 - V)) - 1) * (- S) is Element of the carrier of B
((1 / (1 - V)) * U) + (((1 / (1 - V)) - 1) * (- S)) is Element of the carrier of B
- ((1 / (1 - V)) - 1) is V21() real ext-real Element of REAL
(- ((1 / (1 - V)) - 1)) * S is Element of the carrier of B
((1 / (1 - V)) * U) + ((- ((1 / (1 - V)) - 1)) * S) is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is Element of bool the carrier of V
S \ {B} is Element of bool the carrier of V
conv (S \ {B}) is convex Element of bool the carrier of V
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Sum BS is Element of the carrier of V
BS . B is V21() real ext-real Element of REAL
(BS . B) * B is Element of the carrier of V
1 - (BS . B) is V21() real ext-real Element of REAL
1 / (BS . B) is V21() real ext-real Element of REAL
(1 / (BS . B)) * (Sum BS) is Element of the carrier of V
1 - (1 / (BS . B)) is V21() real ext-real Element of REAL
Carrier BS is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not BS . b1 = 0 } is set
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {B}
X . B is V21() real ext-real Element of REAL
1 * B is Element of the carrier of V
1 - 1 is V21() real ext-real Element of REAL
y is non empty Element of bool the carrier of V
BS - X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- 1 is non empty V21() real ext-real non positive negative Element of REAL
(- 1) * X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
BS + (- X) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 / (1 - (BS . B)) is V21() real ext-real Element of REAL
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
(1 / (1 - (BS . B))) * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Carrier ((1 / (1 - (BS . B))) * U) is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not ((1 / (1 - (BS . B))) * U) . b1 = 0 } is set
U . B is V21() real ext-real Element of REAL
(BS . B) - (BS . B) is V21() real ext-real Element of REAL
((1 / (1 - (BS . B))) * U) . B is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * ((BS . B) - (BS . B)) is V21() real ext-real Element of REAL
Carrier X is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not X . b1 = 0 } is set
xBS is Element of the carrier of V
((1 / (1 - (BS . B))) * U) . xBS is V21() real ext-real Element of REAL
U . xBS is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * (U . xBS) is V21() real ext-real Element of REAL
BS . xBS is V21() real ext-real Element of REAL
X . xBS is V21() real ext-real Element of REAL
(BS . xBS) - (X . xBS) is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * ((BS . xBS) - (X . xBS)) is V21() real ext-real Element of REAL
sum U is V21() real ext-real Element of REAL
sum BS is V21() real ext-real Element of REAL
sum X is V21() real ext-real Element of REAL
(sum BS) - (sum X) is V21() real ext-real Element of REAL
(sum BS) - (BS . B) is V21() real ext-real Element of REAL
sum ((1 / (1 - (BS . B))) * U) is V21() real ext-real Element of REAL
(1 / (1 - (BS . B))) * (1 - (BS . B)) is V21() real ext-real Element of REAL
xBS is non empty Element of bool the carrier of V
BU is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of xBS
Sum BU is Element of the carrier of V
xU is Element of the carrier of V
(1 - (BS . B)) * xU is Element of the carrier of V
((BS . B) * B) + ((1 - (BS . B)) * xU) is Element of the carrier of V
(1 - (1 / (BS . B))) * xU is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) + ((1 - (1 / (BS . B))) * xU) is Element of the carrier of V
ConvexComb V is set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of xBS : b1 in ConvexComb V } is set
Sum U is Element of the carrier of V
Sum X is Element of the carrier of V
(Sum BS) - (Sum X) is Element of the carrier of V
(Sum BS) - ((BS . B) * B) is Element of the carrier of V
(1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(1 - (BS . B)) * ((1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B))) is Element of the carrier of V
(1 - (BS . B)) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
((1 - (BS . B)) * (1 / (1 - (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
1 * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(BS . B) / (BS . B) is V21() real ext-real Element of REAL
((BS . B) / (BS . B)) - (1 / (BS . B)) is V21() real ext-real Element of REAL
(BS . B) - 1 is V21() real ext-real Element of REAL
((BS . B) - 1) / (BS . B) is V21() real ext-real Element of REAL
- (1 - (BS . B)) is V21() real ext-real Element of REAL
(- (1 - (BS . B))) / (BS . B) is V21() real ext-real Element of REAL
(1 - (BS . B)) / (BS . B) is V21() real ext-real Element of REAL
- ((1 - (BS . B)) / (BS . B)) is V21() real ext-real Element of REAL
(1 - (1 / (BS . B))) * (Sum BU) is Element of the carrier of V
(- ((1 - (BS . B)) / (BS . B))) * ((1 / (1 - (BS . B))) * ((Sum BS) - ((BS . B) * B))) is Element of the carrier of V
(- ((1 - (BS . B)) / (BS . B))) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
((- ((1 - (BS . B)) / (BS . B))) * (1 / (1 - (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B))) is V21() real ext-real Element of REAL
- (((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B)))) is V21() real ext-real Element of REAL
(- (((1 - (BS . B)) / (BS . B)) * (1 / (1 - (BS . B))))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
(1 - (BS . B)) / (1 - (BS . B)) is V21() real ext-real Element of REAL
((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B)) is V21() real ext-real Element of REAL
- (((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (((1 - (BS . B)) / (1 - (BS . B))) * (1 / (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
1 * (1 / (BS . B)) is V21() real ext-real Element of REAL
- (1 * (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (1 * (1 / (BS . B)))) * ((Sum BS) - ((BS . B) * B)) is Element of the carrier of V
- (1 / (BS . B)) is V21() real ext-real Element of REAL
(- (1 / (BS . B))) * (Sum BS) is Element of the carrier of V
(- (1 / (BS . B))) * ((BS . B) * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) - ((- (1 / (BS . B))) * ((BS . B) * B)) is Element of the carrier of V
- ((- (1 / (BS . B))) * ((BS . B) * B)) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (- ((- (1 / (BS . B))) * ((BS . B) * B))) is Element of the carrier of V
- (- (1 / (BS . B))) is V21() real ext-real Element of REAL
(- (- (1 / (BS . B)))) * ((BS . B) * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + ((- (- (1 / (BS . B)))) * ((BS . B) * B)) is Element of the carrier of V
(1 / (BS . B)) * (BS . B) is V21() real ext-real Element of REAL
((1 / (BS . B)) * (BS . B)) * B is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (((1 / (BS . B)) * (BS . B)) * B) is Element of the carrier of V
1 * B is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + (1 * B) is Element of the carrier of V
((- (1 / (BS . B))) * (Sum BS)) + B is Element of the carrier of V
- ((1 / (BS . B)) * (Sum BS)) is Element of the carrier of V
(- ((1 / (BS . B)) * (Sum BS))) + B is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) + (- ((1 / (BS . B)) * (Sum BS))) is Element of the carrier of V
(((1 / (BS . B)) * (Sum BS)) + (- ((1 / (BS . B)) * (Sum BS)))) + B is Element of the carrier of V
((1 / (BS . B)) * (Sum BS)) - ((1 / (BS . B)) * (Sum BS)) is Element of the carrier of V
(((1 / (BS . B)) * (Sum BS)) - ((1 / (BS . B)) * (Sum BS))) + B is Element of the carrier of V
V is V21() real ext-real Element of REAL
1 - V is V21() real ext-real Element of REAL
B is V21() real ext-real Element of REAL
1 - B is V21() real ext-real Element of REAL
S is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of S is non empty set
bool the carrier of S is non empty non empty-membered set
BS is Element of the carrier of S
U is Element of the carrier of S
V * U is Element of the carrier of S
B * U is Element of the carrier of S
x is affinely-independent Element of bool the carrier of S
conv x is convex Element of bool the carrier of S
y is Element of the carrier of S
{y} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of S
x \ {y} is Element of bool the carrier of S
conv (x \ {y}) is convex Element of bool the carrier of S
X is Element of the carrier of S
{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of S
x \ {X} is Element of bool the carrier of S
conv (x \ {X}) is convex Element of bool the carrier of S
U is Element of the carrier of S
xBS is Element of the carrier of S
(1 - V) * U is Element of the carrier of S
(V * U) + ((1 - V) * U) is Element of the carrier of S
(1 - B) * xBS is Element of the carrier of S
(B * U) + ((1 - B) * xBS) is Element of the carrier of S
U |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
BS |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
U |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
xBS |-- x is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
Affin x is Affine Element of bool the carrier of S
(U |-- x) . X is V21() real ext-real Element of REAL
y is set
(U |-- x) . y is V21() real ext-real set
Affin (x \ {X}) is Affine Element of bool the carrier of S
xBS |-- (x \ {X}) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x \ {X}
Carrier (xBS |-- x) is finite Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : not (xBS |-- x) . b1 = 0 } is set
(xBS |-- x) . X is V21() real ext-real Element of REAL
(U |-- x) . y is V21() real ext-real Element of REAL
y is set
(U |-- x) . y is V21() real ext-real set
Affin (x \ {y}) is Affine Element of bool the carrier of S
U |-- (x \ {y}) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x \ {y}
Carrier (U |-- x) is finite Element of bool the carrier of S
{ b1 where b1 is Element of the carrier of S : not (U |-- x) . b1 = 0 } is set
(U |-- x) . y is V21() real ext-real Element of REAL
B * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - B) * (xBS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(B * (U |-- x)) + ((1 - B) * (xBS |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(BS |-- x) . X is V21() real ext-real Element of REAL
(B * (U |-- x)) . X is V21() real ext-real Element of REAL
((1 - B) * (xBS |-- x)) . X is V21() real ext-real Element of REAL
((B * (U |-- x)) . X) + (((1 - B) * (xBS |-- x)) . X) is V21() real ext-real Element of REAL
B * ((U |-- x) . X) is V21() real ext-real Element of REAL
(B * ((U |-- x) . X)) + (((1 - B) * (xBS |-- x)) . X) is V21() real ext-real Element of REAL
(1 - B) * ((xBS |-- x) . X) is V21() real ext-real Element of REAL
(B * ((U |-- x) . X)) + ((1 - B) * ((xBS |-- x) . X)) is V21() real ext-real Element of REAL
1 * ((U |-- x) . X) is V21() real ext-real Element of REAL
((BS |-- x) . X) - ((BS |-- x) . X) is V21() real ext-real Element of REAL
((U |-- x) . X) - ((BS |-- x) . X) is V21() real ext-real Element of REAL
(U |-- x) . X is V21() real ext-real Element of REAL
1 / (1 - B) is V21() real ext-real Element of REAL
((U |-- x) . X) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
(1 / (1 - B)) - (((U |-- x) . X) / (((U |-- x) . X) - ((BS |-- x) . X))) is V21() real ext-real Element of REAL
(1 / (1 - B)) - {} is V21() real ext-real Element of REAL
V * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - V) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(V * (U |-- x)) + ((1 - V) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(BS |-- x) . y is V21() real ext-real Element of REAL
(V * (U |-- x)) . y is V21() real ext-real Element of REAL
((1 - V) * (U |-- x)) . y is V21() real ext-real Element of REAL
((V * (U |-- x)) . y) + (((1 - V) * (U |-- x)) . y) is V21() real ext-real Element of REAL
V * ((U |-- x) . y) is V21() real ext-real Element of REAL
(V * ((U |-- x) . y)) + (((1 - V) * (U |-- x)) . y) is V21() real ext-real Element of REAL
(1 - V) * ((U |-- x) . y) is V21() real ext-real Element of REAL
(V * ((U |-- x) . y)) + ((1 - V) * ((U |-- x) . y)) is V21() real ext-real Element of REAL
1 * ((U |-- x) . y) is V21() real ext-real Element of REAL
((BS |-- x) . y) - ((BS |-- x) . y) is V21() real ext-real Element of REAL
((U |-- x) . y) - ((BS |-- x) . y) is V21() real ext-real Element of REAL
(1 / (1 - B)) * BS is Element of the carrier of S
1 - (1 / (1 - B)) is V21() real ext-real Element of REAL
(1 - (1 / (1 - B))) * U is Element of the carrier of S
((1 / (1 - B)) * BS) + ((1 - (1 / (1 - B))) * U) is Element of the carrier of S
(1 / (1 - B)) * (BS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - (1 / (1 - B))) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((1 / (1 - B)) * (BS |-- x)) + ((1 - (1 / (1 - B))) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((U |-- x) . X) - {} is V21() real ext-real Element of REAL
(((U |-- x) . X) - {}) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
1 / (1 - V) is V21() real ext-real Element of REAL
(1 / (1 - V)) * BS is Element of the carrier of S
1 - (1 / (1 - V)) is V21() real ext-real Element of REAL
(1 - (1 / (1 - V))) * U is Element of the carrier of S
((1 / (1 - V)) * BS) + ((1 - (1 / (1 - V))) * U) is Element of the carrier of S
(1 / (1 - V)) * (BS |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(1 - (1 / (1 - V))) * (U |-- x) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((1 / (1 - V)) * (BS |-- x)) + ((1 - (1 / (1 - V))) * (U |-- x)) is Relation-like the carrier of S -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((U |-- x) . X) - ((U |-- x) . X) is V21() real ext-real Element of REAL
(((U |-- x) . X) - ((U |-- x) . X)) / (((U |-- x) . X) - ((BS |-- x) . X)) is V21() real ext-real Element of REAL
(xBS |-- x) . y is V21() real ext-real Element of REAL
((xBS |-- x) . y) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
(1 / (1 - V)) - (((xBS |-- x) . y) / (((U |-- x) . y) - ((BS |-- x) . y))) is V21() real ext-real Element of REAL
(1 / (1 - V)) - {} is V21() real ext-real Element of REAL
((U |-- x) . y) - {} is V21() real ext-real Element of REAL
(((U |-- x) . y) - {}) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
((U |-- x) . y) - ((xBS |-- x) . y) is V21() real ext-real Element of REAL
(((U |-- x) . y) - ((xBS |-- x) . y)) / (((U |-- x) . y) - ((BS |-- x) . y)) is V21() real ext-real Element of REAL
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is finite Element of bool the carrier of V
S is finite affinely-independent Element of bool the carrier of V
conv S is convex Element of bool the carrier of V
Affin S is Affine Element of bool the carrier of V
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
BS + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
Affin U is Affine Element of bool the carrier of V
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
sum x is V21() real ext-real Element of REAL
Sum x is Element of the carrier of V
(Sum x) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of U : sum b1 = 1 } is set
y is Element of the carrier of V
((Sum x) |-- S) . y is V21() real ext-real Element of REAL
X is set
{X} is non empty trivial finite 1 -element set
U is Element of the carrier of V
x . U is V21() real ext-real Element of REAL
U |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(U |-- S) . y is V21() real ext-real Element of REAL
<*((U |-- S) . y)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
<*U*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
Sum <*((U |-- S) . y)*> is V21() real ext-real Element of REAL
len <*((U |-- S) . y)*> is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom <*((U |-- S) . y)*> is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
len <*U*> is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng <*U*> is Element of bool the carrier of V
(x . U) * U is Element of the carrier of V
xU is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
<*((U |-- S) . y)*> . xU is V21() real ext-real set
<*U*> . xU is set
x . (<*U*> . xU) is V21() real ext-real set
(<*U*> . xU) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((<*U*> . xU) |-- S) . y is V21() real ext-real Element of REAL
(x . (<*U*> . xU)) * (((<*U*> . xU) |-- S) . y) is V21() real ext-real Element of REAL
y is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
rng y is Element of bool the carrier of V
x * y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum (x * y) is V21() real ext-real Element of REAL
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (dom y) is epsilon-transitive epsilon-connected ordinal cardinal set
len y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
Seg (len y) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
card (Seg (len y)) is epsilon-transitive epsilon-connected ordinal cardinal set
len (x * y) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
(len y) |-> 1 is Relation-like NAT -defined NAT -valued Function-like len y -element FinSequence-like V50() V51() V52() V53() Element of (len y) -tuples_on NAT
(len y) -tuples_on NAT is functional non empty FinSequence-membered FinSequenceSet of NAT
len ((len y) |-> 1) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
Sum ((len y) |-> 1) is V21() set
(len y) * 1 is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal Element of REAL
X is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
((len y) |-> 1) . X is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
(x * y) . X is V21() real ext-real set
y . X is set
x . (y . X) is V21() real ext-real set
y is Element of the carrier of V
x . y is V21() real ext-real Element of REAL
y is Element of the carrier of V
x . y is V21() real ext-real Element of REAL
1 - (x . y) is V21() real ext-real Element of REAL
{y} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of {y}
U . y is V21() real ext-real Element of REAL
x - U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
- 1 is non empty V21() real ext-real non positive negative Element of REAL
(- 1) * U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
x + (- U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
1 / (1 - (x . y)) is V21() real ext-real Element of REAL
(1 / (1 - (x . y))) * (x - U) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
Carrier U is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not U . b1 = 0 } is set
sum U is V21() real ext-real Element of REAL
sum (x - U) is V21() real ext-real Element of REAL
sum ((1 / (1 - (x . y))) * (x - U)) is V21() real ext-real Element of REAL
(1 / (1 - (x . y))) * (1 - (x . y)) is V21() real ext-real Element of REAL
(x - U) . y is V21() real ext-real Element of REAL
(x . y) - (U . y) is V21() real ext-real Element of REAL
Carrier (x - U) is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not (x - U) . b1 = 0 } is set
U \ {y} is finite Element of bool the carrier of V
card (U \ {y}) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
Sum U is Element of the carrier of V
(x . y) * y is Element of the carrier of V
xU is set
p is Element of the carrier of V
x . p is V21() real ext-real Element of REAL
(x - U) . p is V21() real ext-real Element of REAL
U . p is V21() real ext-real Element of REAL
(x . p) - (U . p) is V21() real ext-real Element of REAL
xU is Element of the carrier of V
((Sum x) |-- S) . xU is V21() real ext-real Element of REAL
1 * (1 - (x . y)) is V21() real ext-real Element of REAL
(1 * (1 - (x . y))) / (1 - (x . y)) is V21() real ext-real Element of REAL
Sum ((1 / (1 - (x . y))) * (x - U)) is Element of the carrier of V
Sum (x - U) is Element of the carrier of V
(1 / (1 - (x . y))) * (Sum (x - U)) is Element of the carrier of V
(1 - (x . y)) * (Sum ((1 / (1 - (x . y))) * (x - U))) is Element of the carrier of V
(1 - (x . y)) * (1 / (1 - (x . y))) is V21() real ext-real Element of REAL
((1 - (x . y)) * (1 / (1 - (x . y)))) * (Sum (x - U)) is Element of the carrier of V
((1 - (x . y)) * (Sum ((1 / (1 - (x . y))) * (x - U)))) + ((x . y) * y) is Element of the carrier of V
(Sum x) - ((x . y) * y) is Element of the carrier of V
((Sum x) - ((x . y) * y)) + ((x . y) * y) is Element of the carrier of V
U \/ {y} is non empty finite Element of bool the carrier of V
Carrier ((1 / (1 - (x . y))) * (x - U)) is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not ((1 / (1 - (x . y))) * (x - U)) . b1 = 0 } is set
(Sum ((1 / (1 - (x . y))) * (x - U))) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU is V21() real ext-real Element of REAL
p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum p is V21() real ext-real Element of REAL
u is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len u is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
len p is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng u is Element of bool the carrier of V
dom p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
(1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
y |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
(x . y) * (y |-- S) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) + ((x . y) * (y |-- S)) is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
(1 - (x . y)) * p is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
(y |-- S) . xU is V21() real ext-real Element of REAL
(x . y) * ((y |-- S) . xU) is V21() real ext-real Element of REAL
<*((x . y) * ((y |-- S) . xU))*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
((1 - (x . y)) * p) ^ <*((x . y) * ((y |-- S) . xU))*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
y is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL
Sum y is V21() real ext-real Element of REAL
len y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
dom y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
<*y*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
u ^ <*y*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
x is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V
len x is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
rng x is Element of bool the carrier of V
Sum ((1 - (x . y)) * p) is V21() real ext-real Element of REAL
(Sum ((1 - (x . y)) * p)) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
(1 - (x . y)) * (((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU) is V21() real ext-real Element of REAL
((1 - (x . y)) * (((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S) . xU)) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU is V21() real ext-real Element of REAL
(((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU) + ((x . y) * ((y |-- S) . xU)) is V21() real ext-real Element of REAL
((x . y) * (y |-- S)) . xU is V21() real ext-real Element of REAL
(((1 - (x . y)) * ((Sum ((1 / (1 - (x . y))) * (x - U))) |-- S)) . xU) + (((x . y) * (y |-- S)) . xU) is V21() real ext-real Element of REAL
(len p) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
x is Relation-like NAT -defined REAL -valued Function-like len p -element FinSequence-like V50() V51() V52() Element of (len p) -tuples_on REAL
(1 - (x . y)) * x is Relation-like NAT -defined REAL -valued Function-like len p -element FinSequence-like V50() V51() V52() Element of (len p) -tuples_on REAL
len ((1 - (x . y)) * x) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of NAT
(len p) + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
rng <*y*> is Element of bool the carrier of V
(U \ {y}) \/ {y} is non empty finite Element of bool the carrier of V
p is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
y . p is V21() real ext-real set
x . p is set
x . (x . p) is V21() real ext-real set
(x . p) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((x . p) |-- S) . xU is V21() real ext-real Element of REAL
(x . (x . p)) * (((x . p) |-- S) . xU) is V21() real ext-real Element of REAL
((1 - (x . y)) * x) . p is V21() real ext-real set
x . p is V21() real ext-real set
(1 - (x . y)) * (x . p) is V21() real ext-real Element of REAL
p . p is V21() real ext-real set
u . p is set
((1 / (1 - (x . y))) * (x - U)) . (u . p) is V21() real ext-real set
(u . p) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
((u . p) |-- S) . xU is V21() real ext-real Element of REAL
(((1 / (1 - (x . y))) * (x - U)) . (u . p)) * (((u . p) |-- S) . xU) is V21() real ext-real Element of REAL
dom u is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
U . (u . p) is V21() real ext-real set
(x - U) . (u . p) is V21() real ext-real set
x . (u . p) is V21() real ext-real set
(x . (u . p)) - {} is V21() real ext-real set
(1 / (1 - (x . y))) * (x . (u . p)) is V21() real ext-real Element of REAL
((1 / (1 - (x . y))) * (x - U)) . (x . p) is V21() real ext-real set
(1 - (x . y)) * (((1 / (1 - (x . y))) * (x - U)) . (x . p)) is V21() real ext-real Element of REAL
((1 - (x . y)) * (1 / (1 - (x . y)))) * (x . (u . p)) is V21() real ext-real Element of REAL
dom ((1 - (x . y)) * p) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() Element of bool NAT
BS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
sum BS is V21() real ext-real Element of REAL
Sum BS is Element of the carrier of V
(Sum BS) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
Carrier BS is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not BS . b1 = 0 } is set
y is finite Element of bool the carrier of V
card y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
Carrier X is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not X . b1 = 0 } is set
sum X is V21() real ext-real Element of REAL
Sum X is Element of the carrier of V
(Sum X) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
{} the carrier of V is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() affinely-independent V273() V274() V275() V276() Element of bool the carrier of V
ZeroLC V is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of V
U is Element of the carrier of V
((Sum X) |-- S) . U is V21() real ext-real Element of REAL
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of Carrier BS
sum x is V21() real ext-real Element of REAL
card (Carrier BS) is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
y is finite Element of bool the carrier of V
card y is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
Carrier X is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not X . b1 = 0 } is set
sum X is V21() real ext-real Element of REAL
Sum X is Element of the carrier of V
(Sum X) |-- S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S
U is Element of the carrier of V
((Sum X) |-- S) . U is V21() real ext-real Element of REAL
y is Element of the carrier of V
((Sum BS) |-- S) . y is V21() real ext-real Element of REAL
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of the carrier of V
{B} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
S is Element of bool the carrier of V
conv S is convex Element of bool the carrier of V
S \ {B} is Element of bool the carrier of V
conv (S \ {B}) is convex Element of bool the carrier of V
BS is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
(conv S) /\ (conv BS) is Element of bool the carrier of V
(conv (S \ {B})) /\ (conv BS) is Element of bool the carrier of V
U is Element of bool the carrier of V
x is set
y is non empty Element of bool the carrier of V
ConvexComb V is set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y : b1 in ConvexComb V } is set
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y
Sum X is Element of the carrier of V
X . B is V21() real ext-real Element of REAL
Carrier X is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not X . b1 = 0 } is set
xBS is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of S \ {B}
Sum xBS is Element of the carrier of V
BU is non empty Element of bool the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BU : b1 in ConvexComb V } is set
conv BU is non empty convex Element of bool the carrier of V
(X . B) * B is Element of the carrier of V
1 - (X . B) is V21() real ext-real Element of REAL
1 / (X . B) is V21() real ext-real Element of REAL
(1 / (X . B)) * (Sum X) is Element of the carrier of V
1 - (1 / (X . B)) is V21() real ext-real Element of REAL
xBS is Element of the carrier of V
(1 - (X . B)) * xBS is Element of the carrier of V
((X . B) * B) + ((1 - (X . B)) * xBS) is Element of the carrier of V
(1 - (1 / (X . B))) * xBS is Element of the carrier of V
((1 / (X . B)) * (Sum X)) + ((1 - (1 / (X . B))) * xBS) 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 non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : ( b1 in conv B & ( for b2 being Element of bool the carrier of V holds
( not b2 c< B or not b1 in conv b2 ) ) ) } is set
BS is set
U is Element of the carrier of V
BS is Element of bool the carrier of V
U is set
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
y is Element of the carrier of V
S is Element of bool the carrier of V
BS is Element of bool the carrier of V
U is set
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
x is Element of bool the carrier of V
conv x is convex 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 non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
S is set
V is non empty RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() V273() V274() V275() V276() Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is Relation-like non-empty empty-yielding RAT -valued empty proper V21() epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural real ext-real non positive non negative finite finite-yielding V39() cardinal {} -element V50() V51() V52() V53() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V66() convex V273() V274() V275() V276() 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 non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
V is non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is set
BS is set
{S} is non empty trivial finite 1 -element set
B \ {S} is Element of bool the carrier of V
conv (B \ {S}) is convex Element of bool the carrier of V
S is Element of the carrier of V
{S} is non empty trivial finite 1 -element Element of bool the carrier of V
BS is Element of bool the carrier of V
conv BS is convex Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex 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
BS is set
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= B } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= B } is set
BS is Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= BS } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= BS } is set
conv BS is convex Element of bool the carrier of V
x is set
y is set
X is Element of bool the carrier of V
(V,X) is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
BS is V21() epsilon-transitive epsilon-connected ordinal natural real ext-real non negative finite cardinal set
BS + 1 is non empty V21() epsilon-transitive epsilon-connected ordinal natural real ext-real positive non negative finite cardinal Element of REAL
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
y is set
(V,U) is Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
xBS is set
BU is Element of bool the carrier of V
(V,BU) is Element of bool the carrier of V
X is Element of bool the carrier of V
conv X is convex Element of bool the carrier of V
BS is finite Element of bool the carrier of V
card BS is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv BS is convex Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= BS } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= BS } is set
BS is set
U is non empty Element of bool the carrier of V
ConvexComb V is set
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of U : b1 in ConvexComb V } is set
x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of U
Sum x is Element of the carrier of V
Carrier x is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not x . b1 = 0 } is set
y is non empty finite Element of bool the carrier of V
X is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of y
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of y : b1 in ConvexComb V } is set
conv y is non empty convex Element of bool the carrier of V
card y is non empty V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real positive non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V271() V272() V273() V274() V275() Element of omega
U is finite Element of bool the carrier of V
card U is V21() epsilon-transitive epsilon-connected ordinal natural real V30() V31() ext-real non negative finite cardinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V273() V274() V275() Element of omega
conv U is convex Element of bool the carrier of V
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= U } is set
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= y } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= y } is set
U is set
xBS is Element of bool the carrier of V
(V,xBS) is Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
conv B is convex Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
{ (conv (B \ {b1})) where b1 is Element of the carrier of V : b1 in B } is set
union { (conv (B \ {b1})) where b1 is Element of the carrier of V : b1 in B } is set
(V,B) \/ (union { (conv (B \ {b1})) where b1 is Element of the carrier of V : b1 in B } ) is set
BS is set
{ (V,b1) where b1 is Element of bool the carrier of V : b1 c= B } is set
union { (V,b1) where b1 is Element of bool the carrier of V : b1 c= B } is set
U is set
x is Element of bool the carrier of V
(V,x) is Element of bool the carrier of V
{ (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
(V,B) \/ (union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } ) is set
y is set
X is Element of the carrier of V
{X} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
B \ {X} is Element of bool the carrier of V
conv (B \ {X}) is convex Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
{ (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
(V,B) \/ (union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } ) is set
{ (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } is set
(V,B) \/ (union { (conv (B \ {b2})) where b1 is Element of the carrier of V : b2 in B } ) is set
BS is set
U is set
x is Element of the carrier of V
{x} is non empty trivial finite 1 -element affinely-independent Element of bool the carrier of V
B \ {x} is Element of bool the carrier of V
conv (B \ {x}) is convex Element of bool the carrier of V
V is set
B is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of B is non empty set
bool the carrier of B is non empty non empty-membered set
S is Element of bool the carrier of B
(B,S) is Element of bool the carrier of B
conv S is convex Element of bool the carrier of B
BS is non empty Element of bool the carrier of B
ConvexComb B is set
{ (Sum b1) where b1 is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b1 in ConvexComb B } is set
U is Relation-like the carrier of B -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS
Sum U is Element of the carrier of B
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Sum S is Element of the carrier of V
Carrier S is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not S . b1 = 0 } is set
BS is non empty Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
ConvexComb V is set
Sum U is Element of the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b1 in ConvexComb V } is set
conv BS is non empty convex Element of bool the carrier of V
V is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct
the carrier of V is non empty set
bool the carrier of V is non empty non empty-membered set
B is affinely-independent Element of bool the carrier of V
(V,B) is Element of bool the carrier of V
S is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of B
Carrier S is finite Element of bool the carrier of V
{ b1 where b1 is Element of the carrier of V : not S . b1 = 0 } is set
Sum S is Element of the carrier of V
BS is non empty Element of bool the carrier of V
U is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of BS
ConvexComb V is set
Sum U is Element of the carrier of V
{ (Sum b1) where b1 is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() convex Linear_Combination of BS : b1 in ConvexComb V } is set
conv BS is non empty convex Element of bool the carrier of V
Affin BS is non empty Affine Element of bool the carrier of V
sum S is V21() real ext-real Element of REAL
x is Element of bool the carrier of V
conv x is convex Element of bool the carrier of V
Affin x is Affine Element of bool the carrier of V
(Sum U) |-- x is Relation-like the carrier of V -defined REAL -valued Function-like total quasi_total V50() V51() V52() Linear_Combination of x
(Sum U) |-- B is Relation-like the carrier of V -defined REAL -val