let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: for f being non empty FinSequence of NAT
for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds
for j being Nat st 1 <= j & j <= k div 2 holds
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1
let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & rng f = Seg k holds
for j being Nat st 1 <= j & j <= k div 2 holds
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1
let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & rng f = Seg k implies for j being Nat st 1 <= j & j <= k div 2 holds
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )
assume that
HL00: f = OnlinePacking (a,(NextFit a)) and
BN00: rng f = Seg k ; :: thesis: for j being Nat st 1 <= j & j <= k div 2 holds
(SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1
set h = OnlinePackingHistory (a,(NextFit a));
let j be Nat; :: thesis: ( 1 <= j & j <= k div 2 implies (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 )
assume that
L202: 1 <= j and
L203: j <= k div 2 ; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1
k <> 0 by BN00;

per cases then ( k = 1 or 2 <= k ) by NAT_1:23;

suppose k = 1 ; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

hence (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 by NAT_D:27, L202, L203; :: thesis: verum

end;

suppose L60: 2 <= k ; :: thesis: (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1

set i = len (OnlinePackingHistory (a,(NextFit a)));
L220: len (OnlinePackingHistory (a,(NextFit a))) = len a by defPackHistory;
1 <= len (OnlinePackingHistory (a,(NextFit a))) by NAT_1:14;
hence (SumBin (a,f,{((2 * j) - 1)})) + (SumBin (a,f,{(2 * j)})) > 1 by L220, NF830, L60, L202, L203, HL00, BN00; :: thesis: verum

end;

end;