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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{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)
{ b1 where b1 is Element of the carrier of V : for b2 being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b2 in (dom L1) /\ (dom L2) or ex b3 being Element of the carrier of V st
( b3 = L1 . b2 & b1 .|. b3 <= L2 . b2 ) ) } is set
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)
{ b1 where b1 is Element of the carrier of V : for b2 being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b2 in (dom L1) /\ (dom L2) or ex b3 being Element of the carrier of V st
( b3 = L1 . b2 & not L2 . b2 <= b1 .|. b3 ) ) } is set
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)
{ b1 where b1 is Element of the carrier of V : for b2 being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b2 in (dom L1) /\ (dom L2) or ex b3 being Element of the carrier of V st
( b3 = L1 . b2 & L2 . b2 <= b1 .|. b3 ) ) } is set
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)
{ b1 where b1 is Element of the carrier of V : for b2 being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b2 in (dom L1) /\ (dom L2) or ex b3 being Element of the carrier of V st
( b3 = L1 . b2 & not b1 .|. b3 <= L2 . b2 ) ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= Btm + 1 ) } is set
(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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= Btm ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= Btm ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len L ) } is set
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)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0 } is set
Seg (len (mid (L,1,Btm))) is finite len (mid (L,1,Btm)) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len (mid (L,1,Btm)) ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= Btm + 1 ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len (L | Btm) ) } is set
(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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len L ) } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= (len (mid (L,1,Btm))) + (len <*((mid (L,1,(Btm + 1))) . (Btm + 1))*>) ) } is set
(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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len r ) } is set
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0 } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len ((L2 (#) r) | Btm) ) } is set
((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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= (len (mid ((L2 (#) r),1,Btm))) + (len <*((mid ((L2 (#) r),1,(Btm + 1))) . (Btm + 1))*>) ) } is set
(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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len (L2 (#) r) ) } is set
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)
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0 } is set
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
{ b1 where b1 is Element of the carrier of V : not Top . b1 = 0 } is set
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)
{ b1 where b1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b1 & b1 <= len <*r,(1 - r)*> ) } is set
{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
{ b1 where b1 is Element of the carrier of V : not Top . b1 = 0 } is set
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
{ b1 where b1 is Element of the carrier of V : not L2 . b1 = 0 } is set
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
{ b1 where b1 is Element of the carrier of V : not L . b1 = 0 } is set
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