theorem NF993: :: BINPACK1:40

for n being Nat
for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL
for f being non empty FinSequence of NAT st n is odd & len a = n & epsilon = 1 / (n + 1) & ( for i being Nat st i in Seg n holds
( ( i is odd implies a . i = 2 * epsilon ) & ( i is even implies a . i = 1 - epsilon ) ) ) & f = OnlinePacking (a,(NextFit a)) holds
n = card (rng f)