let n be Nat; :: thesis:
let epsilon be Real; :: thesis:
let a be non empty positive at_most_one FinSequence of REAL ; :: thesis:
let f be non empty FinSequence of NAT ; :: thesis:
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 ) ) and
L205: dom f = dom a and
L220: for i being Nat st i in Seg n holds
( ( i is odd implies f . i = 1 ) & ( i is even implies f . i = (i div 2) + 1 ) ) ; :: thesis:
L020: 1 <= n by L010, NF992;
L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;
let j be Nat; :: thesis:
assume L250: j in rng f ; :: thesis:
set npd2 = (n + 1) div 2;
1 + 1 <= n + 1 by L010, NF992, XREAL_1:6;
then L189: 2 / 2 <= (n + 1) / 2 by XREAL_1:72;
reconsider npd2 = (n + 1) div 2 as Nat by L010, L060;
L253: dom f = Seg n by L205, FINSEQ_1:def 3, L030;
for y being object holds
( y in Seg npd2 iff ex x being object st
( x in dom f & y = f . x ) )

let y be object ; :: thesis:

hereby :: thesis:

assume L255: y in Seg npd2 ; :: thesis:
then reconsider y0 = y as Nat ;
( 1 <= y0 & y0 <= npd2 ) by L255, 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 by L255, FINSEQ_1:1;

suppose L260: y0 = 1 ; :: thesis:

set x0 = 1;
L262: 1 in Seg n by L020;
L263: 1 in dom f by L020, L253;
1 = (2 * 0) + 1 ;
then f . 1 = y0 by L262, L220, L260;
hence ex x being object st
( x in dom f & y = f . x ) by L263; :: thesis:

end;

suppose L270: ( 2 <= y0 & y0 <= npd2 ) ; :: thesis:

set x0 = (y0 - 1) * 2;
2 - 1 <= y0 - 1 by XREAL_1:9, L270;
then 1 * 2 <= (y0 - 1) * 2 by XREAL_1:64;
then L272: 2 - 1 <= ((y0 - 1) * 2) - 0 by XREAL_1:13;
reconsider x0 = (y0 - 1) * 2 as Nat by L270;
y0 * 2 <= ((n + 1) / 2) * 2 by L060, L270, XREAL_1:64;
then (y0 * 2) - 1 <= n by XREAL_1:20;
then L2735: ((y0 * 2) - 1) - 1 <= n - 0 by XREAL_1:13;
then L275: x0 in Seg n by L272;
L276: x0 in dom f by L253, L272, L2735;
f . x0 = (x0 div 2) + 1 by L275, L220
.= (((y0 - 1) * 2) / 2) + 1 by NAT_6:4
.= y0 ;
hence ex x being object st
( x in dom f & y = f . x ) by L276; :: thesis:

end;

given x0 being object such that L280: x0 in dom f and
L281: y = f . x0 ; :: thesis:
reconsider x0 = x0 as Nat by L280;
L283: ( 1 <= x0 & x0 <= n ) by L280, L253, FINSEQ_1:1;

per cases ;

suppose x0 is odd ; :: thesis:

then f . x0 = 1 by L280, L253, L220;
hence y in Seg npd2 by L281, L189, L060; :: thesis:

end;

suppose L284: x0 is even ; :: thesis:

then L2845: f . x0 = (x0 div 2) + 1 by L280, L253, L220;
reconsider y0 = y as Integer by L281;
L286: y0 = (x0 / 2) + 1 by L2845, L281, L284, NAT_6:4;
L2865: 0 + 1 <= (x0 / 2) + 1 by XREAL_1:6;
reconsider y0 = y0 as Nat by L281;
x0 + 1 <= n + 1 by XREAL_1:6, L283;
then x0 + 1 <= n by L284, L010, NAT_1:8;
then (x0 + 1) + 1 <= n + 1 by XREAL_1:6;
then (x0 + 2) / 2 <= (n + 1) / 2 by XREAL_1:72;
then y0 <= npd2 by L010, NF992, L286;
hence y in Seg npd2 by L286, L2865; :: thesis:

end;

