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