:: 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₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is Element of the carrier of V : for b₂ being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b₂ in (dom L1) /\ (dom L2) or ex b₃ being Element of the carrier of V st
( b₃ = L1 . b₂ & b₁ .|. b₃ <= L2 . b₂ ) ) } 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)
{ b₁ where b₁ is Element of the carrier of V : for b₂ being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b₂ in (dom L1) /\ (dom L2) or ex b₃ being Element of the carrier of V st
( b₃ = L1 . b₂ & not L2 . b₂ <= b₁ .|. b₃ ) ) } 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)
{ b₁ where b₁ is Element of the carrier of V : for b₂ being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b₂ in (dom L1) /\ (dom L2) or ex b₃ being Element of the carrier of V st
( b₃ = L1 . b₂ & L2 . b₂ <= b₁ .|. b₃ ) ) } 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)
{ b₁ where b₁ is Element of the carrier of V : for b₂ being V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT holds
( not b₂ in (dom L1) /\ (dom L2) or ex b₃ being Element of the carrier of V st
( b₃ = L1 . b₂ & not b₁ .|. b₃ <= L2 . b₂ ) ) } 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is Element of the carrier of V : not L2 . b₁ = 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= (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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
{ b₁ where b₁ is Element of the carrier of V : not L2 . b₁ = 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= (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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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)
{ b₁ where b₁ is Element of the carrier of V : not L2 . b₁ = 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
{ b₁ where b₁ is Element of the carrier of V : not Top . b₁ = 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)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is Element of the carrier of V : not Top . b₁ = 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
{ b₁ where b₁ is Element of the carrier of V : not L2 . b₁ = 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
{ b₁ where b₁ is Element of the carrier of V : not L . b₁ = 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 . (<*L2*> . Btm) is V24() V25() ext-real set
{1} is non empty V133() V134() V135() V136() V137() V138() Element of K48(REAL)
L . L2 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
Btm is V8() V12() ext-real non negative set
F2 . Btm is V24() V25() ext-real set
<*L2*> . Btm is set
L . (<*L2*> . Btm) 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
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
M is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
L1 is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
M + L1 is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
Up (M + L1) is non empty Element of K48( the carrier of V)
the carrier of V is non empty set
K48( the carrier of V) is set
Up M is non empty Element of K48( the carrier of V)
Up L1 is non empty Element of K48( the carrier of V)
(Up M) + (Up L1) is Element of K48( the carrier of V)
the carrier of (M + L1) is non empty set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in M & b₂ in L1 ) } is set
L2 is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in Up M & b₂ in Up L1 ) } is set
r is Element of the carrier of V
L is Element of the carrier of V
r + L is Element of the carrier of V
the carrier of L1 is non empty set
the carrier of M is non empty set
L2 is set
r is Element of the carrier of V
L is Element of the carrier of V
r + L is Element of the carrier of V
the carrier of L1 is non empty set
the carrier of M is non empty set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of V : ( b₁ in Up M & b₂ in Up L1 ) } 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
M is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
L1 is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
M /\ L1 is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
Up (M /\ L1) is non empty Element of K48( the carrier of V)
K48( the carrier of V) is set
Up M is non empty Element of K48( the carrier of V)
Up L1 is non empty Element of K48( the carrier of V)
(Up M) /\ (Up L1) is Element of K48( the carrier of V)
the carrier of (M /\ L1) is non empty set
the carrier of M is non empty set
the carrier of L1 is non empty set
the carrier of M /\ the carrier of L1 is set
L2 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
K48( the carrier of V) is set
M is Element of K48( the carrier of V)
Convex-Family M is non empty Element of K48(K48( the carrier of V))
K48(K48( the carrier of V)) 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
M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
L2 is V24() V25() ext-real Element of REAL
r is V24() V25() ext-real Element of REAL
L2 * r is V24() V25() ext-real Element of REAL
L2 * M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
r * L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
(L2 * M) + (r * L1) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier ((L2 * M) + (r * L1)) is finite Element of K48( the carrier of V)
K48( the carrier of V) is set
Carrier (L2 * M) is finite Element of K48( the carrier of V)
Carrier (r * L1) is finite Element of K48( the carrier of V)
(Carrier (L2 * M)) \/ (Carrier (r * L1)) is Element of K48( the carrier of V)
Carrier L1 is finite Element of K48( the carrier of V)
Carrier M is finite Element of K48( the carrier of V)
L is set
{ b₁ where b₁ is Element of the carrier of V : not (L2 * M) . b₁ = 0 } is set
F2 is Element of the carrier of V
(L2 * M) . F2 is V24() V25() ext-real Element of REAL
M . F2 is V24() V25() ext-real Element of REAL
L1 . F2 is V24() V25() ext-real Element of REAL
r * (L1 . F2) is V24() V25() ext-real Element of REAL
(r * L1) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
L2 * (M . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
L2 * (M . F2) is V24() V25() ext-real Element of REAL
(r * L1) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
r * (L1 . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
L1 . F2 is V24() V25() ext-real Element of REAL
r * (L1 . F2) is V24() V25() ext-real Element of REAL
(r * L1) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
{ b₁ where b₁ is Element of the carrier of V : not (r * L1) . b₁ = 0 } is set
F2 is Element of the carrier of V
(r * L1) . F2 is V24() V25() ext-real Element of REAL
L1 . F2 is V24() V25() ext-real Element of REAL
M . F2 is V24() V25() ext-real Element of REAL
r * (L1 . F2) is V24() V25() ext-real Element of REAL
(L2 * M) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
L2 * (M . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
L2 * (M . F2) is V24() V25() ext-real Element of REAL
(L2 * M) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
r * (L1 . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
M . F2 is V24() V25() ext-real Element of REAL
L2 * (M . F2) is V24() V25() ext-real Element of REAL
(L2 * M) . F2 is V24() V25() ext-real Element of REAL
((L2 * M) . F2) + ((r * L1) . F2) is V24() V25() ext-real Element of REAL
((L2 * M) + (r * L1)) . F2 is V24() V25() ext-real Element of REAL
V is Relation-like Function-like set
M is Relation-like Function-like set
dom V is set
dom M is set
L1 is Relation-like Function-like set
dom L1 is set
rng L1 is set
L1 (#) M is Relation-like Function-like set
L2 is set
r is set
V . L2 is set
V . r is set
L1 . L2 is set
L1 . r is set
M . (L1 . r) is set
M . (L1 . 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
K48( the carrier of V) is set
M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier M is finite Element of K48( the carrier of V)
L1 is Element of K48( the carrier of V)
L2 is Relation-like Function-like set
dom L2 is set
rng L2 is set
r is set
L2 . r is set
L is set
r is Relation-like Function-like set
dom r is set
rng r is set
L is set
F2 is set
r . F2 is set
Btm is Element of the carrier of V
L2 . Btm is set
Btm is Element of the carrier of V
r . Btm is set
Btm is Element of the carrier of V
Funcs ( the carrier of V,REAL) is non empty FUNCTION_DOMAIN of the carrier of V, REAL
L is finite Element of K48( the carrier of V)
F2 is Element of the carrier of V
r . F2 is set
F2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier F2 is finite Element of K48( the carrier of V)
Btm is set
Top is Element of the carrier of V
F2 . Top is V24() V25() ext-real Element of REAL
Btm is set
Top is Element of the carrier of V
F2 . Top is V24() V25() ext-real Element of REAL
L2 . Top is set
M . Top 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
M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
L2 is V24() V25() ext-real Element of REAL
L2 * M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
1 - L2 is V24() V25() ext-real Element of REAL
(1 - L2) * L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
(L2 * M) + ((1 - L2) * L1) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier (L2 * M) is finite Element of K48( the carrier of V)
K48( the carrier of V) is set
Carrier M is finite Element of K48( the carrier of V)
Carrier ((1 - L2) * L1) is finite Element of K48( the carrier of V)
(Carrier (L2 * M)) /\ (Carrier ((1 - L2) * L1)) is Element of K48( the carrier of V)
Carrier L1 is finite Element of K48( the carrier of V)
F2 is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng F2 is set
len F2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Carrier ((L2 * M) + ((1 - L2) * L1)) is finite Element of K48( the carrier of V)
(Carrier ((L2 * M) + ((1 - L2) * L1))) \ (Carrier (L2 * M)) is Element of K48( the carrier of V)
(Carrier ((L2 * M) + ((1 - L2) * L1))) \ (Carrier ((1 - L2) * L1)) is Element of K48( the carrier of V)
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
len F1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Lt is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier Lt is finite Element of K48( the carrier of V)
L2 - L2 is V24() V25() ext-real Element of REAL
L2 * (1 - L2) is V24() V25() ext-real Element of REAL
(Carrier (L2 * M)) \/ (Carrier ((1 - L2) * L1)) is Element of K48( the carrier of V)
Lm is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier Lm is finite Element of K48( the carrier of V)
Lb is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier Lb is finite Element of K48( the carrier of V)
Sum Lt is Element of the carrier of V
Ft is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng Ft is set
Lt (#) Ft is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (Lt (#) Ft) is Element of the carrier of V
Sum Lb is Element of the carrier of V
Fb is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng Fb is set
Lb (#) Fb is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (Lb (#) Fb) is Element of the carrier of V
Sum Lm is Element of the carrier of V
Fm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng Fm is set
Lm (#) Fm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
Sum (Lm (#) Fm) is Element of the carrier of V
Ft ^ Fm is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (Ft ^ Fm) is set
(rng Ft) \/ (rng Fm) is set
(Carrier M) \/ (Carrier L1) is Element of K48( the carrier of V)
((Carrier M) \/ (Carrier L1)) \ (Carrier L1) is Element of K48( the carrier of V)
(Carrier M) /\ (Carrier L1) is Element of K48( the carrier of V)
(((Carrier M) \/ (Carrier L1)) \ (Carrier L1)) \/ ((Carrier M) /\ (Carrier L1)) is Element of K48( the carrier of V)
(Carrier M) \ (Carrier L1) is Element of K48( the carrier of V)
(Carrier L1) \ (Carrier L1) is Element of K48( the carrier of V)
((Carrier M) \ (Carrier L1)) \/ ((Carrier L1) \ (Carrier L1)) is Element of K48( the carrier of V)
(((Carrier M) \ (Carrier L1)) \/ ((Carrier L1) \ (Carrier L1))) \/ ((Carrier M) /\ (Carrier L1)) is Element of K48( the carrier of V)
((Carrier M) \ (Carrier L1)) \/ {} is set
(((Carrier M) \ (Carrier L1)) \/ {}) \/ ((Carrier M) /\ (Carrier L1)) is set
(Carrier M) \ ((Carrier L1) \ (Carrier L1)) is Element of K48( the carrier of V)
(Carrier M) \ {} is Element of K48( the carrier of V)
(Ft ^ Fm) ^ Fb is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
f2 is Relation-like NAT -defined REAL -valued Function-like finite 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 V133() V134() V135() V136() V137() V138() Element of K48(NAT)
f2 is Relation-like NAT -defined REAL -valued Function-like finite 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 V133() V134() V135() V136() V137() V138() Element of K48(NAT)
len Ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
ft is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
rng ft is set
ft is set
fm1 is Relation-like Function-like set
dom fm1 is set
rng fm1 is set
fm1 is set
ft . fm1 is set
fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
ft . fm2 is set
Ft . fm2 is set
M . (Ft . fm2) is V24() V25() ext-real set
Seg (len Ft) is finite len Ft -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Ft ) } is set
dom Ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fb is Element of the carrier of V
len Fm is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fm1 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fm1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fm1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
rng fm1 is set
fm1 is set
fm2 is Relation-like Function-like set
dom fm2 is set
rng fm2 is set
fb is set
fm1 . fb is set
fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fm1 . fm2 is set
Fm . fm2 is set
M . (Fm . fm2) is V24() V25() ext-real set
Seg (len Fm) is finite len Fm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fm ) } is set
dom Fm is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fb is Element of the carrier of V
fm2 is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fm2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
ft is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
fm1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
ft ^ fm1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
dom (ft ^ fm1) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fb is set
(ft ^ fm1) . fb is V24() V25() ext-real set
(Ft ^ Fm) . fb is set
M . ((Ft ^ Fm) . fb) is V24() V25() ext-real set
fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Seg (len Ft) is finite len Ft -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Ft ) } is set
dom Ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
ft . fm2 is V24() V25() ext-real set
Ft . fm2 is set
M . (Ft . fm2) is V24() V25() ext-real set
(ft ^ fm1) . fm2 is V24() V25() ext-real set
dom fm1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fb is V8() V12() ext-real non negative set
(len ft) + fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ft) + fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len Fm) is finite len Fm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fm ) } is set
dom Fm is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
(ft ^ fm1) . fm2 is V24() V25() ext-real set
fm1 . fb is V24() V25() ext-real set
Fm . fb is set
M . (Fm . fb) is V24() V25() ext-real set
fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom fm1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
len ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom (Ft ^ Fm) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom M is set
fb is set
(Ft ^ Fm) . fb is set
len (ft ^ fm1) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len fm1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ft) + (len fm1) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len (Ft ^ Fm) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len (ft ^ fm1)) is finite len (ft ^ fm1) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len (ft ^ fm1) ) } is set
(Carrier Lt) \/ (Carrier Lm) is Element of K48( the carrier of V)
M * (Ft ^ Fm) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() Element of K48(K49(NAT,REAL))
dom L1 is set
dom F2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fb is set
F2 . fb is set
Seg (len F2) is finite len F2 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len F2 ) } is set
len Fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fb is Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like set
len fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
rng fm2 is set
fm2 is set
fb is Relation-like Function-like set
dom fb is set
rng fb is set
f is set
fm2 . f is set
f1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fm2 . f1 is set
Fm . f1 is set
L1 . (Fm . f1) is V24() V25() ext-real set
Seg (len Fm) is finite len Fm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fm ) } is set
dom Fm is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is Element of the carrier of V
L2 * fm1 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
K525(L2) is Relation-like REAL -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(REAL,REAL))
fm1 (#) K525(L2) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() set
len (L2 * fm1) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len fm1 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fm2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
(1 - L2) * fm2 is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
K525((1 - L2)) is Relation-like REAL -defined REAL -valued Function-like quasi_total V123() V124() V125() Element of K48(K49(REAL,REAL))
fm2 (#) K525((1 - L2)) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() set
len ((1 - L2) * fm2) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
rng fb is set
fb is set
f is Relation-like Function-like set
dom f is set
rng f is set
f1 is set
fb . f1 is set
x is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
fb . x is set
Fb . x is set
L1 . (Fb . x) is V24() V25() ext-real set
Seg (len Fb) is finite len Fb -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fb ) } is set
dom Fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
n is Element of the carrier of V
L2 * ft is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
ft (#) K525(L2) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() set
(L2 * fm1) + ((1 - L2) * fm2) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
(L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2)) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
fb is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
(1 - L2) * fb is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
fb (#) K525((1 - L2)) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() set
((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb) is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
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
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 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
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)
len (((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ((1 - L2) * fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2)))) + (len ((1 - L2) * fb)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len (L2 * ft) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ((L2 * fm1) + ((1 - L2) * fm2)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len (L2 * ft)) + (len ((L2 * fm1) + ((1 - L2) * fm2))) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
((len (L2 * ft)) + (len ((L2 * fm1) + ((1 - L2) * fm2)))) + (len ((1 - L2) * fb)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ft is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ft) + (len ((L2 * fm1) + ((1 - L2) * fm2))) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
((len ft) + (len ((L2 * fm1) + ((1 - L2) * fm2)))) + (len ((1 - L2) * fb)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len fb is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
((len ft) + (len ((L2 * fm1) + ((1 - L2) * fm2)))) + (len fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ft) + (len (L2 * fm1)) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
((len ft) + (len (L2 * fm1))) + (len fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len Ft) + (len Fm) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
((len Ft) + (len Fm)) + (len Fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len (Ft ^ Fm) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len (Ft ^ Fm)) + (len Fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len ((Ft ^ Fm) ^ Fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom F1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is set
F1 . x is set
Seg (len F1) is finite len F1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len F1 ) } is set
(Carrier Lt) \/ (Carrier Lm) is Element of K48( the carrier of V)
x is set
f1 . x is V24() V25() ext-real set
F1 . x is set
M . (F1 . x) is V24() V25() ext-real set
M * F1 is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() Element of K48(K49(NAT,REAL))
Sum (ft ^ fm1) is V24() V25() ext-real Element of REAL
K243(REAL,(ft ^ fm1),K180()) is V24() V25() ext-real Element of REAL
Fm ^ Fb is Relation-like NAT -defined the carrier of V -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of the carrier of V
rng (Fm ^ Fb) is set
(Carrier Lm) \/ (Carrier Lb) is Element of K48( the carrier of V)
x is set
f2 . x is V24() V25() ext-real set
F2 . x is set
L1 . (F2 . x) is V24() V25() ext-real set
L1 * F2 is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() Element of K48(K49(NAT,REAL))
((Carrier ((L2 * M) + ((1 - L2) * L1))) \ (Carrier (L2 * M))) \/ ((Carrier (L2 * M)) /\ (Carrier ((1 - L2) * L1))) is Element of K48( the carrier of V)
((Carrier M) \/ (Carrier L1)) \ (Carrier M) is Element of K48( the carrier of V)
(((Carrier M) \/ (Carrier L1)) \ (Carrier M)) \/ ((Carrier M) /\ (Carrier L1)) is Element of K48( the carrier of V)
(Carrier M) \ (Carrier M) is Element of K48( the carrier of V)
(Carrier L1) \ (Carrier M) is Element of K48( the carrier of V)
((Carrier M) \ (Carrier M)) \/ ((Carrier L1) \ (Carrier M)) is Element of K48( the carrier of V)
(((Carrier M) \ (Carrier M)) \/ ((Carrier L1) \ (Carrier M))) \/ ((Carrier M) /\ (Carrier L1)) is Element of K48( the carrier of V)
((Carrier L1) \ (Carrier M)) \/ {} is set
(((Carrier L1) \ (Carrier M)) \/ {}) \/ ((Carrier M) /\ (Carrier L1)) is set
(Carrier L1) \ ((Carrier M) \ (Carrier M)) is Element of K48( the carrier of V)
(Carrier L1) \ {} is Element of K48( the carrier of V)
dom (((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)) . x is V24() V25() ext-real set
((Ft ^ Fm) ^ Fb) . x is set
((L2 * M) + ((1 - L2) * L1)) . (((Ft ^ Fm) ^ Fb) . x) is V24() V25() ext-real set
dom ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) . x is V24() V25() ext-real set
dom (L2 * ft) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Seg (len (Ft ^ Fm)) is finite len (Ft ^ Fm) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len (Ft ^ Fm) ) } is set
(Ft ^ Fm) . x is set
dom ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Seg (len Ft) is finite len Ft -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Ft ) } is set
dom Ft is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Ft . x is set
(L2 * ft) . x is V24() V25() ext-real set
ft . x is V24() V25() ext-real set
L2 * (ft . x) is V24() V25() ext-real Element of REAL
M . (Ft . x) is V24() V25() ext-real set
L2 * (M . (Ft . x)) is V24() V25() ext-real Element of REAL
n is Element of the carrier of V
L1 . n is V24() V25() ext-real Element of REAL
(1 - L2) * (L1 . n) is V24() V25() ext-real Element of REAL
((1 - L2) * L1) . n is V24() V25() ext-real Element of REAL
(L2 * M) . n is V24() V25() ext-real Element of REAL
((L2 * M) . n) + (((1 - L2) * L1) . n) is V24() V25() ext-real Element of REAL
((L2 * M) + ((1 - L2) * L1)) . (Ft . x) is V24() V25() ext-real set
m is set
F1 . m is set
m9 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len f1) is finite len f1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len f1 ) } is set
f1 . m9 is V24() V25() ext-real set
F1 . m9 is set
M . (F1 . m9) is V24() V25() ext-real set
dom ((L2 * fm1) + ((1 - L2) * fm2)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
n is V8() V12() ext-real non negative set
(len (L2 * ft)) + n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len (L2 * ft)) + n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom Fm is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Fm . n is set
dom fm1 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom fm2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
((L2 * fm1) + ((1 - L2) * fm2)) . n is V24() V25() ext-real set
(L2 * fm1) . n is V24() V25() ext-real set
((1 - L2) * fm2) . n is V24() V25() ext-real set
((L2 * fm1) . n) + (((1 - L2) * fm2) . n) is set
fm1 . n is V24() V25() ext-real set
L2 * (fm1 . n) is V24() V25() ext-real Element of REAL
(L2 * (fm1 . n)) + (((1 - L2) * fm2) . n) is V24() V25() ext-real Element of REAL
fm2 . n is V24() V25() ext-real set
(1 - L2) * (fm2 . n) is V24() V25() ext-real Element of REAL
(L2 * (fm1 . n)) + ((1 - L2) * (fm2 . n)) is V24() V25() ext-real Element of REAL
M . (Fm . n) is V24() V25() ext-real set
L2 * (M . (Fm . n)) is V24() V25() ext-real Element of REAL
(L2 * (M . (Fm . n))) + ((1 - L2) * (fm2 . n)) is V24() V25() ext-real Element of REAL
L1 . (Fm . n) is V24() V25() ext-real set
(1 - L2) * (L1 . (Fm . n)) is V24() V25() ext-real Element of REAL
(L2 * (M . (Fm . n))) + ((1 - L2) * (L1 . (Fm . n))) is V24() V25() ext-real Element of REAL
Seg (len (Ft ^ Fm)) is finite len (Ft ^ Fm) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len (Ft ^ Fm) ) } is set
(Ft ^ Fm) . x is set
m is Element of the carrier of V
M . m is V24() V25() ext-real Element of REAL
L2 * (M . m) is V24() V25() ext-real Element of REAL
(L2 * M) . (Fm . n) is V24() V25() ext-real set
L1 . m is V24() V25() ext-real Element of REAL
(1 - L2) * (L1 . m) is V24() V25() ext-real Element of REAL
((1 - L2) * L1) . (Fm . n) is V24() V25() ext-real set
((L2 * M) + ((1 - L2) * L1)) . (Fm . n) is V24() V25() ext-real set
m9 is set
F1 . m9 is set
m9 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len F1) is finite len F1 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len F1 ) } is set
f1 . m9 is V24() V25() ext-real set
F1 . m9 is set
M . (F1 . m9) is V24() V25() ext-real set
m9 is set
F2 . m9 is set
m9 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len F2) is finite len F2 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len F2 ) } is set
f2 . m9 is V24() V25() ext-real set
F2 . m9 is set
L1 . (F2 . m9) is V24() V25() ext-real set
0 + 0 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom (L2 * ft) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom ((L2 * fm1) + ((1 - L2) * fm2)) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom ((1 - L2) * fb) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
n is V8() V12() ext-real non negative set
(len ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2)))) + n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2)))) + n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Seg (len Fb) is finite len Fb -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fb ) } is set
dom Fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Fb . n is set
((1 - L2) * fb) . n is V24() V25() ext-real set
fb . n is V24() V25() ext-real set
(1 - L2) * (fb . n) is V24() V25() ext-real Element of REAL
L1 . (Fb . n) is V24() V25() ext-real set
(1 - L2) * (L1 . (Fb . n)) is V24() V25() ext-real Element of REAL
m is Element of the carrier of V
M . m is V24() V25() ext-real Element of REAL
L2 * (M . m) is V24() V25() ext-real Element of REAL
(L2 * M) . m is V24() V25() ext-real Element of REAL
((1 - L2) * L1) . m is V24() V25() ext-real Element of REAL
((L2 * M) . m) + (((1 - L2) * L1) . m) is V24() V25() ext-real Element of REAL
((L2 * M) + ((1 - L2) * L1)) . (Fb . n) is V24() V25() ext-real set
m9 is set
F2 . m9 is set
m9 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len F2) is finite len F2 -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len F2 ) } is set
f2 . m9 is V24() V25() ext-real set
F2 . m9 is set
L1 . (F2 . m9) is V24() V25() ext-real set
dom ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom ((1 - L2) * fb) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is V8() V12() ext-real non negative set
(((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)) . x is V24() V25() ext-real set
((Ft ^ Fm) ^ Fb) . x is set
((L2 * M) + ((1 - L2) * L1)) . (((Ft ^ Fm) ^ Fb) . x) is V24() V25() ext-real set
(Carrier ((L2 * M) + ((1 - L2) * L1))) \ (Carrier M) is Element of K48( the carrier of V)
fm2 ^ fb is Relation-like NAT -defined REAL -valued Function-like finite FinSequence-like FinSubsequence-like V123() V124() V125() FinSequence of REAL
dom (fm2 ^ fb) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is set
(fm2 ^ fb) . x is V24() V25() ext-real set
(Fm ^ Fb) . x is set
L1 . ((Fm ^ Fb) . x) is V24() V25() ext-real set
n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fm2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
Seg (len Fm) is finite len Fm -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fm ) } is set
dom Fm is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
fm2 . n is V24() V25() ext-real set
Fm . n is set
L1 . (Fm . n) is V24() V25() ext-real set
(fm2 ^ fb) . n is V24() V25() ext-real set
dom fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
m is V8() V12() ext-real non negative set
(len fm2) + m is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
m is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len fm2) + m is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len Fb) is finite len Fb -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len Fb ) } is set
dom Fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
(fm2 ^ fb) . n is V24() V25() ext-real set
fb . m is V24() V25() ext-real set
Fb . m is set
L1 . (Fb . m) is V24() V25() ext-real set
n is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom fm2 is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
dom fb is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
len fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
dom (Fm ^ Fb) is V133() V134() V135() V136() V137() V138() Element of K48(NAT)
x is set
(Fm ^ Fb) . x is set
len (fm2 ^ fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len fm2 is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
(len fm2) + (len fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
len (Fm ^ Fb) is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT
Seg (len (fm2 ^ fb)) is finite len (fm2 ^ fb) -element V133() V134() V135() V136() V137() V138() Element of K48(NAT)
{ b₁ where b₁ is V8() V12() V24() V25() V30() V31() ext-real non negative V133() V134() V135() V136() V137() V138() Element of NAT : ( 1 <= b₁ & b₁ <= len (fm2 ^ fb) ) } is set
L1 * (Fm ^ Fb) is Relation-like NAT -defined REAL -valued Function-like V123() V124() V125() Element of K48(K49(NAT,REAL))
Sum (fm2 ^ fb) is V24() V25() ext-real Element of REAL
K243(REAL,(fm2 ^ fb),K180()) is V24() V25() ext-real Element of REAL
Sum (((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)) is V24() V25() ext-real Element of REAL
K243(REAL,(((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) ^ ((1 - L2) * fb)),K180()) is V24() V25() ext-real Element of REAL
Sum ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))) is V24() V25() ext-real Element of REAL
K243(REAL,((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2))),K180()) is V24() V25() ext-real Element of REAL
Sum ((1 - L2) * fb) is V24() V25() ext-real Element of REAL
K243(REAL,((1 - L2) * fb),K180()) is V24() V25() ext-real Element of REAL
(Sum ((L2 * ft) ^ ((L2 * fm1) + ((1 - L2) * fm2)))) + (Sum ((1 - L2) * fb)) is V24() V25() ext-real Element of REAL
Sum (L2 * ft) is V24() V25() ext-real Element of REAL
K243(REAL,(L2 * ft),K180()) is V24() V25() ext-real Element of REAL
Sum ((L2 * fm1) + ((1 - L2) * fm2)) is V24() V25() ext-real Element of REAL
K243(REAL,((L2 * fm1) + ((1 - L2) * fm2)),K180()) is V24() V25() ext-real Element of REAL
(Sum (L2 * ft)) + (Sum ((L2 * fm1) + ((1 - L2) * fm2))) is V24() V25() ext-real Element of REAL
((Sum (L2 * ft)) + (Sum ((L2 * fm1) + ((1 - L2) * fm2)))) + (Sum ((1 - L2) * fb)) is V24() V25() ext-real Element of REAL
Sum ft is V24() V25() ext-real Element of REAL
K243(REAL,ft,K180()) is V24() V25() ext-real Element of REAL
L2 * (Sum ft) is V24() V25() ext-real Element of REAL
(L2 * (Sum ft)) + (Sum ((L2 * fm1) + ((1 - L2) * fm2))) is V24() V25() ext-real Element of REAL
((L2 * (Sum ft)) + (Sum ((L2 * fm1) + ((1 - L2) * fm2)))) + (Sum ((1 - L2) * fb)) is V24() V25() ext-real Element of REAL
Sum fb is V24() V25() ext-real Element of REAL
K243(REAL,fb,K180()) is V24() V25() ext-real Element of REAL
(1 - L2) * (Sum fb) is V24() V25() ext-real Element of REAL
((L2 * (Sum ft)) + (Sum ((L2 * fm1) + ((1 - L2) * fm2)))) + ((1 - L2) * (Sum fb)) is V24() V25() ext-real Element of REAL
Sum (L2 * fm1) is V24() V25() ext-real Element of REAL
K243(REAL,(L2 * fm1),K180()) is V24() V25() ext-real Element of REAL
Sum ((1 - L2) * fm2) is V24() V25() ext-real Element of REAL
K243(REAL,((1 - L2) * fm2),K180()) is V24() V25() ext-real Element of REAL
(Sum (L2 * fm1)) + (Sum ((1 - L2) * fm2)) is V24() V25() ext-real Element of REAL
(L2 * (Sum ft)) + ((Sum (L2 * fm1)) + (Sum ((1 - L2) * fm2))) is V24() V25() ext-real Element of REAL
((L2 * (Sum ft)) + ((Sum (L2 * fm1)) + (Sum ((1 - L2) * fm2)))) + ((1 - L2) * (Sum fb)) is V24() V25() ext-real Element of REAL
Sum fm1 is V24() V25() ext-real Element of REAL
K243(REAL,fm1,K180()) is V24() V25() ext-real Element of REAL
L2 * (Sum fm1) is V24() V25() ext-real Element of REAL
(L2 * (Sum fm1)) + (Sum ((1 - L2) * fm2)) is V24() V25() ext-real Element of REAL
(L2 * (Sum ft)) + ((L2 * (Sum fm1)) + (Sum ((1 - L2) * fm2))) is V24() V25() ext-real Element of REAL
((L2 * (Sum ft)) + ((L2 * (Sum fm1)) + (Sum ((1 - L2) * fm2)))) + ((1 - L2) * (Sum fb)) is V24() V25() ext-real Element of REAL
Sum fm2 is V24() V25() ext-real Element of REAL
K243(REAL,fm2,K180()) is V24() V25() ext-real Element of REAL
(1 - L2) * (Sum fm2) is V24() V25() ext-real Element of REAL
(L2 * (Sum fm1)) + ((1 - L2) * (Sum fm2)) is V24() V25() ext-real Element of REAL
(L2 * (Sum ft)) + ((L2 * (Sum fm1)) + ((1 - L2) * (Sum fm2))) is V24() V25() ext-real Element of REAL
((L2 * (Sum ft)) + ((L2 * (Sum fm1)) + ((1 - L2) * (Sum fm2)))) + ((1 - L2) * (Sum fb)) is V24() V25() ext-real Element of REAL
(Sum ft) + (Sum fm1) is V24() V25() ext-real Element of REAL
L2 * ((Sum ft) + (Sum fm1)) is V24() V25() ext-real Element of REAL
(Sum fm2) + (Sum fb) is V24() V25() ext-real Element of REAL
(1 - L2) * ((Sum fm2) + (Sum fb)) is V24() V25() ext-real Element of REAL
(L2 * ((Sum ft) + (Sum fm1))) + ((1 - L2) * ((Sum fm2) + (Sum fb))) is V24() V25() ext-real Element of REAL
L2 * (Sum (ft ^ fm1)) is V24() V25() ext-real Element of REAL
(L2 * (Sum (ft ^ fm1))) + ((1 - L2) * ((Sum fm2) + (Sum fb))) is V24() V25() ext-real Element of REAL
L2 * 1 is V24() V25() ext-real Element of REAL
(1 - L2) * 1 is V24() V25() ext-real Element of REAL
(L2 * 1) + ((1 - L2) * 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
rng ((Ft ^ Fm) ^ Fb) is set
(Carrier M) \/ ((Carrier ((L2 * M) + ((1 - L2) * L1))) \ (Carrier M)) is Element of K48( the carrier of V)
(Carrier M) \/ (Carrier ((L2 * M) + ((1 - L2) * L1))) is Element of K48( 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 non empty Element of K48( the carrier of V)
L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of M
L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of M
r is V24() V25() ext-real Element of REAL
r * L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
1 - r is V24() V25() ext-real Element of REAL
(1 - r) * L2 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
(r * L1) + ((1 - r) * L2) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
V is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() RLSStruct
M is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
L1 is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
M + L1 is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
Up (M + L1) is non empty Element of K48( the carrier of V)
the carrier of V is non empty set
K48( the carrier of V) is set
Up M is non empty Element of K48( the carrier of V)
Up L1 is non empty Element of K48( the carrier of V)
(Up M) + (Up L1) is Element of K48( 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
M is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
L1 is non empty V73() V74() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
M /\ L1 is non empty V73() V74() strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V106() Subspace of V
Up (M /\ L1) is non empty Element of K48( the carrier of V)
the carrier of V is non empty set
K48( the carrier of V) is set
Up M is non empty Element of K48( the carrier of V)
Up L1 is non empty Element of K48( the carrier of V)
(Up M) /\ (Up L1) is Element of K48( 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
L2 is V24() V25() ext-real Element of REAL
r is V24() V25() ext-real Element of REAL
L2 * r is V24() V25() ext-real Element of REAL
M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
L2 * M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() convex Linear_Combination of V
r * L1 is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
(L2 * M) + (r * L1) is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier ((L2 * M) + (r * L1)) is finite Element of K48( the carrier of V)
K48( the carrier of V) is set
Carrier (L2 * M) is finite Element of K48( the carrier of V)
Carrier (r * L1) is finite Element of K48( the carrier of V)
(Carrier (L2 * M)) \/ (Carrier (r * L1)) is Element of K48( the carrier of V)
V is Relation-like Function-like set
M is Relation-like Function-like set
L1 is set
dom V is set
L2 is set
dom M is set
V . L1 is set
V . 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
K48( the carrier of V) is set
L1 is Element of K48( the carrier of V)
M is Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V123() V124() V125() Linear_Combination of V
Carrier M is finite Element of K48( the carrier of V)