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 * (Opt 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 * (Opt a)) - 1

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

assume that

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

BK00: k = card (rng f) ; :: thesis: k <= (2 * (Opt a)) - 1

F200: k <= (2 * [/(Sum a)\]) - 1 by HL00, BK00, NF980;

2 * [/(Sum a)\] <= 2 * (Opt a) by NF330, XREAL_1:64;

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

hence k <= (2 * (Opt a)) - 1 by F200, XXREAL_0:2; :: thesis: verum

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

k <= (2 * (Opt 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 * (Opt a)) - 1

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

assume that

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

BK00: k = card (rng f) ; :: thesis: k <= (2 * (Opt a)) - 1

F200: k <= (2 * [/(Sum a)\]) - 1 by HL00, BK00, NF980;

2 * [/(Sum a)\] <= 2 * (Opt a) by NF330, XREAL_1:64;

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

hence k <= (2 * (Opt a)) - 1 by F200, XXREAL_0:2; :: thesis: verum