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

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