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) ) )

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

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

then
Opt a = (n + 1) div 2
by defOpt;
defpred S_{1}[ 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_{1}[i,x]

L200: dom g0 = Seg n and

L210: for i being Nat st i in Seg n holds

S_{1}[i,g0 . i]
from FINSEQ_1:sch 1(L100);

for i being Nat st i in dom g0 holds

g0 . i in NAT

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 ) )

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;L100: for i being Nat st i in Seg n holds

ex x being object st S

proof

consider g0 being FinSequence such that
let i be Nat; :: thesis: ( i in Seg n implies ex x being object st S_{1}[i,x] )

assume i in Seg n ; :: thesis: ex x being object st S_{1}[i,x]

end;assume i in Seg n ; :: thesis: ex x being object st S

L200: dom g0 = Seg n and

L210: for i being Nat st i in Seg n holds

S

for i being Nat st i in dom g0 holds

g0 . i in NAT

proof

then reconsider g0 = g0 as non empty FinSequence of NAT by NF315, L010, L200;
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

end;assume L309: i in dom g0 ; :: thesis: g0 . i in NAT

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

then
rng g0 = Seg npd2
by FUNCT_1:def 3;
let y be object ; :: thesis: ( y in Seg npd2 iff ex x being object st

( x in dom g0 & y = g0 . x ) )

L442: y = g0 . x0 ; :: thesis: y in Seg npd2

reconsider x0 = x0 as Nat by L440;

end;( 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 )

given x0 being object such that L440:
x0 in dom g0
and ( 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;

end;( 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;

end;

suppose L410:
y0 = 1
; :: thesis: ex x being object st

( x in dom g0 & y = g0 . x )

( 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;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

suppose L430:
( 2 <= y0 & y0 <= npd2 )
; :: thesis: ex x being object st

( x in dom g0 & y = g0 . x )

( 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;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

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 )
;

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;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

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

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