then L291: rng f = Seg npd2 by FUNCT_1:def 3;
then ( 1 <= j & j <= npd2 ) by L250, FINSEQ_1:1;
then 1 + 1 <= j + 1 by XREAL_1:6;
then ( 2 <= j or 2 = j + 1 ) by NAT_1:8;

per cases by L291, L250, FINSEQ_1:1;

suppose L300: j = 1 ; :: thesis:

set OddSegn = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ;
defpred S₁[ Nat, object ] means $2 = (2 * $1) - 1;
L310: for i being Nat st i in Seg npd2 holds
ex x being object st S₁[i,x] ;
consider sgmo being FinSequence such that
L320: dom sgmo = Seg npd2 and
L321: for i being Nat st i in Seg npd2 holds
S₁[i,sgmo . i] from FINSEQ_1:sch 1(L310);
for y being object holds
( y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } iff ex x being object st
( x in dom sgmo & y = sgmo . x ) )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ; :: thesis:
then consider y0 being Nat such that
L322: y0 = y and
L323: ( 1 <= y0 & y0 <= n & y0 is odd ) ;
set x0 = (y0 + 1) div 2;
((y0 + 1) div 2) * 2 = ((y0 + 1) / 2) * 2 by L323, NAT_6:4
.= y0 + 1 ;
then L326: y0 = (2 * ((y0 + 1) div 2)) - 1 ;
then 1 + 1 <= 2 * ((y0 + 1) div 2) by L323, XREAL_1:19;
then L3265: 2 / 2 <= (((y0 + 1) div 2) * 2) / 2 by XREAL_1:72;
then (y0 + 1) div 2 in NAT by INT_1:3;
then reconsider x0 = (y0 + 1) div 2 as Nat ;
x0 * 2 <= n + 1 by L323, L326, XREAL_1:20;
then L3275: (x0 * 2) / 2 <= (n + 1) / 2 by XREAL_1:72;
then L329: x0 in Seg npd2 by L3265, L060;
L330: x0 in dom sgmo by L3265, L3275, L060, L320;
y0 = sgmo . x0 by L329, L321, L326;
hence ex x being object st
( x in dom sgmo & y = sgmo . x ) by L330, L322; :: thesis:

end;

given x0 being object such that L340: x0 in dom sgmo and
L342: y = sgmo . x0 ; :: thesis:
reconsider x0 = x0 as Nat by L340;
L351: ( 1 <= x0 & x0 <= npd2 ) by L340, L320, FINSEQ_1:1;
L352: y = (2 * x0) - 1 by L340, L320, L321, L342;
then reconsider y0 = y as Integer ;
1 * 2 <= x0 * 2 by L351, XREAL_1:64;
then L359: 2 - 1 <= (2 * x0) - 1 by XREAL_1:9;
then 1 <= y0 by L340, L320, L321, L342;
then y0 in NAT by INT_1:3;
then reconsider y0 = y0 as Nat ;
x0 * 2 <= ((n + 1) / 2) * 2 by L351, L060, XREAL_1:64;
then y0 <= n by XREAL_1:20, L352;
hence y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by L359, L352; :: thesis:

end;

then L370: rng sgmo = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by FUNCT_1:def 3;
for x1, x2 being object st x1 in dom sgmo & x2 in dom sgmo & sgmo . x1 = sgmo . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis:
assume that
L371: ( x1 in dom sgmo & x2 in dom sgmo ) and
L372: sgmo . x1 = sgmo . x2 ; :: thesis:
reconsider x01 = x1, x02 = x2 as Nat by L371;
( sgmo . x01 = (2 * x01) - 1 & sgmo . x02 = (2 * x02) - 1 ) by L320, L371, L321;
then (2 * x01) - 1 = (2 * x02) - 1 by L372;
hence x1 = x2 ; :: thesis:

end;

then L380: sgmo is one-to-one by FUNCT_1:def 4;
L395: card (Seg npd2) = npd2 by FINSEQ_1:57;
L419: for x being object st x in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } holds
x in Seg n

proof

let x be object ; :: thesis:
assume x in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ; :: thesis:
then consider x0 being Nat such that
L410: x0 = x and
L411: ( 1 <= x0 & x0 <= n & x0 is odd ) ;
thus x in Seg n by L410, L411; :: thesis:

