let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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

let h be non empty FinSequence of NAT * ; :: thesis: for f being FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

ex k being Nat st rng f = Seg k

let f be FinSequence of NAT ; :: thesis: ( f = OnlinePacking (a,(NextFit a)) implies ex k being Nat st rng f = Seg k )

assume HL00: f = OnlinePacking (a,(NextFit a)) ; :: thesis: ex k being Nat st rng f = Seg k

set h = OnlinePackingHistory (a,(NextFit a));

set i = len (OnlinePackingHistory (a,(NextFit a)));

L200: 1 <= len (OnlinePackingHistory (a,(NextFit a))) by NAT_1:14;

L220: len (OnlinePackingHistory (a,(NextFit a))) <= len a by defPackHistory;

ex k being Nat st

( rng ((OnlinePackingHistory (a,(NextFit a))) . (len (OnlinePackingHistory (a,(NextFit a))))) = Seg k & ((OnlinePackingHistory (a,(NextFit a))) . (len (OnlinePackingHistory (a,(NextFit a))))) . (len (OnlinePackingHistory (a,(NextFit a)))) = k ) by L200, L220, NF805;

hence ex k being Nat st rng f = Seg k by HL00; :: thesis: verum

for f being FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

ex k being Nat st rng f = Seg k

let h be non empty FinSequence of NAT * ; :: thesis: for f being FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

ex k being Nat st rng f = Seg k

let f be FinSequence of NAT ; :: thesis: ( f = OnlinePacking (a,(NextFit a)) implies ex k being Nat st rng f = Seg k )

assume HL00: f = OnlinePacking (a,(NextFit a)) ; :: thesis: ex k being Nat st rng f = Seg k

set h = OnlinePackingHistory (a,(NextFit a));

set i = len (OnlinePackingHistory (a,(NextFit a)));

L200: 1 <= len (OnlinePackingHistory (a,(NextFit a))) by NAT_1:14;

L220: len (OnlinePackingHistory (a,(NextFit a))) <= len a by defPackHistory;

ex k being Nat st

( rng ((OnlinePackingHistory (a,(NextFit a))) . (len (OnlinePackingHistory (a,(NextFit a))))) = Seg k & ((OnlinePackingHistory (a,(NextFit a))) . (len (OnlinePackingHistory (a,(NextFit a))))) . (len (OnlinePackingHistory (a,(NextFit a)))) = k ) by L200, L220, NF805;

hence ex k being Nat st rng f = Seg k by HL00; :: thesis: verum