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)) & k = card (rng f) holds

k <= (2 * [/(Sum a)\]) - 1

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k <= (2 * [/(Sum a)\]) - 1

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & k = card (rng f) implies k <= (2 * [/(Sum a)\]) - 1 )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BK00: k = card (rng f) ; :: thesis: k <= (2 * [/(Sum a)\]) - 1

Sum a <= [/(Sum a)\] by INT_1:def 7;

then k div 2 < [/(Sum a)\] by HL00, BK00, NF960, XXREAL_0:2;

then (k div 2) + 1 <= [/(Sum a)\] by INT_1:7;

then F29: ((k div 2) + 1) - 1 <= [/(Sum a)\] - 1 by XREAL_1:9;

F40: (k - 1) / 2 <= k div 2

then ((k - 1) / 2) * 2 <= ([/(Sum a)\] - 1) * 2 by XREAL_1:64;

then (k - 1) + 1 <= ((2 * [/(Sum a)\]) - 2) + 1 by XREAL_1:7;

hence k <= (2 * [/(Sum a)\]) - 1 ; :: thesis: verum

for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k <= (2 * [/(Sum a)\]) - 1

let f be non empty FinSequence of NAT ; :: thesis: for k being Nat st f = OnlinePacking (a,(NextFit a)) & k = card (rng f) holds

k <= (2 * [/(Sum a)\]) - 1

let k be Nat; :: thesis: ( f = OnlinePacking (a,(NextFit a)) & k = card (rng f) implies k <= (2 * [/(Sum a)\]) - 1 )

assume that

HL00: f = OnlinePacking (a,(NextFit a)) and

BK00: k = card (rng f) ; :: thesis: k <= (2 * [/(Sum a)\]) - 1

Sum a <= [/(Sum a)\] by INT_1:def 7;

then k div 2 < [/(Sum a)\] by HL00, BK00, NF960, XXREAL_0:2;

then (k div 2) + 1 <= [/(Sum a)\] by INT_1:7;

then F29: ((k div 2) + 1) - 1 <= [/(Sum a)\] - 1 by XREAL_1:9;

F40: (k - 1) / 2 <= k div 2

proof
end;

(k - 1) / 2 <= [/(Sum a)\] - 1
by F29, F40, XXREAL_0:2;then ((k - 1) / 2) * 2 <= ([/(Sum a)\] - 1) * 2 by XREAL_1:64;

then (k - 1) + 1 <= ((2 * [/(Sum a)\]) - 2) + 1 by XREAL_1:7;

hence k <= (2 * [/(Sum a)\]) - 1 ; :: thesis: verum