end;

then L420: { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } c= Seg n ;
then l420: { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } is included_in_Seg ;
L430: len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) = card { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by l420, FINSEQ_3:39
.= npd2 by L320, L370, L380, WELLORD2:def 4, L395, CARD_1:5 ;
L505: dom a = Seg n by FINSEQ_1:def 3, L030;
then L510: { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } c= dom a by L419;
then L512: dom (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by RELAT_1:62;
L522: dom (Sgm (dom (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ))) = dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L510, RELAT_1:62;
L499: for i being object holds
( i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } iff ( i in dom f & f . i in {j} ) )

proof

let i be object ; :: thesis:

hereby :: thesis:

assume i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ; :: thesis:
then consider i0 being Nat such that
L440: i0 = i and
L441: ( 1 <= i0 & i0 <= n & i0 is odd ) ;
L442: i0 in Seg n by L441;
thus i in dom f by L441, L505, L205, L440; :: thesis:
f . i0 = 1 by L442, L441, L220;
hence f . i in {j} by TARSKI:def 1, L440, L300; :: thesis:

end;

assume that
L450: i in dom f and
L451: f . i in {j} ; :: thesis:
L452: f . i = 1 by L451, TARSKI:def 1, L300;
reconsider i0 = i as Nat by L450;
L454: ( 1 <= i0 & i0 <= n ) by L450, L205, L505, FINSEQ_1:1;
i0 is odd

proof

assume L460: not i0 is odd ; :: thesis:
0 / 2 < i0 / 2 by L454, XREAL_1:74;
then 0 < i0 div 2 by L460, NAT_6:4;
then 0 + 1 < (i0 div 2) + 1 by XREAL_1:6;
hence contradiction by L460, L450, L205, L505, L220, L452; :: thesis:

end;

hence i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by L454; :: thesis:

end;

L515: Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) = (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) * (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L510, RELAT_1:62;
then reconsider aosgmo = (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) * (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) as FinSequence ;
L525: rng (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by l420, FINSEQ_1:def 14;
rng (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) c= dom (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by FINSEQ_1:def 14, L512;
then L520: len (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) = len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L515, FINSEQ_2:29
.= len (npd2 |-> (2 * epsilon)) by L430, CARD_1:def 7 ;
reconsider co = card { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } as Nat by L370;
L524: dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) = Seg co by l420, FINSEQ_3:40
.= Seg npd2 by L320, L370, L380, WELLORD2:def 4, L395, CARD_1:5 ;
L526: for k being Nat st k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) holds
(Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k = (2 * k) - 1

proof

reconsider npd2 = npd2 as Element of NAT by ORDINAL1:def 12;
defpred S₂[ Nat] means (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . $1 = (2 * $1) - 1;

now :: thesis:

assume not (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 = 1 ; :: thesis:

per cases ) . 1 < 1 or (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 > 1 ) by XXREAL_0:1;

suppose B210: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 < 1 ; :: thesis:

1 in Seg npd2 by L189, L060;
then (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 in rng (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L524, FUNCT_1:3;
then consider i being Nat such that
B211: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 = i and
B212: 1 <= i and
i <= n and
i is odd by L525;
thus contradiction by B211, B212, B210; :: thesis:

end;

suppose B218: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . 1 > 1 ; :: thesis:

1 = (2 * 0) + 1 ;
then 1 in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by L020;
then consider l being object such that
B220: l in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) and
B230: 1 = (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . l by L525, FUNCT_1:def 3;
reconsider l = l as Nat by B220;
B237: ( 1 <= l & l <= len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) ) by L430, L524, B220, FINSEQ_1:1;
then 1 < l by XXREAL_0:1, B230, B218;
hence contradiction by B237, B230, B218, l420, FINSEQ_1:def 14; :: thesis:

end;

then B300: S₂[1] ;
B400: for k being Element of NAT st 1 <= k & k < npd2 & S₂[k] holds
S₂[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume that
B410: ( 1 <= k & k < npd2 ) and
B412: S₂[k] ; :: thesis:

now :: thesis:

assume not (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) = (2 * (k + 1)) - 1 ; :: thesis:

per cases ) . (k + 1) < (2 * (k + 1)) - 1 or (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) > (2 * (k + 1)) - 1 ) by XXREAL_0:1;

suppose B500: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) < (2 * (k + 1)) - 1 ; :: thesis:

(Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) <= ((2 * (k + 1)) - 1) - 1 by B500, INT_1:52;
then B510: ((Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1)) + 1 <= (2 * k) + 1 by XREAL_1:6;
B520: ((Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1)) + 1 <> (2 * k) + 1

proof

assume B521: not ((Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1)) + 1 <> (2 * k) + 1 ; :: thesis:
B523: 1 + 0 <= k + 1 by XREAL_1:7;
B524: k + 1 <= npd2 by B410, INT_1:7;
k + 1 in Seg npd2 by B523, B524;
then 2 * k in rng (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L524, B521, FUNCT_1:3;
then consider i being Nat such that
B525: 2 * k = i and
( 1 <= i & i <= n ) and
B526: i is odd by L525;
thus contradiction by B525, B526; :: thesis:

end;

( 1 <= k & k < k + 1 & k + 1 <= len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) & (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k >= (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) ) by B410, XREAL_1:29, XREAL_1:19, L430, B510, B520, NAT_1:8, B412;
hence contradiction by l420, FINSEQ_1:def 14; :: thesis:

end;

suppose B700: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1) > (2 * (k + 1)) - 1 ; :: thesis:

0 <= ((2 * k) + (2 * 1)) - 1 ;
then reconsider i0 = (2 * (k + 1)) - 1 as Nat ;
B710: 0 + 1 <= (2 * k) + 1 by XREAL_1:6;
k <= npd2 - 1 by B410, INT_1:52;
then (k + 1) * 2 <= ((n + 1) / 2) * 2 by L060, XREAL_1:19, XREAL_1:64;
then B717: i0 <= n by XREAL_1:20;
(2 * (k + 1)) - 1 in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } by B710, B717;
then consider l being object such that
B720: l in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) and
B730: (2 * (k + 1)) - 1 = (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . l by L525, FUNCT_1:def 3;
reconsider l = l as Nat by B720;
B737: ( 1 <= l & l <= len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) ) by L430, L524, B720, FINSEQ_1:1;

