for a being non empty 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
ex k being Nat st
( rng (h . i) = Seg k & (h . i) . i = k )