:: RLAFFIN2 semantic presentation

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

{ b

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

{ b

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

{ b

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 b

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

{ b

(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

{ b

(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

{ b

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 b

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

{ b

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

{ b

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

{ b

(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

{ b

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

{ b

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

{ b

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 b

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

{ b

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 b

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

{ b

( not b

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

union { (V,b

BS is Element of bool the carrier of V

{ (V,b

union { (V,b

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

union { (V,b

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

union { (V,b

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

union { (V,b

BS is set

U is non empty Element of bool the carrier of V

ConvexComb V is set

{ (Sum b

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

{ b

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 b

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

union { (V,b

{ (V,b

union { (V,b

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 \ {b

union { (conv (B \ {b

(V,B) \/ (union { (conv (B \ {b

BS is set

{ (V,b

union { (V,b

U is set

x is Element of bool the carrier of V

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

{ (conv (B \ {b

union { (conv (B \ {b

(V,B) \/ (union { (conv (B \ {b

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 \ {b

union { (conv (B \ {b

(V,B) \/ (union { (conv (B \ {b

{ (conv (B \ {b

union { (conv (B \ {b

(V,B) \/ (union { (conv (B \ {b

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 b

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

{ b

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 b

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

{ b

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 b

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