B749: now :: thesis:

assume B740: not l <= k + 1 ; :: thesis:
1 + 0 <= k + 1 by XREAL_1:7;
hence contradiction by B740, B737, B700, B730, l420, FINSEQ_1:def 14; :: thesis:

end;

B769: now :: thesis:

assume B760: not l >= k ; :: thesis:
2 * (k + 1) > 2 * k by XREAL_1:29, XREAL_1:68;
then ( 1 <= l & l < k & k <= len (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) & (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . l > (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k ) by XREAL_1:9, B730, B412, L430, L524, B720, FINSEQ_1:1, B760, B410;
hence contradiction by l420, FINSEQ_1:def 14; :: thesis:

end;

now :: thesis:

assume not l <> k ; :: thesis:
then (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k = (2 * (k + 1)) - 1 by B730;
hence contradiction by B412; :: thesis:

end;

hence contradiction by B749, B769, B730, B700, NAT_1:9; :: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

B900: for k being Element of NAT st 1 <= k & k <= npd2 holds
S₂[k] from INT_1:sch 7(B300, B400);
for k being Nat st k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) holds
S₂[k]

proof

let k be Nat; :: thesis:
assume k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) ; :: thesis:
then B920: ( 1 <= k & k <= npd2 ) by L524, FINSEQ_1:1;
k in NAT by ORDINAL1:def 12;
hence S₂[k] by B920, B900; :: thesis:

end;

hence for k being Nat st k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) holds
(Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k = (2 * k) - 1 ; :: thesis:

end;

L699: for k being Nat st k in dom (npd2 |-> (2 * epsilon)) holds
(npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k

proof

let k be Nat; :: thesis:
assume L530: k in dom (npd2 |-> (2 * epsilon)) ; :: thesis:
L535: len (npd2 |-> (2 * epsilon)) = npd2 by CARD_1:def 7;
L536: dom (npd2 |-> (2 * epsilon)) = Seg (len (npd2 |-> (2 * epsilon))) by FINSEQ_1:def 3;
L537: k in Seg npd2 by FINSEQ_1:def 3, L530, L535;
then L630: (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . k = (2 * k) - 1 by L526, L524;
then L655: (2 * k) - 1 in Seg n by L537, L524, FUNCT_1:3, L525, L419;
(a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . ((2 * k) - 1) = a . ((2 * k) - 1) by L537, L524, FUNCT_1:3, L630, L525, FUNCT_1:49
.= 2 * epsilon by L655, L050 ;
then (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . ((Sgm (dom (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ))) . k) = 2 * epsilon by L630, L505, L420, RELAT_1:62;
then (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k = 2 * epsilon by L522, L524, L537, FUNCT_1:13;
hence (npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k by L536, L530, L535, FINSEQ_2:57; :: thesis:

end;

L750: Seq (a,(f " {j})) = Seq (a, { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) by L499, FUNCT_1:def 7
.= Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )
.= npd2 |-> (2 * epsilon) by L699, L520, FINSEQ_2:9 ;
npd2 * (2 * epsilon) = ((n + 1) / 2) * (2 * epsilon) by L010, NF992
.= (((n + 1) / 2) * 2) * epsilon
.= 1 by L040, XCMPLX_1:106 ;
hence SumBin (a,f,{j}) <= 1 by L750, RVSUM_1:80; :: thesis:

end;

suppose L800: ( 2 <= j & j <= npd2 ) ; :: thesis:

set tjm2 = (2 * j) - 2;
2 - 1 <= j - 1 by L800, XREAL_1:9;
then L808: 1 * 2 <= (j - 1) * 2 by XREAL_1:64;
then L809: 2 - 1 <= ((j - 1) * 2) - 0 by XREAL_1:13;
(2 * j) - 2 in NAT by L808, INT_1:3;
then reconsider tjm2 = (2 * j) - 2 as Nat ;
j * 2 <= ((n + 1) / 2) * 2 by L800, L060, XREAL_1:64;
then (j * 2) - 2 <= (n + 1) - 1 by XREAL_1:13;
then L820: tjm2 in Seg n by L809;
L829: tjm2 = 2 * (j - 1) ;
then L860: a . tjm2 = 1 - epsilon by L820, L050;
L929: for i being object holds
( i in {tjm2} iff ( i in dom f & f . i in {j} ) )

proof

let i be object ; :: thesis:

hereby :: thesis:

assume L869: i in {tjm2} ; :: thesis:
then L870: i = tjm2 by TARSKI:def 1;
reconsider i0 = i as Nat by L869;
thus i in dom f by L869, TARSKI:def 1, L820, L253; :: thesis:
f . i0 = (i0 div 2) + 1 by L820, L220, L870, L829
.= (((j - 1) * 2) / 2) + 1 by L870, NAT_6:4
.= j ;
hence f . i in {j} by TARSKI:def 1; :: thesis:

end;

assume that
L900: i in dom f and
L901: f . i in {j} ; :: thesis:
L902: f . i = j by L901, TARSKI:def 1;
reconsider i0 = i as Nat by L900;
L910: i0 is even

proof

assume i0 is odd ; :: thesis:
then f . i0 = 1 by L900, L253, L220;
hence contradiction by L902, L800; :: thesis:

end;

then f . i0 = (i0 div 2) + 1 by L900, L253, L220;
then i0 / 2 = j - 1 by L902, L910, NAT_6:4;
hence i in {tjm2} by TARSKI:def 1; :: thesis:

end;

L939: a | {tjm2} = {[tjm2,(a . tjm2)]} by L820, L253, L205, GRFUNC_1:28;
Seq (a,(f " {j})) = Seq (a,{tjm2}) by L929, FUNCT_1:def 7
.= Seq (a | {tjm2})
.= <*(1 - epsilon)*> by L939, L860, FINSEQ_3:157 ;
then SumBin (a,f,{j}) = 1 - epsilon by RVSUM_1:73;
hence SumBin (a,f,{j}) <= 1 by XREAL_1:139, L040, XREAL_1:44; :: thesis:

end;