theorem NF807: :: BINPACK1:31

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, k being Nat st 1 <= i & i <= len a & rng (h . i) = Seg k holds
(h . i) . i = k