let a be non empty FinSequence of REAL ; for Alg being Function of [:REAL,(NAT *):],NAT
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1
let Alg be Function of [:REAL,(NAT *):],NAT; for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,Alg) holds
SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1
let h be non empty FinSequence of NAT * ; ( h = OnlinePackingHistory (a,Alg) implies SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1 )
assume HC00:
h = OnlinePackingHistory (a,Alg)
; SumBin (a,(h . 1),{((h . 1) . 1)}) = a . 1
L010:
h . 1 = {[1,1]}
by HC00, defPackHistory;
1 in Seg 1
;
then
(a | 1) . 1 = a . 1
by FUNCT_1:49;
then L049:
a | 1 = <*(a . 1)*>
by FINSEQ_1:40;
L055: Seq (a,{1}) =
Seq (a | {1})
.=
<*(a . 1)*>
by L049, FINSEQ_1:2, FINSEQ_3:157
;
thus SumBin (a,(h . 1),{((h . 1) . 1)}) =
SumBin (a,{[1,1]},{1})
by defPackHistory, L010
.=
Sum (Seq (a,{1}))
by NF501
.=
a . 1
by L055, RVSUM_1:73
; verum