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