theorem NF890: :: BINPACK1:29

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, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
SumBin (a,(h . i),{j}) <= 1