theorem NF880: :: BINPACK1:28

for a being non empty positive at_most_one FinSequence of REAL
for h being non empty FinSequence of NAT * st h = OnlinePackingHistory (a,(NextFit a)) holds
for i being Nat st 1 <= i & i <= len a holds
SumBin (a,(h . i),{((h . i) . i)}) <= 1