for a being non empty positive at_most_one FinSequence of REAL
for h being non empty FinSequence of NAT *
for f being FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
ex k being Nat st rng f = Seg k