:: CONVEX3 semantic presentation

REAL is non empty V5() non finite set

NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal Element of K32(REAL)

K32(REAL) is V5() non finite set

NAT is non empty V5() V17() V18() V19() non finite cardinal limit_cardinal set

K32(NAT) is V5() non finite set

K32(NAT) is V5() non finite set

K149(NAT) is V33() set

COMPLEX is non empty V5() non finite set

RAT is non empty V5() non finite set

INT is non empty V5() non finite set

K33(REAL,REAL) is V5() non finite set

K32(K33(REAL,REAL)) is V5() non finite set

{} is empty V17() V18() V19() V21() V22() V23() V24() V25() finite V38() cardinal {} -element ext-real non positive non negative set

2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of NAT

K33(COMPLEX,COMPLEX) is V5() non finite set

K32(K33(COMPLEX,COMPLEX)) is V5() non finite set

K33(K33(COMPLEX,COMPLEX),COMPLEX) is V5() non finite set

K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is V5() non finite set

K33(K33(REAL,REAL),REAL) is V5() non finite set

K32(K33(K33(REAL,REAL),REAL)) is V5() non finite set

K33(RAT,RAT) is V5() non finite set

K32(K33(RAT,RAT)) is V5() non finite set

K33(K33(RAT,RAT),RAT) is V5() non finite set

K32(K33(K33(RAT,RAT),RAT)) is V5() non finite set

K33(INT,INT) is V5() non finite set

K32(K33(INT,INT)) is V5() non finite set

K33(K33(INT,INT),INT) is V5() non finite set

K32(K33(K33(INT,INT),INT)) is V5() non finite set

K33(NAT,NAT) is V5() non finite set

K33(K33(NAT,NAT),NAT) is V5() non finite set

K32(K33(K33(NAT,NAT),NAT)) is V5() non finite set

1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of NAT

0 is empty V17() V18() V19() V21() V22() V23() V24() V25() finite V38() cardinal {} -element ext-real non positive non negative Element of NAT

Seg 1 is Element of K32(NAT)

{1} is non empty V5() finite V38() 1 -element set

Seg 2 is Element of K32(NAT)

{1,2} is non empty finite V38() set

3 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of NAT

Seg 3 is Element of K32(NAT)

K5(1,2,3) is finite 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

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

M is set

N 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

K32( the carrier of V) is set

M is non empty Element of K32( the carrier of V)

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

N is set

r 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

K32( the carrier of V) is set

M is Element of the carrier of V

{M} is non empty V5() finite 1 -element Element of K32( the carrier of V)

N is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {M}

N . M is V24() V25() ext-real Element of REAL

Carrier N is finite Element of K32( the carrier of V)

Sum N is Element of the carrier of V

r is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng r is set

N (#) r is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (N (#) r) is Element of the carrier of V

<*M*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

r . 1 is set

len r is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

v is Relation-like Function-like FinSequence-like set

len v is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

dom v is Element of K32(NAT)

v . 1 is set

N . (r . 1) is V24() V25() ext-real set

<*1*> is Relation-like NAT -defined NAT -valued Function-like FinSequence-like V50() V51() V52() V53() FinSequence of NAT

rng v is set

{1} is non empty V5() finite V38() 1 -element Element of K32(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

u is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . u is V24() V25() ext-real set

r . u is set

N . (r . u) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

u is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is non empty Element of K32( the carrier of V)

Sum u is Element of the carrier of V

1 * M is Element of the carrier of V

L2 is non empty Element of K32( 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

K32( the carrier of V) is set

M is Element of the carrier of V

N is Element of the carrier of V

{M,N} is non empty finite Element of K32( the carrier of V)

1 / 2 is V24() V25() ext-real non negative Element of REAL

r is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {M,N}

r . M is V24() V25() ext-real Element of REAL

r . N is V24() V25() ext-real Element of REAL

Carrier r is finite Element of K32( the carrier of V)

Sum r is Element of the carrier of V

v is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng v is set

r (#) v is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (r (#) v) is Element of the carrier of V

len v is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

L2 is Relation-like Function-like FinSequence-like set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

dom L2 is Element of K32(NAT)

L2 . 2 is set

v . 2 is set

r . (v . 2) is V24() V25() ext-real set

L2 . 1 is set

v . 1 is set

r . (v . 1) is V24() V25() ext-real set

<*M,N*> is set

<*(1 / 2),(1 / 2)*> is set

<*(1 / 2)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 2)*> ^ <*(1 / 2)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng L2 is set

rng <*(1 / 2)*> is V60() V61() V62() Element of K32(REAL)

(rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) is Element of K32(REAL)

{(1 / 2)} is non empty V5() finite 1 -element Element of K32(REAL)

u is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom u is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

u . L2 is V24() V25() ext-real set

v . L2 is set

r . (v . L2) is V24() V25() ext-real set

len u is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len u) is Element of K32(NAT)

Sum u is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,u,K417()) is V24() V25() ext-real Element of REAL

(1 / 2) + (1 / 2) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is non empty Element of K32( the carrier of V)

<*N,M*> is set

<*(1 / 2),(1 / 2)*> is set

<*(1 / 2)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 2)*> ^ <*(1 / 2)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng L2 is set

