theorem NF530: :: BINPACK1:25

for a being non empty positive 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
for i, l being Nat st 1 <= i & i < len a holds
SumBin (a,(h . i),{l}) <= SumBin (a,(h . (i + 1)),{l})