let n be Nat; :: thesis:
assume L010: n is odd ; :: thesis:
L020: 1 <= n by L010, NF992;
set epsilon = 1 / (n + 1);
defpred S₁[ Nat, object ] means ( ( $1 is odd implies $2 = 2 * (1 / (n + 1)) ) & ( $1 is even implies $2 = 1 - (1 / (n + 1)) ) );
L100: for i being Nat st i in Seg n holds
ex x being object st S₁[i,x]

proof

let i be Nat; :: thesis:
assume i in Seg n ; :: thesis:

per cases ;

suppose i is odd ; :: thesis:

hence ex x being object st S₁[i,x] ; :: thesis:

end;

suppose i is even ; :: thesis:

hence ex x being object st S₁[i,x] ; :: thesis:

end;

end;

end;

consider a0 being FinSequence such that
L200: dom a0 = Seg n and
L210: for i being Nat st i in Seg n holds
S₁[i,a0 . i] from FINSEQ_1:sch 1(L100);
for i being Nat st i in dom a0 holds
a0 . i in REAL

proof

let i be Nat; :: thesis:
assume L309: i in dom a0 ; :: thesis:

per cases ;

suppose i is odd ; :: thesis:

then a0 . i = 2 * (1 / (n + 1)) by L309, L200, L210;
hence a0 . i in REAL by XREAL_0:def 1; :: thesis:

end;

suppose i is even ; :: thesis:

then a0 . i = 1 - (1 / (n + 1)) by L309, L200, L210;
hence a0 . i in REAL by XREAL_0:def 1; :: thesis:

end;

end;

end;

then reconsider a0 = a0 as non empty FinSequence of REAL by NF315, L010, L200;
L500: a0 is positive

proof

1 + 1 <= n + 1 by L010, NF992, XREAL_1:6;
then ( 2 <= n or 2 = n + 1 ) by NAT_1:8;

per cases ;

suppose B000: n = 1 ; :: thesis:

for y being object holds
( y in {(2 * (1 / (n + 1)))} iff ex x being object st
( x in dom a0 & y = a0 . x ) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in {(2 * (1 / (n + 1)))} ; :: thesis:
then L410: y = 2 * (1 / (n + 1)) by TARSKI:def 1;
set x0 = 1;
L415: 1 in Seg n by L020;
L420: 1 in dom a0 by L020, L200;
reconsider x0 = 1 as Nat ;
x0 mod 2 = 1 by NAT_D:14;
then x0 is odd by NAT_2:22;
then y = a0 . x0 by L415, L210, L410;
hence ex x being object st
( x in dom a0 & y = a0 . x ) by L420; :: thesis:

end;

given x0 being object such that L440: x0 in dom a0 and
L442: y = a0 . x0 ; :: thesis:
L455: x0 = 1 by L440, L200, B000, FINSEQ_1:2, TARSKI:def 1;
reconsider x0 = x0 as Nat by L440;
x0 mod 2 = 1 by L455, NAT_D:14;
then L460: x0 is odd by NAT_2:22;
a0 . x0 = 2 * (1 / (n + 1)) by L440, L200, L460, L210;
hence y in {(2 * (1 / (n + 1)))} by L442, TARSKI:def 1; :: thesis:

end;

then L480: rng a0 = {(2 * (1 / (n + 1)))} by FUNCT_1:def 3;
for r being Real st r in rng a0 holds
0 < r

proof

let r be Real; :: thesis:
assume L489: r in rng a0 ; :: thesis:
0 / (n + 1) < 1 / (n + 1) by XREAL_1:74;
then 0 * 2 < (1 / (n + 1)) * 2 by XREAL_1:68;
hence 0 < r by L489, L480, TARSKI:def 1; :: thesis:

end;

hence a0 is positive by PARTFUN3:def 1; :: thesis:

end;

suppose B500: 2 <= n ; :: thesis:

for y being object holds
( y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} iff ex x being object st
( x in dom a0 & y = a0 . x ) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} ; :: thesis:

per cases by TARSKI:def 2;

suppose L410: y = 2 * (1 / (n + 1)) ; :: thesis:

set x0 = 1;
L415: 1 in Seg n by L020;
L420: 1 in dom a0 by L020, L200;
reconsider x0 = 1 as Nat ;
x0 = (2 * 0) + 1 ;
then y = a0 . x0 by L415, L210, L410;
hence ex x being object st
( x in dom a0 & y = a0 . x ) by L420; :: thesis:

end;

suppose L430: y = 1 - (1 / (n + 1)) ; :: thesis:

set x0 = 2;
L415: 2 in Seg n by B500;
L420: 2 in dom a0 by L200, B500;
reconsider x0 = 2 as Nat ;
x0 = 2 * 1 ;
then y = a0 . x0 by L415, L210, L430;
hence ex x being object st
( x in dom a0 & y = a0 . x ) by L420; :: thesis:

end;

end;

end;

given x0 being object such that L440: x0 in dom a0 and
L442: y = a0 . x0 ; :: thesis:
reconsider x0 = x0 as Nat by L440;

per cases ;

suppose x0 is odd ; :: thesis:

S₁[x0,a0 . x0] by L440, L200, L210;
hence y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} by L442, TARSKI:def 2; :: thesis:

end;

suppose x0 is even ; :: thesis:

S₁[x0,a0 . x0] by L440, L200, L210;
hence y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} by L442, TARSKI:def 2; :: thesis:

end;

end;

end;

then L480: rng a0 = {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} by FUNCT_1:def 3;
for r being Real st r in rng a0 holds
0 < r

proof

let r be Real; :: thesis:
assume r in rng a0 ; :: thesis:

per cases by L480, TARSKI:def 2;

suppose L490: r = 2 * (1 / (n + 1)) ; :: thesis:

0 / (n + 1) < 1 / (n + 1) by XREAL_1:74;
then 0 * 2 < (1 / (n + 1)) * 2 by XREAL_1:68;
hence 0 < r by L490; :: thesis:

end;

suppose L495: r = 1 - (1 / (n + 1)) ; :: thesis:

1 < (n + 1) * 1 by L010, NF992, NAT_1:13;
then 1 / (n + 1) < 1 by XREAL_1:83;
hence 0 < r by XREAL_1:50, L495; :: thesis:

end;

end;

end;

hence a0 is positive by PARTFUN3:def 1; :: thesis:

end;

end;

end;

for i being Nat st 1 <= i & i <= len a0 holds
a0 . i <= 1

proof

let i be Nat; :: thesis:
assume ( 1 <= i & i <= len a0 ) ; :: thesis:
then L510: i in Seg n by FINSEQ_3:25, L200;

per cases ;

suppose i is odd ; :: thesis:

then L530: a0 . i = 2 * (1 / (n + 1)) by L510, L210;
1 + 1 <= n + 1 by L010, NF992, XREAL_1:6;
then (2 * 1) / (n + 1) <= 1 by XREAL_1:183;
hence a0 . i <= 1 by XCMPLX_1:74, L530; :: thesis:

end;

suppose L560: i is even ; :: thesis:

1 - (1 / (n + 1)) <= 1 - 0 by XREAL_1:10;
hence a0 . i <= 1 by L510, L560, L210; :: thesis:

end;

end;

end;

then a0 is at_most_one ;
then reconsider a0 = a0 as non empty positive at_most_one FinSequence of REAL by L500;
take a0 ; :: thesis:
L649: Seg (len a0) = Seg n by FINSEQ_1:def 3, L200;
hence len a0 = n by FINSEQ_1:6; :: thesis:
let f be non empty FinSequence of NAT ; :: thesis:
assume f = OnlinePacking (a0,(NextFit a0)) ; :: thesis:
hence n = card (rng f) by L010, L649, FINSEQ_1:6, L210, NF993; :: thesis:
thus n = (2 * (Opt a0)) - 1 by L010, L649, FINSEQ_1:6, L210, NF997; :: thesis: