:: CONVEX2 semantic presentation

REAL is non empty non finite V133() V134() V135() V139() set

NAT is V133() V134() V135() V136() V137() V138() V139() Element of K48(REAL)

K48(REAL) is set

COMPLEX is non empty non finite V133() V139() set

RAT is non empty non finite V133() V134() V135() V136() V139() set

INT is non empty non finite V133() V134() V135() V136() V137() V139() set

K49(COMPLEX,COMPLEX) is Relation-like V123() set

K48(K49(COMPLEX,COMPLEX)) is set

K49(K49(COMPLEX,COMPLEX),COMPLEX) is Relation-like V123() set

K48(K49(K49(COMPLEX,COMPLEX),COMPLEX)) is set

K49(REAL,REAL) is Relation-like V123() V124() V125() set

K48(K49(REAL,REAL)) is set

K49(K49(REAL,REAL),REAL) is Relation-like V123() V124() V125() set

K48(K49(K49(REAL,REAL),REAL)) is set

K49(RAT,RAT) is Relation-like RAT -valued V123() V124() V125() set

K48(K49(RAT,RAT)) is set

K49(K49(RAT,RAT),RAT) is Relation-like RAT -valued V123() V124() V125() set

K48(K49(K49(RAT,RAT),RAT)) is set

K49(INT,INT) is Relation-like RAT -valued INT -valued V123() V124() V125() set

K48(K49(INT,INT)) is set

K49(K49(INT,INT),INT) is Relation-like RAT -valued INT -valued V123() V124() V125() set

K48(K49(K49(INT,INT),INT)) is set

K49(NAT,NAT) is Relation-like RAT -valued INT -valued V123() V124() V125() V126() set

