:: 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₁₁ is non empty Element of K32( the carrier of V)
<*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₁₁ is non empty Element of K32( the carrier of V)
<*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₁₁ is non empty Element of K32( the carrier of V)
<*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₁₁ is non empty Element of K32( the carrier of V)
<*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₁₁ is non empty Element of K32( the carrier of V)
<*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₁₁ is non empty Element of K32( the carrier of V)
<*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₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M : b₁ in (V) } is set
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₁₁ is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
x is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
(r | L2) /. c₁₁ is Element of the carrier of V
(r | L2) /. x is Element of the carrier of V
r /. c₁₁ is Element of the carrier of V
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₂₁ is Relation-like Function-like set
dom c₂₁ is set
rng c₂₁ is set
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₁₁ is non empty Element of K32( the carrier of V)
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₂₁ is Element of the carrier of V
N . c₂₁ is V24() V25() ext-real Element of REAL
((L2 * L1) + ((1 - L2) * L2)) . c₂₁ is V24() V25() ext-real Element of REAL
(L2 * L1) . c₂₁ is V24() V25() ext-real Element of REAL
((1 - L2) * L2) . c₂₁ is V24() V25() ext-real Element of REAL
((L2 * L1) . c₂₁) + (((1 - L2) * L2) . c₂₁) is V24() V25() ext-real Element of REAL
L2 . c₂₁ is V24() V25() ext-real Element of REAL
(1 - L2) * (L2 . c₂₁) is V24() V25() ext-real Element of REAL
L1 . c₂₁ is V24() V25() ext-real Element of REAL
L2 * (L1 . c₂₁) is V24() V25() ext-real Element of REAL
L1 . c₂₁ is V24() V25() ext-real Element of REAL
L2 * (L1 . c₂₁) is V24() V25() ext-real Element of REAL
L2 . c₂₁ is V24() V25() ext-real Element of REAL
(1 / (1 - L2)) * (N . c₂₁) is V24() V25() ext-real Element of REAL
(1 - L2) * (L2 . c₂₁) is V24() V25() ext-real Element of REAL
(1 - L2) * (1 / (1 - L2)) is V24() V25() ext-real Element of REAL
((1 - L2) * (1 / (1 - L2))) * (N . c₂₁) is V24() V25() ext-real Element of REAL
(1 / ((1 - L2) / (1 - L2))) * (N . c₂₁) is V24() V25() ext-real Element of REAL
1 * (N . c₂₁) is V24() V25() ext-real Element of REAL
L1 . c₂₁ is V24() V25() ext-real Element of REAL
L2 * (L1 . c₂₁) is V24() V25() ext-real Element of REAL
L2 . c₂₁ is V24() V25() ext-real Element of REAL
(1 - L2) * (L2 . c₂₁) is V24() V25() ext-real Element of REAL
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₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M : b₁ in (V) } is set
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₁₁ is set
{c₁₁} is non empty V5() finite 1 -element set
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₁₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M
Lu * c₁₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
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₁₁) + ((1 - Lu) * x) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
Carrier c₁₁ is finite Element of K32( the carrier of V)
card (Carrier c₁₁) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
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₁₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M
Lu * c₁₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
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₁₁) + ((1 - Lu) * x) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
Carrier c₁₁ is finite Element of K32( the carrier of V)
card (Carrier c₁₁) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
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₁₁ is Element of the carrier of V
x1 is Element of the carrier of V
c₁₁ . x1 is V24() V25() ext-real Element of REAL
(c₁₁ . x1) * x1 is Element of the carrier of V
{x1} is non empty V5() finite 1 -element Element of K32( the carrier of V)
Sum (Lu * c₁₁) is Element of the carrier of V
Sum ((1 - Lu) * x) is Element of the carrier of V
(Sum (Lu * c₁₁)) + (Sum ((1 - Lu) * x)) is Element of the carrier of V
Lu * (Sum c₁₁) is Element of the carrier of V
(Lu * (Sum c₁₁)) + (Sum ((1 - Lu) * x)) is Element of the carrier of V
(1 - Lu) * (Sum x) is Element of the carrier of V
(Lu * (Sum c₁₁)) + ((1 - Lu) * (Sum x)) is Element of the carrier of V
c₁₁ 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
c₁₁ * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
1 - c₁₁ 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 - c₁₁) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
(c₁₁ * L2) + ((1 - c₁₁) * 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
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₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M : b₁ in (V) } is set
r is non empty Element of K32( the carrier of N)
(N) is set
{ (Sum b₁) where b₁ is Relation-like the carrier of N -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of r : b₁ in (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
(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₁) where b₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of M : b₁ in (V) } is set
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₁₁ is V24() V25() ext-real Element of REAL
c₁₁ * L2 is Element of the carrier of V
1 - c₁₁ is V24() V25() ext-real Element of REAL
(1 - c₁₁) * L2 is Element of the carrier of V
(c₁₁ * L2) + ((1 - c₁₁) * L2) is Element of 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 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₁₁ * Lu is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
(1 - c₁₁) * x is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
(c₁₁ * Lu) + ((1 - c₁₁) * x) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of V
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₁₁ * Lu) is Element of the carrier of V
Sum ((1 - c₁₁) * x) is Element of the carrier of V
(Sum (c₁₁ * Lu)) + (Sum ((1 - c₁₁) * x)) is Element of the carrier of V
c₁₁ * (Sum Lu) is Element of the carrier of V
(c₁₁ * (Sum Lu)) + (Sum ((1 - c₁₁) * x)) is Element of the carrier of V
(1 - c₁₁) * (Sum x) is Element of the carrier of V
(c₁₁ * (Sum Lu)) + ((1 - c₁₁) * (Sum x)) is Element of the carrier of V
L2 is set
L2 is Element of the carrier of V
c₁₁ is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() convex Linear_Combination of V
Sum c₁₁ is Element of 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 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₁₁ is Element of the carrier of V
N . c₁₁ 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
L2 is finite Element of K32( the carrier of V)
c₁₁ is Element of the carrier of V
L2 . c₁₁ is set
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₁₁ is Element of the carrier of V
L2 . c₁₁ 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
Carrier L2 is finite Element of K32( the carrier of V)
c₁₁ is set
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₁₁ is Element of the carrier of V
N . c₁₁ is V24() V25() ext-real Element of REAL
(u + L2) . c₁₁ is V24() V25() ext-real Element of REAL
u . c₁₁ is V24() V25() ext-real Element of REAL
L2 . c₁₁ is V24() V25() ext-real Element of REAL
(u . c₁₁) + (L2 . c₁₁) is V24() V25() ext-real Element of REAL
(N . c₁₁) + 0 is V24() V25() ext-real Element of REAL
u . c₁₁ is V24() V25() ext-real Element of REAL
L2 . c₁₁ is V24() V25() ext-real Element of REAL
(u . c₁₁) + (L2 . c₁₁) is V24() V25() ext-real Element of REAL
0 + (N . c₁₁) is V24() V25() ext-real Element of REAL
L2 . c₁₁ is V24() V25() ext-real Element of REAL
u . c₁₁ is V24() V25() ext-real Element of REAL
(u . c₁₁) + (L2 . c₁₁) is V24() V25() ext-real Element of REAL
c₁₁ is set
x is Element of the carrier of V
N . x is V24() V25() ext-real Element of REAL
L2 . x is V24() V25() ext-real Element of REAL
Sum u is Element of the carrier of V
card (Carrier u) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
Sum L2 is Element of the carrier of V
(Sum u) + (Sum L2) is Element of 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 N)) - (card (Carrier u)) is V24() V25() ext-real set
c₁₁ is Element of the carrier of V
u . c₁₁ is V24() V25() ext-real Element of REAL
N . c₁₁ is V24() V25() ext-real Element of REAL
x is Element of the carrier of V
L2 . x is V24() V25() ext-real Element of REAL
N . x is V24() V25() 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
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
{r} is non empty V5() finite 1 -element Element of K32( the carrier of V)
v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {r}
v . r is V24() V25() ext-real Element of REAL
Carrier v is finite 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
L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M
Sum L2 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,r} is non empty finite Element of K32( the carrier of V)
v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of {N,r}
v . N is V24() V25() ext-real Element of REAL
v . r is V24() V25() ext-real Element of REAL
Sum v is Element of the carrier of V
1 * N is Element of the carrier of V
1 * r is Element of the carrier of V
(1 * N) + (1 * r) is Element of the carrier of V
N + (1 * r) is Element of the carrier of V
Carrier v is finite 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
L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M
Sum L2 is Element of the carrier of V
1 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL
(1 + 1) * N is Element of the carrier of V
1 * N is Element of the carrier of V
(1 * N) + (1 * N) is Element of the carrier of V
N + (1 * N) is Element of 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
{r} is non empty V5() finite 1 -element set
v is Element of the carrier of V
N . v is V24() V25() ext-real Element of REAL
(N . v) * v is Element of the carrier of V
N is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative set
N + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive 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
Carrier r is finite Element of K32( the carrier of V)
card (Carrier r) is V17() V18() V19() V23() V24() V25() finite cardinal ext-real non negative Element of NAT
Sum r is Element of the carrier of V
(card (Carrier r)) - 1 is V24() V25() ext-real 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
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() Linear_Combination of M
Sum L2 is Element of the carrier of V
(Sum v) + (Sum 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
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
v is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M
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() Linear_Combination of M
Sum L2 is Element of the carrier of V
(Sum v) + (Sum 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
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
u is Element of the carrier of V
v . u is V24() V25() ext-real Element of REAL
r . u is V24() V25() ext-real Element of REAL
u is Element of the carrier of V
L2 . u is V24() V25() ext-real Element of REAL
r . u is V24() V25() ext-real Element of REAL
(card (Carrier v)) - 1 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() Linear_Combination of M
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() Linear_Combination of M
Sum L2 is Element of the carrier of V
(Sum u) + (Sum L2) is Element of the carrier of V
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
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
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL
(card (Carrier L2)) - 1 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() Linear_Combination of M
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() Linear_Combination of M
Sum L2 is Element of the carrier of V
(Sum u) + (Sum L2) is Element of the carrier of V
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
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
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)
Sum N is Element of the carrier of V
0 + 1 is non empty V17() V18() V19() V23() V24() V25() finite cardinal ext-real positive non negative Element of REAL
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 the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M
Sum 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() Linear_Combination of M
Sum v is Element of the carrier of V
(Sum r) + (Sum v) is Element of the carrier of V
Carrier r is finite Element of K32( the carrier of V)
card (Carrier r) 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
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)
Sum N is Element of the carrier of V
r is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V50() V51() V52() Linear_Combination of M
Carrier r is finite Element of K32( the carrier of V)
Sum 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
M is Element of K32( the carrier of V)
N is Element of K32( the carrier of V)
M /\ 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