let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds
for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1
let f be non empty FinSequence of NAT ; :: thesis: ( f = OnlinePacking (a,(NextFit a)) implies for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 )
assume HL00: f = OnlinePacking (a,(NextFit a)) ; :: thesis: for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1
let j be Nat; :: thesis: ( j in rng f implies SumBin (a,f,{j}) <= 1 )
assume L002: j in rng f ; :: thesis: SumBin (a,f,{j}) <= 1
set h = OnlinePackingHistory (a,(NextFit a));
reconsider i = len (OnlinePackingHistory (a,(NextFit a))) as Nat ;
L200: 1 <= i by NAT_1:14;
i <= len a by defPackHistory;
hence SumBin (a,f,{j}) <= 1 by L200, L002, HL00, NF890; :: thesis: verum