rng <*(1 / 2)*> is V60() V61() V62() Element of K32(REAL)

(rng <*(1 / 2)*>) \/ (rng <*(1 / 2)*>) is Element of K32(REAL)

{(1 / 2)} is non empty V5() finite 1 -element Element of K32(REAL)

u is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom u is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

u . L2 is V24() V25() ext-real set

v . L2 is set

r . (v . L2) is V24() V25() ext-real set

len u is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len u) is Element of K32(NAT)

Sum u is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,u,K417()) is V24() V25() ext-real Element of REAL

(1 / 2) + (1 / 2) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is non empty Element of K32( the carrier of V)

<*M,N*> is set

<*N,M*> is set

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination 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

K32( the carrier of V) is set

M is Element of the carrier of V

N is Element of the carrier of V

r is Element of the carrier of V

{M,N,r} is finite Element of K32( the carrier of V)

1 / 3 is V24() V25() ext-real non negative Element of REAL

v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {M,N,r}

v . M is V24() V25() ext-real Element of REAL

v . N is V24() V25() ext-real Element of REAL

v . r is V24() V25() ext-real Element of REAL

Carrier v is finite Element of K32( the carrier of V)

Sum v is Element of the carrier of V

L2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng L2 is set

v (#) L2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

Sum (v (#) L2) is Element of the carrier of V

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

u is Relation-like Function-like FinSequence-like set

len u is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

dom u is Element of K32(NAT)

L2 is set

L2 is Element of the carrier of V

u . 2 is set

L2 . 2 is set

v . (L2 . 2) is V24() V25() ext-real set

u . 3 is set

L2 . 3 is set

v . (L2 . 3) is V24() V25() ext-real set

u . 1 is set

L2 . 1 is set

v . (L2 . 1) is V24() V25() ext-real set

<*M,N,r*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*M,r,N*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*N,M,r*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*N,r,M*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*r,M,N*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*r,N,M*> is set

<*(1 / 3),(1 / 3),(1 / 3)*> is set

<*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(1 / 3)*> ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(<*(1 / 3)*> ^ <*(1 / 3)*>) ^ <*(1 / 3)*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

rng u is set

rng (<*(1 / 3)*> ^ <*(1 / 3)*>) is V60() V61() V62() Element of K32(REAL)

rng <*(1 / 3)*> is V60() V61() V62() Element of K32(REAL)

(rng (<*(1 / 3)*> ^ <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

(rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

((rng <*(1 / 3)*>) \/ (rng <*(1 / 3)*>)) \/ (rng <*(1 / 3)*>) is Element of K32(REAL)

{(1 / 3)} is non empty V5() finite 1 -element Element of K32(REAL)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom L2 is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

L2 . L2 is V24() V25() ext-real set

L2 . L2 is set

v . (L2 . L2) is V24() V25() ext-real set

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len L2) is Element of K32(NAT)

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

(1 / 3) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

((1 / 3) + (1 / 3)) + (1 / 3) is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

c

<*M,N,r*> is set

<*M,r,N*> is set

<*N,M,r*> is set

<*N,r,M*> is set

<*r,M,N*> is set

<*r,N,M*> is set

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination 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

K32( the carrier of V) is set

(V) is set

M is non empty Element of K32( the carrier of V)

{ (Sum b

r is Element of the carrier of V

v is Element of the carrier of V

L2 is V24() V25() ext-real Element of REAL

L2 * r is Element of the carrier of V

1 - L2 is V24() V25() ext-real Element of REAL

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

(L2 * r) + ((1 - L2) * v) is Element of the carrier of V

u is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

Sum u is Element of the carrier of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

Sum L2 is Element of the carrier of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

L2 * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Sum (L2 * L2) is Element of the carrier of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum L2 is Element of the carrier of V

(1 - L2) * (Sum L2) is Element of the carrier of V

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

(1 - L2) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Sum ((1 - L2) * L2) is Element of the carrier of V

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

(L2 * L2) + ((1 - L2) * L2) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Sum ((L2 * L2) + ((1 - L2) * L2)) is Element of 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

K32( the carrier of V) is set

M is non empty Element of K32( the carrier of V)

N is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Carrier N is finite Element of K32( the carrier of V)

card (Carrier N) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

(card (Carrier N)) - 1 is V24() V25() ext-real Element of REAL

r is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng r is set

len r is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

v is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

r . v is set

r . L2 is set

Seg (len r) is Element of K32(NAT)

dom r is Element of K32(NAT)

v is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

v + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

r . (len r) is set

dom r is Element of K32(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

dom L2 is Element of K32(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

len L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Sum L2 is V24() V25() ext-real Element of REAL

K417() is Relation-like K33(REAL,REAL) -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(K33(REAL,REAL),REAL))

K175(REAL,L2,K417()) is V24() V25() ext-real Element of REAL

dom L2 is Element of K32(NAT)

Seg (len L2) is Element of K32(NAT)

r . 1 is set

N . (r . 1) is V24() V25() ext-real set

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

L2 | L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom (L2 | L2) is Element of K32(NAT)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

(L2 | L2) . L2 is V24() V25() ext-real set

Seg L2 is Element of K32(NAT)

L2 | (Seg L2) is Relation-like NAT -defined REAL -valued Function-like V50() V51() V52() Element of K32(K33(NAT,REAL))

K33(NAT,REAL) is V5() non finite set

K32(K33(NAT,REAL)) is V5() non finite set

L2 . L2 is V24() V25() ext-real set

1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

(len r) - 1 is V24() V25() ext-real Element of REAL

Seg L2 is Element of K32(NAT)

L2 | (Seg L2) is Relation-like NAT -defined REAL -valued Function-like V50() V51() V52() Element of K32(K33(NAT,REAL))

K33(NAT,REAL) is V5() non finite set

K32(K33(NAT,REAL)) is V5() non finite set

dom (L2 | (Seg L2)) is set

(L2 | L2) . 1 is V24() V25() ext-real set

L2 . 1 is V24() V25() ext-real set

Sum (L2 | L2) is V24() V25() ext-real Element of REAL

K175(REAL,(L2 | L2),K417()) is V24() V25() ext-real Element of REAL

L2 . (len L2) is V24() V25() ext-real set

rng L2 is V60() V61() V62() Element of K32(REAL)

L2 /^ L2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

(L2 | L2) ^ (L2 /^ L2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

r | L2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

dom (r | L2) is Element of K32(NAT)

c

x is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

(r | L2) /. c

(r | L2) /. x is Element of the carrier of V

r /. c

r /. x is Element of the carrier of V

u is Element of the carrier of V

{u} is non empty V5() finite 1 -element Element of K32( the carrier of V)

x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

Sum x is Element of the carrier of V

L2 is V24() V25() ext-real Element of REAL

1 - L2 is V24() V25() ext-real Element of REAL

1 / (1 - L2) is V24() V25() ext-real Element of REAL

(rng r) \ {u} is Element of K32((rng r))

K32((rng r)) is set

LL is set

N . LL is V24() V25() ext-real set

(1 / (1 - L2)) * (N . LL) is V24() V25() ext-real Element of REAL

LL is Relation-like Function-like set

dom LL is set

rng LL is set

x1 is set

L2 is set

LL . L2 is set

f2 is Element of the carrier of V

N . f2 is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * (N . f2) is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * N is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

((1 / (1 - L2)) * N) . f2 is V24() V25() ext-real Element of REAL

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

(Carrier N) \ {u} is finite Element of K32( the carrier of V)

x1 is finite Element of K32( the carrier of V)

L2 is Element of the carrier of V

LL . L2 is set

L2 is finite Element of K32( the carrier of V)

x1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Carrier x1 is finite Element of K32( the carrier of V)

(Carrier N) \ {u} is finite Element of K32( the carrier of V)

L2 is set

f2 is Element of the carrier of V

x1 . f2 is V24() V25() ext-real Element of REAL

L2 /. (len L2) is V24() V25() ext-real Element of REAL

<*(L2 /. (len L2))*> is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

<*(L2 . (len L2))*> is Relation-like Function-like set

(Sum (L2 | L2)) + L2 is V24() V25() ext-real Element of REAL

L2 + 0 is V24() V25() ext-real Element of REAL

L2 is set

f2 is Element of the carrier of V

N . f2 is V24() V25() ext-real Element of REAL

x1 . f2 is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * (N . f2) is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M

len (r | L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

f2 is Relation-like Function-like FinSequence-like set

len f2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

dom f2 is Element of K32(NAT)

r /^ L2 is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

(r | L2) ^ (r /^ L2) is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

rng (r | L2) is set

rng (r /^ L2) is set

(rng (r | L2)) \/ (rng (r /^ L2)) is set

(Carrier N) \ (rng (r /^ L2)) is finite Element of K32( the carrier of V)

rng f2 is set

f2 is set

L2 is set

f2 . L2 is set

Seg (len f2) is Element of K32(NAT)

L1 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

(r | L2) . L1 is set

L2 . ((r | L2) . L1) is V24() V25() ext-real set

rng L2 is V60() V61() V62() Element of K32(REAL)

c

dom c

rng c

f2 is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

dom f2 is Element of K32(NAT)

Seg (len (r | L2)) is Element of K32(NAT)

len (L2 | L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Seg (len (L2 | L2)) is Element of K32(NAT)

(1 / (1 - L2)) * (L2 | L2) is Relation-like NAT -defined REAL -valued Function-like FinSequence-like V50() V51() V52() FinSequence of REAL

K276((1 / (1 - L2))) is Relation-like REAL -defined REAL -valued Function-like quasi_total V50() V51() V52() Element of K32(K33(REAL,REAL))

(L2 | L2) (#) K276((1 / (1 - L2))) is Relation-like V50() V51() V52() set

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

f2 . L2 is V24() V25() ext-real set

((1 / (1 - L2)) * (L2 | L2)) . L2 is V24() V25() ext-real set

(r | L2) . L2 is set

L2 . ((r | L2) . L2) is V24() V25() ext-real set

(dom L2) /\ (Seg L2) is Element of K32(NAT)

r | (Seg L2) is Relation-like NAT -defined the carrier of V -valued Function-like Element of K32(K33(NAT, the carrier of V))

K33(NAT, the carrier of V) is V5() non finite set

K32(K33(NAT, the carrier of V)) is V5() non finite set

r . L2 is set

L1 is Element of the carrier of V

L2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

dom (r | (Seg L2)) is set

(L2 | L2) . L2 is V24() V25() ext-real set

L2 . L2 is V24() V25() ext-real set

N . (r . L2) is V24() V25() ext-real set

N . ((r | L2) . L2) is V24() V25() ext-real set

(1 / (1 - L2)) * ((L2 | L2) . L2) is V24() V25() ext-real Element of REAL

L2 . L1 is V24() V25() ext-real Element of REAL

N . L1 is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * (N . L1) is V24() V25() ext-real Element of REAL

N . L1 is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * ((L2 | L2) . L2) is V24() V25() ext-real Element of REAL

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

f2 . L2 is V24() V25() ext-real set

(r | L2) . L2 is set

L2 . ((r | L2) . L2) is V24() V25() ext-real set

r /. (len r) is Element of the carrier of V

<*(r /. (len r))*> is Relation-like NAT -defined the carrier of V -valued Function-like FinSequence-like FinSequence of the carrier of V

<*(r . (len r))*> is Relation-like Function-like set

Carrier L2 is finite Element of K32( the carrier of V)

L2 is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

f2 . L2 is V24() V25() ext-real set

((1 / (1 - L2)) * (L2 | L2)) . L2 is V24() V25() ext-real set

dom ((1 / (1 - L2)) * (L2 | L2)) is Element of K32(NAT)

Sum f2 is V24() V25() ext-real Element of REAL

K175(REAL,f2,K417()) is V24() V25() ext-real Element of REAL

(1 / (1 - L2)) * (1 - L2) is V24() V25() ext-real Element of REAL

(1 - L2) / (1 - L2) is V24() V25() ext-real Element of REAL

1 / ((1 - L2) / (1 - L2)) is V24() V25() ext-real Element of REAL

1 / 1 is V24() V25() ext-real non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

card {u} is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of NAT

(card (Carrier N)) - (card {u}) is V24() V25() ext-real set

L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

c

Carrier L1 is finite Element of K32( the carrier of V)

L2 * L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(1 - L2) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(L2 * L1) + ((1 - L2) * L2) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

c

N . c

((L2 * L1) + ((1 - L2) * L2)) . c

(L2 * L1) . c

((1 - L2) * L2) . c

((L2 * L1) . c

L2 . c

(1 - L2) * (L2 . c

L1 . c

L2 * (L1 . c

L1 . c

L2 * (L1 . c

L2 . c

(1 / (1 - L2)) * (N . c

(1 - L2) * (L2 . c

(1 - L2) * (1 / (1 - L2)) is V24() V25() ext-real Element of REAL

((1 - L2) * (1 / (1 - L2))) * (N . c

(1 / ((1 - L2) / (1 - L2))) * (N . c

1 * (N . c

L1 . c

L2 * (L1 . c

L2 . c

(1 - L2) * (L2 . c

0 + 0 is empty V17() V18() V19() V21() V22() V23() V24() V25() finite V38() cardinal {} -element ext-real non positive non negative Element of REAL

card (Carrier L1) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

r . (len L2) is set

N . (r . (len L2)) is V24() V25() ext-real 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

K32( the carrier of V) is set

(V) is set

M is non empty Element of K32( the carrier of V)

{ (Sum b

r is set

v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum v is Element of the carrier of V

Carrier v is finite Element of K32( the carrier of V)

card (Carrier v) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

u is set

{u} is non empty V5() finite 1 -element set

L2 is Element of the carrier of V

{L2} is non empty V5() finite 1 -element Element of K32( the carrier of V)

L2 is Element of the carrier of V

v . L2 is V24() V25() ext-real Element of REAL

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

1 * L2 is Element of the carrier of V

Carrier v is finite Element of K32( the carrier of V)

card (Carrier v) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

u is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Carrier u is finite Element of K32( the carrier of V)

card (Carrier u) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

(card (Carrier u)) - 1 is V24() V25() ext-real Element of REAL

Sum u is Element of the carrier of V

L2 is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

L2 * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

1 - L2 is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - L2) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(L2 * L2) + ((1 - L2) * L2) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

L2 is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

L2 * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

1 - L2 is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - L2) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(L2 * L2) + ((1 - L2) * L2) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

c

{c

Sum L2 is Element of the carrier of V

x is Element of the carrier of V

L2 . x is V24() V25() ext-real Element of REAL

(L2 . x) * x is Element of the carrier of V

{x} is non empty V5() finite 1 -element Element of K32( the carrier of V)

Lu is set

{Lu} is non empty V5() finite 1 -element set

Sum L2 is Element of the carrier of V

LL is Element of the carrier of V

L2 . LL is V24() V25() ext-real Element of REAL

(L2 . LL) * LL is Element of the carrier of V

{LL} is non empty V5() finite 1 -element Element of K32( the carrier of V)

Sum (L2 * L2) is Element of the carrier of V

Sum ((1 - L2) * L2) is Element of the carrier of V

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

L2 * (Sum L2) is Element of the carrier of V

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

(1 - L2) * (Sum L2) is Element of the carrier of V

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

u is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative set

u + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

L2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of NAT

1 + L2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

(card (Carrier v)) - 1 is V24() V25() ext-real Element of REAL

L2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative set

1 + L2 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

L2 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

1 + (L2 + 1) is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

(card (Carrier L2)) - 1 is V24() V25() ext-real Element of REAL

Sum L2 is Element of the carrier of V

Lu is V24() V25() ext-real Element of REAL

c

Lu * c

1 - Lu is V24() V25() ext-real Element of REAL

x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - Lu) * x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(Lu * c

Carrier c

card (Carrier c

Carrier x is finite Element of K32( the carrier of V)

card (Carrier x) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Lu is V24() V25() ext-real Element of REAL

c

Lu * c

1 - Lu is V24() V25() ext-real Element of REAL

x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - Lu) * x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(Lu * c

Carrier c

card (Carrier c

Carrier x is finite Element of K32( the carrier of V)

card (Carrier x) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL

(card (Carrier x)) - 1 is V24() V25() ext-real Element of REAL

Sum x is Element of the carrier of V

L2 is V24() V25() ext-real Element of REAL

LL is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

L2 * LL is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

1 - L2 is V24() V25() ext-real Element of REAL

x1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - L2) * x1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

(L2 * LL) + ((1 - L2) * x1) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Carrier LL is finite Element of K32( the carrier of V)

card (Carrier LL) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Carrier x1 is finite Element of K32( the carrier of V)

card (Carrier x1) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

LL is set

{LL} is non empty V5() finite 1 -element set

Sum c

x1 is Element of the carrier of V

c

(c

{x1} is non empty V5() finite 1 -element Element of K32( the carrier of V)

Sum (Lu * c

Sum ((1 - Lu) * x) is Element of the carrier of V

(Sum (Lu * c

Lu * (Sum c

(Lu * (Sum c

(1 - Lu) * (Sum x) is Element of the carrier of V

(Lu * (Sum c

c

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

c

1 - c

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

(1 - c

(c

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Carrier L2 is finite Element of K32( the carrier of V)

card (Carrier L2) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Carrier v is finite Element of K32( the carrier of V)

card (Carrier v) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

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

K32( the carrier of V) is set

N is non empty V97() V98() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V130() RLSStruct

the carrier of N is non empty set

K32( the carrier of N) is set

M is non empty Element of K32( the carrier of V)

(V) is set

{ (Sum b

r is non empty Element of K32( the carrier of N)

(N) is set

{ (Sum 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

K32( the carrier of V) is set

(V) is set

M is non empty Element of K32( the carrier of V)

conv M is convex Element of K32( the carrier of V)

{ (Sum b

N is set

r is Element of the carrier of V

v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V

Sum v is Element of the carrier of V

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

u is non empty set

L2 is set

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum L2 is Element of the carrier of V

L2 is set

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum L2 is Element of the carrier of V

L2 is Element of K32( the carrier of V)

L2 is Element of the carrier of V

L2 is Element of the carrier of V

c

c

1 - c

(1 - c

(c

x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum x is Element of the carrier of V

Lu is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum Lu is Element of the carrier of V

c

(1 - c

(c

LL is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

Sum LL is Element of the carrier of V

Sum (c

Sum ((1 - c

(Sum (c

c

(c

(1 - c

(c

L2 is set

L2 is Element of the carrier of V

c

Sum c

x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M

V is non empty RLSStruct

the carrier of V is non empty set

K32( the carrier of V) is set

V is non empty RLSStruct

the carrier of V is non empty set

K32( the carrier of V) is set

M is Element of K32( the carrier of V)

N is V24() V25() ext-real Element of REAL

r is Element of the carrier of V

N * r is Element of the carrier of V

V is non empty RLSStruct

the carrier of V is non empty set

K32( the carrier of V) is set

{} V is empty V17() V18() V19() V21() V22() V23() V24() V25() finite V38() cardinal {} -element ext-real non positive non negative Element of K32( the carrier of V)

V is non empty RLSStruct

the carrier of V is non empty set

K32( the carrier of V) is set

N is Element of K32( the carrier of V)

r is (V) Element of K32( 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

K32( the carrier of V) is set

0. V is V79(V) Element of the carrier of V

{(0. V)} is non empty V5() finite 1 -element Element of K32( the carrier of V)

N is Element of K32( the carrier of V)

r is V24() V25() ext-real Element of REAL

v is Element of the carrier of V

r * v is Element of the carrier of V

r is (V) Element of K32( the carrier of V)

V is non empty RLSStruct

the carrier of V is non empty set

K32( the carrier of V) is set

M is (V) Element of K32( the carrier of V)

N is Element of the carrier of V

r is Element of the carrier of V

v is V24() V25() ext-real Element of REAL

v * N is Element of the carrier of V

1 - v is V24() V25() ext-real Element of REAL

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

(v * N) + ((1 - v) * r) is Element of the carrier of V

v + 0 is V24() V25() ext-real Element of REAL

N is Element of the carrier of V

r is Element of the carrier of V

N + r is Element of the carrier of V

1 / 2 is V24() V25() ext-real non negative Element of REAL

(1 / 2) * N is Element of the carrier of V

1 - (1 / 2) is V24() V25() ext-real Element of REAL

(1 - (1 / 2)) * r is Element of the carrier of V

((1 / 2) * N) + ((1 - (1 / 2)) * r) is Element of the carrier of V

(1 / 2) * r is Element of the carrier of V

((1 / 2) * N) + ((1 / 2) * r) is Element of the carrier of V

2 * (((1 / 2) * N) + ((1 / 2) * r)) is Element of the carrier of V

2 * ((1 / 2) * N) is Element of the carrier of V

2 * ((1 / 2) * r) is Element of the carrier of V

(2 * ((1 / 2) * N)) + (2 * ((1 / 2) * r)) is Element of the carrier of V

2 * (1 / 2) is V24() V25() ext-real non negative Element of REAL

(2 * (1 / 2)) * N is Element of the carrier of V

((2 * (1 / 2)) * N) + (2 * ((1 / 2) * r)) is Element of the carrier of V

1 * N is Element of the carrier of V

(2 * (1 / 2)) * r is Element of the carrier of V

(1 * N) + ((2 * (1 / 2)) * r) is Element of the carrier of V

1 * r is Element of the carrier of V

N + (1 * r) is Element of the carrier of V

N is Element of the carrier of V

r is Element of the carrier of V

N + r is Element of the carrier of V

N is Element of the carrier of V

r is Element of the carrier of V

N + r is Element of the carrier of V

v is Element of the carrier of V

L2 is Element of the carrier of V

v + L2 is Element of 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

K32( the carrier of V) is set

M is Element of K32( the carrier of V)

N is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M

Carrier N is finite Element of K32( the carrier of V)

card (Carrier N) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT

Sum N is Element of the carrier of V

(card (Carrier N)) - 1 is V24() V25() ext-real Element of REAL

r is set

v is Element of the carrier of V

{v} is non empty V5() finite 1 -element Element of K32( the carrier of V)

N . v is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {v}

L2 . v is V24() V25() ext-real Element of REAL

Carrier L2 is finite Element of K32( the carrier of V)

u is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M

Carrier u is finite Element of K32( the carrier of V)

L2 is Element of the carrier of V

u . L2 is V24() V25() ext-real Element of REAL

N . L2 is V24() V25() ext-real Element of REAL

(Carrier N) \ {v} is finite Element of K32( the carrier of V)

L2 is set

N . L2 is V24() V25() ext-real set

L2 is Relation-like Function-like set

dom L2 is set

rng L2 is set

L2 is set

L2 is set

L2 . L2 is set

c

N . c

Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL

L2 is finite Element of K32( the carrier of V)

c

L2 . c

L2 is finite Element of K32( the carrier of V)

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

Carrier L2 is finite Element of K32( the carrier of V)

L2 is set

c

L2 . c

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M

Carrier L2 is finite Element of K32( the carrier of V)

c

x is Element of the carrier of V

L2 . x is V24() V25() ext-real Element of REAL

u + L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V

c

N . c

(u + L2) . c