for a being 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