let n be Nat; :: thesis: for epsilon being Real
for a being non empty positive at_most_one FinSequence of REAL 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 ) ) ) holds
n = (2 * (Opt a)) - 1
let epsilon be Real; :: thesis: for a being non empty positive at_most_one FinSequence of REAL 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 ) ) ) holds
n = (2 * (Opt a)) - 1
let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: ( 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 ) ) ) implies n = (2 * (Opt a)) - 1 )
assume that
L010: n is odd and
L030: len a = n and
L040: epsilon = 1 / (n + 1) and
L050: 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 ) ) ; :: thesis: n = (2 * (Opt a)) - 1
L020: 1 <= n by L010, NF992;
L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;
ex g being non empty FinSequence of NAT st
( dom g = dom a & ( for j being Nat st j in rng g holds
SumBin (a,g,{j}) <= 1 ) & (n + 1) div 2 = card (rng g) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f) ) )

proof

defpred S₁[ Nat, object ] means ( ( $1 is odd implies $2 = 1 ) & ( $1 is even implies $2 = ($1 div 2) + 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: ( i in Seg n implies ex x being object st S₁[i,x] )
assume i in Seg n ; :: thesis: ex x being object st S₁[i,x]

per cases ( i is odd or i is even ) ;

suppose i is odd ; :: thesis: ex x being object st S₁[i,x]

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

end;

suppose i is even ; :: thesis: ex x being object st S₁[i,x]

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

end;

end;

end;

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

proof

let i be Nat; :: thesis: ( i in dom g0 implies g0 . i in NAT )
assume L309: i in dom g0 ; :: thesis: g0 . i in NAT

per cases ( i is odd or i is even ) ;

suppose i is odd ; :: thesis: g0 . i in NAT

then g0 . i = 1 by L309, L200, L210;
hence g0 . i in NAT ; :: thesis: verum

end;

suppose i is even ; :: thesis: g0 . i in NAT

then L370: g0 . i = (i div 2) + 1 by L309, L200, L210;
0 <= i div 2 by INT_1:55;
hence g0 . i in NAT by INT_1:3, L370; :: thesis: verum

end;

end;

end;

then reconsider g0 = g0 as non empty FinSequence of NAT by NF315, L010, L200;
take g0 ; :: thesis: ( dom g0 = dom a & ( for j being Nat st j in rng g0 holds
SumBin (a,g0,{j}) <= 1 ) & (n + 1) div 2 = card (rng g0) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f) ) )
L379: dom a = Seg n by FINSEQ_1:def 3, L030;
thus dom g0 = dom a by FINSEQ_1:def 3, L030, L200; :: thesis: ( ( for j being Nat st j in rng g0 holds
SumBin (a,g0,{j}) <= 1 ) & (n + 1) div 2 = card (rng g0) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f) ) )
thus for j being Nat st j in rng g0 holds
SumBin (a,g0,{j}) <= 1 by L010, L030, L040, L050, L379, L200, L210, NF996; :: thesis: ( (n + 1) div 2 = card (rng g0) & ( for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f) ) )
set npd2 = (n + 1) div 2;
1 + 1 <= n + 1 by L010, NF992, XREAL_1:6;
then L388: 2 / 2 <= (n + 1) / 2 by XREAL_1:72;
reconsider npd2 = (n + 1) div 2 as Nat by L010, L060;
for y being object holds
( y in Seg npd2 iff ex x being object st
( x in dom g0 & y = g0 . x ) )

proof

let y be object ; :: thesis: ( y in Seg npd2 iff ex x being object st
( x in dom g0 & y = g0 . x ) )

hereby :: thesis: ( ex x being object st
( x in dom g0 & y = g0 . x ) implies y in Seg npd2 )

assume L405: y in Seg npd2 ; :: thesis: ex x being object st
( x in dom g0 & y = g0 . x )
reconsider y0 = y as Nat by L405;
( 1 <= y0 & y0 <= npd2 ) by L405, FINSEQ_1:1;
then 1 + 1 <= y0 + 1 by XREAL_1:6;
then ( 2 <= y0 or 2 = y0 + 1 ) by NAT_1:8;

per cases then ( y0 = 1 or ( 2 <= y0 & y0 <= npd2 ) ) by L405, FINSEQ_1:1;

suppose L410: y0 = 1 ; :: thesis: ex x being object st
( x in dom g0 & y = g0 . x )

set x0 = 1;
L415: 1 in Seg n by L020;
L420: 1 in dom g0 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 y0 = g0 . x0 by L415, L210, L410;
hence ex x being object st
( x in dom g0 & y = g0 . x ) by L420; :: thesis: verum

end;

suppose L430: ( 2 <= y0 & y0 <= npd2 ) ; :: thesis: ex x being object st
( x in dom g0 & y = g0 . x )

set x0 = (y0 - 1) * 2;
2 - 1 <= y0 - 1 by L430, XREAL_1:9;
then 1 * 2 <= (y0 - 1) * 2 by XREAL_1:64;
then L4125: 2 - 1 <= ((y0 - 1) * 2) - 0 by XREAL_1:13;
reconsider x0 = (y0 - 1) * 2 as Nat by L430;
x0 div 2 = ((y0 - 1) * 2) / 2 by NAT_6:4;
then L412: y0 = (x0 div 2) + 1 ;
y0 - 1 <= ((n + 1) / 2) - 1 by L430, L060, XREAL_1:9;
then x0 <= (((n + 1) / 2) - 1) * 2 by XREAL_1:64;
then L4135: x0 + 0 <= (n - 1) + 1 by XREAL_1:7;
then L415: x0 in Seg n by L4125;
L420: x0 in dom g0 by L4125, L4135, L200;
y0 = g0 . x0 by L415, L210, L412;
hence ex x being object st
( x in dom g0 & y = g0 . x ) by L420; :: thesis: verum

end;

end;

end;

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

per cases ( x0 is odd or x0 is even ) ;

suppose x0 is odd ; :: thesis: y in Seg npd2

then g0 . x0 = 1 by L440, L200, L210;
hence y in Seg npd2 by L442, L388, L060; :: thesis: verum

end;

suppose L470: x0 is even ; :: thesis: y in Seg npd2

then g0 . x0 = (x0 div 2) + 1 by L440, L200, L210;
then L472: y = (x0 / 2) + 1 by L442, L470, NAT_6:4;
reconsider y0 = y as Nat by L442;
L4725: 0 + 1 <= (x0 / 2) + 1 by XREAL_1:6;
L474: x0 <= n by L440, L200, FINSEQ_1:1;
( x0 + 1 <= n or not x0 + 1 <= n + 1 ) by L010, L470, NAT_1:8;
then (x0 + 1) + 1 <= n + 1 by L474, XREAL_1:6;
then (x0 + 2) / 2 <= (n + 1) / 2 by XREAL_1:72;
hence y in Seg npd2 by L4725, L442, L060, L472; :: thesis: verum

end;

end;

end;

then rng g0 = Seg npd2 by FUNCT_1:def 3;
hence (n + 1) div 2 = card (rng g0) by FINSEQ_1:57; :: thesis: for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f)
reconsider i0 = (n + 1) / 2 as Integer by L010;
reconsider r = (1 / (n + 1)) - (1 / 2) as Real ;
L810: Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2) by L010, L030, L040, L050, NF994
.= r + i0 ;
1 + 1 <= n + 1 by L010, NF992, XREAL_1:6;
then 1 * 2 <= 1 * (n + 1) ;
then 1 / (n + 1) <= 1 / 2 by XREAL_1:102;
then L820: r <= 0 by XREAL_1:47;
0 < (1 / (n + 1)) + (1 / 2) by XREAL_1:34;
then 0 < r + 1 ;
then L835: [/r\] = 0 by L820, INT_1:def 7;
[/(r + i0)\] = [/r\] + i0 by INT_1:33
.= i0 by L835 ;
then [/(Sum a)\] = (n + 1) div 2 by L810, L010, NF992;
hence for f being non empty FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
(n + 1) div 2 <= card (rng f) by NF320; :: thesis: verum

end;

then Opt a = (n + 1) div 2 by defOpt;
hence n = (2 * (Opt a)) - 1 by L060; :: thesis: verum