K49(K49(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V123() V124() V125() V126() set

K48(K49(K49(NAT,NAT),NAT)) is set

NAT is V133() V134() V135() V136() V137() V138() V139() set

K48(NAT) is set

K48(NAT) is set

K242(NAT) is V46() set

K49(NAT,REAL) is Relation-like V123() V124() V125() set

K48(K49(NAT,REAL)) is set

2 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

1 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

{} is Relation-like non-empty empty-yielding NAT -defined RAT -valued empty Function-like one-to-one constant functional finite FinSequence-like FinSubsequence-like FinSequence-membered V123() V124() V125() V126() V133() V134() V135() V136() V137() V138() V139() set

3 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

0 is Relation-like non-empty empty-yielding NAT -defined RAT -valued V8() V12() empty Function-like one-to-one constant functional V24() V25() V30() V31() finite FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative V123() V124() V125() V126() V133() V134() V135() V136() V137() V138() V139() Element of NAT

Seg 1 is non empty finite 1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

{1} is non empty V133() V134() V135() V136() V137() V138() set

Seg 2 is non empty finite 2 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

{1,2} is non empty V133() V134() V135() V136() V137() V138() set

card {} is cardinal set

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

<*rr*> is Relation-like NAT -defined REAL -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

[1,rr] is set

{1,rr} is non empty V133() V134() V135() set

{{1,rr},{1}} is non empty set

{[1,rr]} is Relation-like non empty Function-like set

V is non empty RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

M is convex Element of K48( the carrier of V)

L1 is convex Element of K48( the carrier of V)

M /\ L1 is convex Element of K48( the carrier of V)

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

dom L1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

dom L2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(dom L1) /\ (dom L2) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

( not b

( b

r is Element of the carrier of V

L is Element of the carrier of V

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

F2 * r is Element of the carrier of V

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

(1 - F2) * L is Element of the carrier of V

(F2 * r) + ((1 - F2) * L) is Element of the carrier of V

Btm is Element of the carrier of V

Top is Element of the carrier of V

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

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L1 . F1 is set

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

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

Lm is Element of the carrier of V

Top .|. Lm is V24() V25() ext-real Element of REAL

Lb is Element of the carrier of V

((F2 * r) + ((1 - F2) * L)) .|. Lb is V24() V25() ext-real Element of REAL

(F2 * r) .|. Lb is V24() V25() ext-real Element of REAL

((1 - F2) * L) .|. Lb is V24() V25() ext-real Element of REAL

((F2 * r) .|. Lb) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

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

F2 * (r .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

L .|. Lb is V24() V25() ext-real Element of REAL

(1 - F2) * (L .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

F2 * Lt is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

(((F2 * r) + ((1 - F2) * L)) .|. Lb) - (F2 * Lt) is V24() V25() ext-real Element of REAL

(1 - F2) * Lt is V24() V25() ext-real Element of REAL

Ft is Element of the carrier of V

Btm .|. Ft is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * Lt) is V24() V25() ext-real Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

dom L1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

dom L2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(dom L1) /\ (dom L2) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

( not b

( b

r is Element of the carrier of V

L is Element of the carrier of V

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

F2 * r is Element of the carrier of V

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

(1 - F2) * L is Element of the carrier of V

(F2 * r) + ((1 - F2) * L) is Element of the carrier of V

Btm is Element of the carrier of V

Top is Element of the carrier of V

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

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L1 . F1 is set

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

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

Lm is Element of the carrier of V

Top .|. Lm is V24() V25() ext-real Element of REAL

Lb is Element of the carrier of V

((F2 * r) + ((1 - F2) * L)) .|. Lb is V24() V25() ext-real Element of REAL

(F2 * r) .|. Lb is V24() V25() ext-real Element of REAL

((1 - F2) * L) .|. Lb is V24() V25() ext-real Element of REAL

((F2 * r) .|. Lb) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

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

F2 * (r .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

L .|. Lb is V24() V25() ext-real Element of REAL

(1 - F2) * (L .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

F2 * Lt is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

(((F2 * r) + ((1 - F2) * L)) .|. Lb) - (F2 * Lt) is V24() V25() ext-real Element of REAL

(1 - F2) * Lt is V24() V25() ext-real Element of REAL

Ft is Element of the carrier of V

Btm .|. Ft is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * Lt) is V24() V25() ext-real Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

dom L1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

dom L2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(dom L1) /\ (dom L2) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

( not b

( b

r is Element of the carrier of V

L is Element of the carrier of V

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

F2 * r is Element of the carrier of V

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

(1 - F2) * L is Element of the carrier of V

(F2 * r) + ((1 - F2) * L) is Element of the carrier of V

Btm is Element of the carrier of V

Top is Element of the carrier of V

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

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L1 . F1 is set

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

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

Lm is Element of the carrier of V

Top .|. Lm is V24() V25() ext-real Element of REAL

Lb is Element of the carrier of V

((F2 * r) + ((1 - F2) * L)) .|. Lb is V24() V25() ext-real Element of REAL

(F2 * r) .|. Lb is V24() V25() ext-real Element of REAL

((1 - F2) * L) .|. Lb is V24() V25() ext-real Element of REAL

((F2 * r) .|. Lb) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

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

F2 * (r .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

L .|. Lb is V24() V25() ext-real Element of REAL

(1 - F2) * (L .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

F2 * Lt is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

(((F2 * r) + ((1 - F2) * L)) .|. Lb) - (F2 * Lt) is V24() V25() ext-real Element of REAL

(1 - F2) * Lt is V24() V25() ext-real Element of REAL

Ft is Element of the carrier of V

Btm .|. Ft is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * Lt) is V24() V25() ext-real Element of REAL

V is non empty RealUnitarySpace-like UNITSTR

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

L1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

dom L1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

dom L2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(dom L1) /\ (dom L2) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

( not b

( b

r is Element of the carrier of V

L is Element of the carrier of V

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

F2 * r is Element of the carrier of V

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

(1 - F2) * L is Element of the carrier of V

(F2 * r) + ((1 - F2) * L) is Element of the carrier of V

Btm is Element of the carrier of V

Top is Element of the carrier of V

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

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L1 . F1 is set

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

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

Lm is Element of the carrier of V

Top .|. Lm is V24() V25() ext-real Element of REAL

Lb is Element of the carrier of V

((F2 * r) + ((1 - F2) * L)) .|. Lb is V24() V25() ext-real Element of REAL

(F2 * r) .|. Lb is V24() V25() ext-real Element of REAL

((1 - F2) * L) .|. Lb is V24() V25() ext-real Element of REAL

((F2 * r) .|. Lb) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

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

F2 * (r .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + (((1 - F2) * L) .|. Lb) is V24() V25() ext-real Element of REAL

L .|. Lb is V24() V25() ext-real Element of REAL

(1 - F2) * (L .|. Lb) is V24() V25() ext-real Element of REAL

(F2 * (r .|. Lb)) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

F2 * Lt is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * (L .|. Lb)) is V24() V25() ext-real Element of REAL

(((F2 * r) + ((1 - F2) * L)) .|. Lb) - (F2 * Lt) is V24() V25() ext-real Element of REAL

(1 - F2) * Lt is V24() V25() ext-real Element of REAL

Ft is Element of the carrier of V

Btm .|. Ft is V24() V25() ext-real Element of REAL

(F2 * Lt) + ((1 - F2) * Lt) is V24() V25() ext-real Element of REAL

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

M is convex Element of K48( the carrier of V)

L1 is Element of K48( the carrier of V)

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of L1

Sum L2 is Element of the carrier of V

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

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

rng r is set

len r is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len L is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,L,K180()) is V24() V25() ext-real Element of REAL

dom L is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len L is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,L,K180()) is V24() V25() ext-real Element of REAL

dom L is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

card (Carrier L2) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

card {} is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

len (L2 (#) r) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Btm is V8() V12() non empty ext-real positive non negative set

mid ((L2 (#) r),1,Btm) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (mid ((L2 (#) r),1,Btm)) is Element of the carrier of V

mid (L,1,Btm) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Sum (mid (L,1,Btm)) is V24() V25() ext-real Element of REAL

K243(REAL,(mid (L,1,Btm)),K180()) is V24() V25() ext-real Element of REAL

1 / (Sum (mid (L,1,Btm))) is V24() V25() ext-real Element of REAL

(1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))) is Element of the carrier of V

Btm + 1 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

mid ((L2 (#) r),1,(Btm + 1)) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (mid ((L2 (#) r),1,(Btm + 1))) is Element of the carrier of V

mid (L,1,(Btm + 1)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Sum (mid (L,1,(Btm + 1))) is V24() V25() ext-real Element of REAL

K243(REAL,(mid (L,1,(Btm + 1))),K180()) is V24() V25() ext-real Element of REAL

1 / (Sum (mid (L,1,(Btm + 1)))) is V24() V25() ext-real Element of REAL

(1 / (Sum (mid (L,1,(Btm + 1))))) * (Sum (mid ((L2 (#) r),1,(Btm + 1)))) is Element of the carrier of V

(L2 (#) r) | (Btm + 1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Seg (Btm + 1) is non empty finite Btm + 1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

(L2 (#) r) | (Seg (Btm + 1)) is Relation-like NAT -defined Seg (Btm + 1) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

L | Btm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Seg Btm is non empty finite Btm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

L | (Seg Btm) is Relation-like NAT -defined Seg Btm -defined NAT -defined REAL -valued Function-like FinSubsequence-like V123() V124() V125() set

L | (Btm + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

L | (Seg (Btm + 1)) is Relation-like NAT -defined Seg (Btm + 1) -defined NAT -defined REAL -valued Function-like FinSubsequence-like V123() V124() V125() set

(L2 (#) r) | Btm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(L2 (#) r) | (Seg Btm) is Relation-like NAT -defined Seg Btm -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

L | Btm is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Seg Btm is non empty finite Btm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

L | (Seg Btm) is Relation-like NAT -defined Seg Btm -defined NAT -defined REAL -valued Function-like FinSubsequence-like V123() V124() V125() set

len (mid (L,1,Btm)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (mid (L,1,Btm)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(mid (L,1,Btm)) . 1 is V24() V25() ext-real set

Seg (len L) is finite len L -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

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

r . 1 is set

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

dom r is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

Seg (len (mid (L,1,Btm))) is finite len (mid (L,1,Btm)) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

Top is Element of the carrier of V

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

(mid (L,1,(Btm + 1))) . (Btm + 1) is V24() V25() ext-real set

<*((mid (L,1,(Btm + 1))) . (Btm + 1))*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,((mid (L,1,(Btm + 1))) . (Btm + 1))] is set

{1,((mid (L,1,(Btm + 1))) . (Btm + 1))} is non empty V133() V134() V135() set

{{1,((mid (L,1,(Btm + 1))) . (Btm + 1))},{1}} is non empty set

{[1,((mid (L,1,(Btm + 1))) . (Btm + 1))]} is Relation-like non empty Function-like set

dom <*((mid (L,1,(Btm + 1))) . (Btm + 1))*> is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

Top is V8() V12() ext-real non negative set

(len (mid (L,1,Btm))) + Top is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

(mid (L,1,(Btm + 1))) . ((len (mid (L,1,Btm))) + Top) is V24() V25() ext-real set

<*((mid (L,1,(Btm + 1))) . (Btm + 1))*> . Top is set

L | (Btm + 1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Seg (Btm + 1) is non empty finite Btm + 1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

L | (Seg (Btm + 1)) is Relation-like NAT -defined Seg (Btm + 1) -defined NAT -defined REAL -valued Function-like FinSubsequence-like V123() V124() V125() set

F1 is V8() V12() ext-real non negative set

(mid (L,1,Btm)) . F1 is V24() V25() ext-real set

L . F1 is V24() V25() ext-real set

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

(mid (L,1,Btm)) . F1 is V24() V25() ext-real set

len (L | (Btm + 1)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

F1 is V8() V12() ext-real non negative set

(mid (L,1,(Btm + 1))) . F1 is V24() V25() ext-real set

(mid (L,1,Btm)) . F1 is V24() V25() ext-real set

len (L | Btm) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Seg (len (L | Btm)) is finite len (L | Btm) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

(L | Btm) . F1 is V24() V25() ext-real set

(L | Btm) /. F1 is V24() V25() ext-real Element of REAL

L /. F1 is V24() V25() ext-real Element of REAL

dom (L | (Btm + 1)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(L | (Btm + 1)) . F1 is V24() V25() ext-real set

(L | (Btm + 1)) /. F1 is V24() V25() ext-real Element of REAL

Seg (len L) is finite len L -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

dom r is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

dom (L | (Btm + 1)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(L | (Btm + 1)) /. (Btm + 1) is V24() V25() ext-real Element of REAL

L /. (Btm + 1) is V24() V25() ext-real Element of REAL

L . (Btm + 1) is V24() V25() ext-real set

r . (Btm + 1) is set

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

r /. (Btm + 1) is Element of the carrier of V

L2 . (r /. (Btm + 1)) is V24() V25() ext-real Element of REAL

len <*((mid (L,1,(Btm + 1))) . (Btm + 1))*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

len (mid (L,1,(Btm + 1))) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (mid (L,1,(Btm + 1))) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(len (mid (L,1,Btm))) + (len <*((mid (L,1,(Btm + 1))) . (Btm + 1))*>) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Seg ((len (mid (L,1,Btm))) + (len <*((mid (L,1,(Btm + 1))) . (Btm + 1))*>)) is finite (len (mid (L,1,Btm))) + (len <*((mid (L,1,(Btm + 1))) . (Btm + 1))*>) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

(mid (L,1,Btm)) ^ <*((mid (L,1,(Btm + 1))) . (Btm + 1))*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

(Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))) is V24() V25() ext-real Element of REAL

(L2 (#) r) | (Btm + 1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(L2 (#) r) | (Seg (Btm + 1)) is Relation-like NAT -defined Seg (Btm + 1) -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) is V24() V25() ext-real Element of REAL

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm))) is V24() V25() ext-real Element of REAL

(Sum (mid (L,1,Btm))) / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) is V24() V25() ext-real Element of REAL

Seg (len r) is finite len r -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

{ b

Lb is Element of the carrier of V

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

0 + 0 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (L2 (#) r) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

len ((L2 (#) r) | (Btm + 1)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (mid ((L2 (#) r),1,Btm)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

Lb is V8() V12() ext-real non negative set

(mid ((L2 (#) r),1,(Btm + 1))) . Lb is set

(mid ((L2 (#) r),1,Btm)) . Lb is set

(L2 (#) r) | Btm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(L2 (#) r) | (Seg Btm) is Relation-like NAT -defined Seg Btm -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

len ((L2 (#) r) | Btm) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Seg (len ((L2 (#) r) | Btm)) is finite len ((L2 (#) r) | Btm) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

((L2 (#) r) | Btm) . Lb is set

((L2 (#) r) | Btm) /. Lb is Element of the carrier of V

(L2 (#) r) /. Lb is Element of the carrier of V

dom ((L2 (#) r) | (Btm + 1)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

((L2 (#) r) | (Btm + 1)) . Lb is set

((L2 (#) r) | (Btm + 1)) /. Lb is Element of the carrier of V

dom ((L2 (#) r) | (Btm + 1)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

((L2 (#) r) | (Btm + 1)) /. (Btm + 1) is Element of the carrier of V

(L2 (#) r) /. (Btm + 1) is Element of the carrier of V

(mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1) is set

(L2 (#) r) . (Btm + 1) is set

(L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)) is Element of the carrier of V

(L2 (#) r) | Btm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(L2 (#) r) | (Seg Btm) is Relation-like NAT -defined Seg Btm -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

len (mid ((L2 (#) r),1,Btm)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

<*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))] is set

{1,((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))} is non empty set

{{1,((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))},{1}} is non empty set

{[1,((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))]} is Relation-like non empty Function-like set

dom <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*> is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

Lb is V8() V12() ext-real non negative set

(len (mid ((L2 (#) r),1,Btm))) + Lb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

(mid ((L2 (#) r),1,(Btm + 1))) . ((len (mid ((L2 (#) r),1,Btm))) + Lb) is set

<*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*> . Lb is set

len <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

len (mid ((L2 (#) r),1,(Btm + 1))) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (mid ((L2 (#) r),1,(Btm + 1))) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(len (mid ((L2 (#) r),1,Btm))) + (len <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*>) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Seg ((len (mid ((L2 (#) r),1,Btm))) + (len <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*>)) is finite (len (mid ((L2 (#) r),1,Btm))) + (len <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*>) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

(mid ((L2 (#) r),1,Btm)) ^ <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*> is Relation-like NAT -defined non empty Function-like finite FinSequence-like FinSubsequence-like set

(Sum (mid ((L2 (#) r),1,Btm))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((Sum (mid ((L2 (#) r),1,Btm))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

1 * (Sum (mid ((L2 (#) r),1,Btm))) is Element of the carrier of V

(1 * (Sum (mid ((L2 (#) r),1,Btm)))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((1 * (Sum (mid ((L2 (#) r),1,Btm)))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

(Sum (mid (L,1,Btm))) * (1 / (Sum (mid (L,1,Btm)))) is V24() V25() ext-real Element of REAL

((Sum (mid (L,1,Btm))) * (1 / (Sum (mid (L,1,Btm))))) * (Sum (mid ((L2 (#) r),1,Btm))) is Element of the carrier of V

(((Sum (mid (L,1,Btm))) * (1 / (Sum (mid (L,1,Btm))))) * (Sum (mid ((L2 (#) r),1,Btm)))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((((Sum (mid (L,1,Btm))) * (1 / (Sum (mid (L,1,Btm))))) * (Sum (mid ((L2 (#) r),1,Btm)))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

(Sum (mid (L,1,Btm))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm)))) is Element of the carrier of V

((Sum (mid (L,1,Btm))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (((Sum (mid (L,1,Btm))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))))) + ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((Sum (mid (L,1,Btm))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1))) is Element of the carrier of V

((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((Sum (mid (L,1,Btm))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm)))))) + ((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm)))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm)))) is Element of the carrier of V

(((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm)))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))))) + ((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * ((L2 . (r /. (Btm + 1))) * (r /. (Btm + 1)))) is Element of the carrier of V

(1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (L2 . (r /. (Btm + 1))) is V24() V25() ext-real Element of REAL

((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (L2 . (r /. (Btm + 1)))) * (r /. (Btm + 1)) is Element of the carrier of V

(((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm)))) * ((1 / (Sum (mid (L,1,Btm)))) * (Sum (mid ((L2 (#) r),1,Btm))))) + (((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (L2 . (r /. (Btm + 1)))) * (r /. (Btm + 1))) is Element of the carrier of V

1 - ((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm)))) is V24() V25() ext-real Element of REAL

((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) * (1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) is V24() V25() ext-real Element of REAL

(((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) * (1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))))) - ((1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) * (Sum (mid (L,1,Btm)))) is V24() V25() ext-real Element of REAL

((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) - (Sum (mid (L,1,Btm))) is V24() V25() ext-real Element of REAL

(((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1)))) - (Sum (mid (L,1,Btm)))) * (1 / ((Sum (mid (L,1,Btm))) + (L2 . (r /. (Btm + 1))))) is V24() V25() ext-real Element of REAL

0 + 1 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

mid ((L2 (#) r),1,1) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (mid ((L2 (#) r),1,1)) is Element of the carrier of V

mid (L,1,1) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Sum (mid (L,1,1)) is V24() V25() ext-real Element of REAL

K243(REAL,(mid (L,1,1)),K180()) is V24() V25() ext-real Element of REAL

1 / (Sum (mid (L,1,1))) is V24() V25() ext-real Element of REAL

(1 / (Sum (mid (L,1,1)))) * (Sum (mid ((L2 (#) r),1,1))) is Element of the carrier of V

L | 1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

L | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined REAL -valued Function-like FinSubsequence-like V123() V124() V125() set

len (mid (L,1,1)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom (mid (L,1,1)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

(mid (L,1,1)) . 1 is V24() V25() ext-real set

<*((mid (L,1,1)) . 1)*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,((mid (L,1,1)) . 1)] is set

{1,((mid (L,1,1)) . 1)} is non empty V133() V134() V135() set

{{1,((mid (L,1,1)) . 1)},{1}} is non empty set

{[1,((mid (L,1,1)) . 1)]} is Relation-like non empty Function-like set

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

(L2 (#) r) | 1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

(L2 (#) r) | (Seg 1) is Relation-like NAT -defined Seg 1 -defined NAT -defined the carrier of V -valued Function-like FinSubsequence-like set

len (mid ((L2 (#) r),1,1)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

(mid ((L2 (#) r),1,1)) . 1 is set

<*((mid ((L2 (#) r),1,1)) . 1)*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,((mid ((L2 (#) r),1,1)) . 1)] is set

{1,((mid ((L2 (#) r),1,1)) . 1)} is non empty set

{{1,((mid ((L2 (#) r),1,1)) . 1)},{1}} is non empty set

{[1,((mid ((L2 (#) r),1,1)) . 1)]} is Relation-like non empty Function-like set

Seg (len (L2 (#) r)) is finite len (L2 (#) r) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

dom r is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

r /. 1 is Element of the carrier of V

r . 1 is set

dom (L2 (#) r) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

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

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

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

(L2 (#) r) . 1 is set

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

(1 / (Sum (mid (L,1,1)))) * ((L2 . (r /. 1)) * (r /. 1)) is Element of the carrier of V

(1 / (Sum (mid (L,1,1)))) * (L2 . (r /. 1)) is V24() V25() ext-real Element of REAL

((1 / (Sum (mid (L,1,1)))) * (L2 . (r /. 1))) * (r /. 1) is Element of the carrier of V

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

Top is Element of the carrier of V

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

F2 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

mid ((L2 (#) r),1,F2) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (mid ((L2 (#) r),1,F2)) is Element of the carrier of V

mid (L,1,F2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Sum (mid (L,1,F2)) is V24() V25() ext-real Element of REAL

K243(REAL,(mid (L,1,F2)),K180()) is V24() V25() ext-real Element of REAL

1 / (Sum (mid (L,1,F2))) is V24() V25() ext-real Element of REAL

(1 / (Sum (mid (L,1,F2)))) * (Sum (mid ((L2 (#) r),1,F2))) is Element of the carrier of V

mid (L,1,(len L)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

Sum (mid (L,1,(len L))) is V24() V25() ext-real Element of REAL

K243(REAL,(mid (L,1,(len L))),K180()) is V24() V25() ext-real Element of REAL

mid ((L2 (#) r),1,(len (L2 (#) r))) is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

Sum (mid ((L2 (#) r),1,(len (L2 (#) r)))) is Element of the carrier of V

1 / (Sum (mid (L,1,(len L)))) is V24() V25() ext-real Element of REAL

(1 / (Sum (mid (L,1,(len L))))) * (Sum (mid ((L2 (#) r),1,(len (L2 (#) r))))) is Element of the carrier of V

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

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

L1 is Element of the carrier of V

L2 is Element of the carrier of V

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

r * L1 is Element of the carrier of V

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

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

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

{L1,L2} is non empty Element of K48( the carrier of V)

Btm is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of {L1,L2}

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

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

F2 is Element of K48( the carrier of V)

Top is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of F2

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

{ b

Carrier Top is finite Element of K48( the carrier of V)

<*r,(1 - r)*> is Relation-like NAT -defined REAL -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

<*r*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,r] is set

{1,r} is non empty V133() V134() V135() set

{{1,r},{1}} is non empty set

{[1,r]} is Relation-like non empty Function-like set

<*(1 - r)*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,(1 - r)] is set

{1,(1 - r)} is non empty V133() V134() V135() set

{{1,(1 - r)},{1}} is non empty set

{[1,(1 - r)]} is Relation-like non empty Function-like set

<*r*> ^ <*(1 - r)*> is Relation-like NAT -defined non empty Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set

1 + 1 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

dom <*r,(1 - r)*> is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

<*L1,L2*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

<*L1*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,L1] is set

{1,L1} is non empty set

{{1,L1},{1}} is non empty set

{[1,L1]} is Relation-like non empty Function-like set

<*L2*> is Relation-like NAT -defined non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like set

[1,L2] is set

{1,L2} is non empty set

{{1,L2},{1}} is non empty set

{[1,L2]} is Relation-like non empty Function-like set

<*L1*> ^ <*L2*> is Relation-like NAT -defined non empty Function-like finite 1 + 1 -element FinSequence-like FinSubsequence-like set

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

<*r,(1 - r)*> . F1 is V24() V25() ext-real set

<*L1,L2*> . F1 is set

Top . (<*L1,L2*> . F1) is V24() V25() ext-real set

len <*r,(1 - r)*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Seg (len <*r,(1 - r)*>) is finite len <*r,(1 - r)*> -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)

{ b

{1,2} is non empty V133() V134() V135() V136() V137() V138() Element of K48(REAL)

F1 is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F1 is non empty set

len F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Sum <*r,(1 - r)*> is V24() V25() ext-real Element of REAL

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,<*r,(1 - r)*>,K180()) is V24() V25() ext-real Element of REAL

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

<*L1*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng <*L1*> is non empty set

<*L2*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng <*L2*> is non empty set

(rng <*L1*>) \/ (rng <*L2*>) is non empty set

{L1} is non empty Element of K48( the carrier of V)

{L1} \/ (rng <*L2*>) is non empty set

{L2} is non empty Element of K48( the carrier of V)

{L1} \/ {L2} is non empty Element of K48( the carrier of V)

Lt is Relation-like NAT -defined REAL -valued non empty Function-like finite 2 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len Lt is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K243(REAL,Lt,K180()) is V24() V25() ext-real Element of REAL

dom Lt is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

len <*r,(1 - r)*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

len <*L1,L2*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Lm is V8() V12() ext-real non negative set

Lt . Lm is V24() V25() ext-real set

F1 . Lm is set

Top . (F1 . Lm) is V24() V25() ext-real set

Sum Top is Element of the carrier of V

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

{L1} is non empty Element of K48( the carrier of V)

Btm is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of {L1}

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

F2 is Element of K48( the carrier of V)

Top is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of F2

Carrier Top is finite Element of K48( the carrier of V)

<*L1*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

[1,L1] is set

{1,L1} is non empty set

{{1,L1},{1}} is non empty set

{[1,L1]} is Relation-like non empty Function-like set

rng <*L1*> is non empty set

len <*L1*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

len <*rr*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

Sum <*rr*> is V24() V25() ext-real Element of REAL

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,<*rr*>,K180()) is V24() V25() ext-real Element of REAL

dom <*rr*> is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

<*rr*> . F1 is V24() V25() ext-real set

<*L1*> . F1 is set

Top . (<*L1*> . F1) is V24() V25() ext-real set

{1} is non empty V133() V134() V135() V136() V137() V138() Element of K48(REAL)

<*1*> is Relation-like NAT -defined REAL -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

[1,1] is set

{1,1} is non empty V133() V134() V135() V136() V137() V138() set

{{1,1},{1}} is non empty set

{[1,1]} is Relation-like non empty Function-like set

len <*1*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

F1 is V8() V12() ext-real non negative set

<*rr*> . F1 is V24() V25() ext-real set

<*L1*> . F1 is set

Top . (<*L1*> . F1) is V24() V25() ext-real set

{ b

F1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,F1,K180()) is V24() V25() ext-real Element of REAL

dom F1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

F1 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V

rng F1 is set

Lt is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len Lt is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

len F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,Lt,K180()) is V24() V25() ext-real Element of REAL

dom Lt is V133() V134() V135() V136() V137() V138() Element of K48(NAT)

Sum Top is Element of the carrier of V

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

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

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

0 + 1 is V8() V12() non empty V24() V25() V30() V31() ext-real positive non negative V133() V134() V135() V136() V137() V138() Element of NAT

(0 + 1) * L1 is Element of the carrier of V

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

L1 is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of L1 is non empty set

K48( the carrier of L1) is set

r is Element of K48( the carrier of L1)

M is Element of K48( the carrier of V)

L2 is Element of K48( the carrier of L1)

L is Relation-like the carrier of L1 -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of r

Sum L is Element of the carrier of L1

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

M is Element of K48( the carrier of V)

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

L1 is set

L2 is set

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

the Element of the carrier of V is Element of the carrier of V

{ the Element of the carrier of V} is non empty Element of K48( the carrier of V)

K48( the carrier of V) is set

L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of { the Element of the carrier of V}

L1 . the Element of the carrier of V is V24() V25() ext-real Element of REAL

L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V

<* the Element of the carrier of V*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

[1, the Element of the carrier of V] is set

{1, the Element of the carrier of V} is non empty set

{{1, the Element of the carrier of V},{1}} is non empty set

{[1, the Element of the carrier of V]} is Relation-like non empty Function-like set

rng <* the Element of the carrier of V*> is non empty set

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

len <* the Element of the carrier of V*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

{ b

r is Relation-like NAT -defined REAL -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len r is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

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

dom r is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

L is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

r . L is V24() V25() ext-real set

<* the Element of the carrier of V*> . L is set

L2 . (<* the Element of the carrier of V*> . L) is V24() V25() ext-real set

{1} is non empty V133() V134() V135() V136() V137() V138() Element of K48(REAL)

L2 . the Element of the carrier of V is V24() V25() ext-real Element of REAL

<*1*> is Relation-like NAT -defined REAL -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

[1,1] is set

{1,1} is non empty V133() V134() V135() V136() V137() V138() set

{{1,1},{1}} is non empty set

{[1,1]} is Relation-like non empty Function-like set

len <*1*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

L is V8() V12() ext-real non negative set

r . L is V24() V25() ext-real set

<* the Element of the carrier of V*> . L is set

L2 . (<* the Element of the carrier of V*> . L) is V24() V25() ext-real set

V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct

the carrier of V is non empty set

K48( the carrier of V) is set

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

L1 is set

L2 is Element of the carrier of V

{L2} is non empty Element of K48( the carrier of V)

r is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of {L2}

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

L is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of M

<*L2*> is Relation-like NAT -defined the carrier of V -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like FinSequence of the carrier of V

[1,L2] is set

{1,L2} is non empty set

{{1,L2},{1}} is non empty set

{[1,L2]} is Relation-like non empty Function-like set

rng <*L2*> is non empty set

Carrier L is finite Element of K48( the carrier of V)

len <*L2*> is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

{ b

F2 is Relation-like NAT -defined REAL -valued non empty Function-like finite 1 -element FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL

len F2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

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

K180() is Relation-like K49(REAL,REAL) -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(K49(REAL,REAL),REAL))

K243(REAL,F2,K180()) is V24() V25() ext-real Element of REAL

dom F2 is non empty V133() V134() V135() V136() V137() V138() Element of K48(NAT)

Btm is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT

F2 . Btm is V24() V25() ext-real set

<*L2*> . Btm is set

L