let n be Nat; :: thesis: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let epsilon be Real; :: thesis: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let f be non empty FinSequence of NAT ; :: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) implies for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 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 ) ) 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: for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

L020: 1 <= n by L010, NF992;

L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;

let j be Nat; :: thesis: ( j in rng f implies SumBin (a,f,{j}) <= 1 )

assume L250: j in rng f ; :: thesis: SumBin (a,f,{j}) <= 1

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

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;

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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let epsilon be Real; :: thesis: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let a be non empty positive at_most_one FinSequence of REAL ; :: thesis: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) holds

for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

let f be non empty FinSequence of NAT ; :: 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 ) ) ) & dom f = dom a & ( 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 ) ) ) implies for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 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 ) ) 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: for j being Nat st j in rng f holds

SumBin (a,f,{j}) <= 1

L020: 1 <= n by L010, NF992;

L060: (n + 1) div 2 = (n + 1) / 2 by L010, NF992;

let j be Nat; :: thesis: ( j in rng f implies SumBin (a,f,{j}) <= 1 )

assume L250: j in rng f ; :: thesis: SumBin (a,f,{j}) <= 1

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

proof

then L291:
rng f = 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 f & y = f . x ) )

L281: y = f . x0 ; :: thesis: y in Seg npd2

reconsider x0 = x0 as Nat by L280;

L283: ( 1 <= x0 & x0 <= n ) by L280, L253, FINSEQ_1:1;

end;( x in dom f & y = f . x ) )

hereby :: thesis: ( ex x being object st

( x in dom f & y = f . x ) implies y in Seg npd2 )

given x0 being object such that L280:
x0 in dom f
and ( x in dom f & y = f . x ) implies y in Seg npd2 )

assume L255:
y in Seg npd2
; :: thesis: ex x being object st

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

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;

end;( x in dom f & y = f . x )

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 then
( y0 = 1 or ( 2 <= y0 & y0 <= npd2 ) )
by L255, FINSEQ_1:1;

end;

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

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

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

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: verum

end;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: verum

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

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

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

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: verum

end;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: verum

L281: y = f . x0 ; :: thesis: y in Seg npd2

reconsider x0 = x0 as Nat by L280;

L283: ( 1 <= x0 & x0 <= n ) by L280, L253, FINSEQ_1:1;

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

end;

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

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: verum

end;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: verum

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 then
( j = 1 or ( 2 <= j & j <= npd2 ) )
by L291, L250, FINSEQ_1:1;

end;

suppose L300:
j = 1
; :: thesis: SumBin (a,f,{j}) <= 1

set OddSegn = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ;

defpred S_{1}[ Nat, object ] means $2 = (2 * $1) - 1;

L310: for i being Nat st i in Seg npd2 holds

ex x being object st S_{1}[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_{1}[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 ) )

for x1, x2 being object st x1 in dom sgmo & x2 in dom sgmo & sgmo . x1 = sgmo . x2 holds

x1 = x2

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

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

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

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 L420, FINSEQ_1:def 13, 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

(npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k

.= 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: verum

end;defpred S

L310: for i being Nat st i in Seg npd2 holds

ex x being object st S

consider sgmo being FinSequence such that

L320: dom sgmo = Seg npd2 and

L321: for i being Nat st i in Seg npd2 holds

S

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

then L370:
rng sgmo = { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }
by FUNCT_1:def 3;
let y be object ; :: thesis: ( 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 ) )

L342: y = sgmo . x0 ; :: thesis: y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }

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: verum

end;( x in dom sgmo & y = sgmo . x ) )

hereby :: thesis: ( ex x being object st

( x in dom sgmo & y = sgmo . x ) implies y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )

given x0 being object such that L340:
x0 in dom sgmo
and ( x in dom sgmo & y = sgmo . x ) implies y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )

assume
y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }
; :: thesis: ex x being object st

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

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: verum

end;( x in dom sgmo & y = sgmo . x )

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: verum

L342: y = sgmo . x0 ; :: thesis: y in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }

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: verum

for x1, x2 being object st x1 in dom sgmo & x2 in dom sgmo & sgmo . x1 = sgmo . x2 holds

x1 = x2

proof

then L380:
sgmo is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom sgmo & x2 in dom sgmo & sgmo . x1 = sgmo . x2 implies x1 = x2 )

assume that

L371: ( x1 in dom sgmo & x2 in dom sgmo ) and

L372: sgmo . x1 = sgmo . x2 ; :: thesis: x1 = x2

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: verum

end;assume that

L371: ( x1 in dom sgmo & x2 in dom sgmo ) and

L372: sgmo . x1 = sgmo . x2 ; :: thesis: x1 = x2

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: verum

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

then L420:
{ i where i is Nat : ( 1 <= i & i <= n & i is odd ) } c= Seg n
;
let x be object ; :: thesis: ( x in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } implies x in Seg n )

assume x in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ; :: thesis: x in Seg n

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: verum

end;assume x in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ; :: thesis: x in Seg n

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: verum

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

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;
let i be object ; :: thesis: ( i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } iff ( i in dom f & f . i in {j} ) )

L450: i in dom f and

L451: f . i in {j} ; :: thesis: i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }

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

end;hereby :: thesis: ( i in dom f & f . i in {j} implies i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )

assume that assume
i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }
; :: thesis: ( i in dom f & f . i in {j} )

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 . i in {j}

f . i0 = 1 by L442, L441, L220;

hence f . i in {j} by TARSKI:def 1, L440, L300; :: thesis: verum

end;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 . i in {j}

f . i0 = 1 by L442, L441, L220;

hence f . i in {j} by TARSKI:def 1, L440, L300; :: thesis: verum

L450: i in dom f and

L451: f . i in {j} ; :: thesis: i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }

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

hence
i in { i where i is Nat : ( 1 <= i & i <= n & i is odd ) }
by L454; :: thesis: verum
assume L460:
not i0 is odd
; :: thesis: contradiction

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: verum

end;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: verum

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

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 L420, FINSEQ_1:def 13, 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

L699:
for k being Nat st k in dom (npd2 |-> (2 * epsilon)) holds
reconsider npd2 = npd2 as Element of NAT by ORDINAL1:def 12;

defpred S_{2}[ Nat] means (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . $1 = (2 * $1) - 1;

_{2}[1]
;

B400: for k being Element of NAT st 1 <= k & k < npd2 & S_{2}[k] holds

S_{2}[k + 1]

S_{2}[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_{2}[k]

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

end;defpred S

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

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

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

end;

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

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: verum

end;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: verum

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

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 13; :: thesis: verum

end;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 13; :: thesis: verum

B400: for k being Element of NAT st 1 <= k & k < npd2 & S

S

proof

B900:
for k being Element of NAT st 1 <= k & k <= npd2 holds
let k be Element of NAT ; :: thesis: ( 1 <= k & k < npd2 & S_{2}[k] implies S_{2}[k + 1] )

assume that

B410: ( 1 <= k & k < npd2 ) and

B412: S_{2}[k]
; :: thesis: S_{2}[k + 1]

_{2}[k + 1]
; :: thesis: verum

end;assume that

B410: ( 1 <= k & k < npd2 ) and

B412: S

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

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

end;per cases then
( (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (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;

end;

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

(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

hence contradiction by L420, FINSEQ_1:def 13; :: thesis: verum

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

( 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;
assume B521:
not ((Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) . (k + 1)) + 1 <> (2 * k) + 1
; :: thesis: contradiction

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: verum

end;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: verum

hence contradiction by L420, FINSEQ_1:def 13; :: thesis: verum

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

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;

end;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: l <= k + 1

assume B740:
not l <= k + 1
; :: thesis: contradiction

1 + 0 <= k + 1 by XREAL_1:7;

hence contradiction by B740, B737, B700, B730, L420, FINSEQ_1:def 13; :: thesis: verum

end;1 + 0 <= k + 1 by XREAL_1:7;

hence contradiction by B740, B737, B700, B730, L420, FINSEQ_1:def 13; :: thesis: verum

B769: now :: thesis: l >= k

assume B760:
not l >= k
; :: thesis: contradiction

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 13; :: thesis: verum

end;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 13; :: thesis: verum

now :: thesis: l <> k

hence
contradiction
by B749, B769, B730, B700, NAT_1:9; :: thesis: verumassume
not l <> k
; :: thesis: contradiction

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: verum

end;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: verum

S

for k being Nat st k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) holds

S

proof

hence
for k being Nat st k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) holds
let k be Nat; :: thesis: ( k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) implies S_{2}[k] )

assume k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) ; :: thesis: S_{2}[k]

then B920: ( 1 <= k & k <= npd2 ) by L524, FINSEQ_1:1;

k in NAT by ORDINAL1:def 12;

hence S_{2}[k]
by B920, B900; :: thesis: verum

end;assume k in dom (Sgm { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } ) ; :: thesis: S

then B920: ( 1 <= k & k <= npd2 ) by L524, FINSEQ_1:1;

k in NAT by ORDINAL1:def 12;

hence S

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

(npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k

proof

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
let k be Nat; :: thesis: ( k in dom (npd2 |-> (2 * epsilon)) implies (npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k )

assume L530: k in dom (npd2 |-> (2 * epsilon)) ; :: thesis: (npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k

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: verum

end;assume L530: k in dom (npd2 |-> (2 * epsilon)) ; :: thesis: (npd2 |-> (2 * epsilon)) . k = (Seq (a | { i where i is Nat : ( 1 <= i & i <= n & i is odd ) } )) . k

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: verum

.= 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: verum

suppose L800:
( 2 <= j & j <= npd2 )
; :: thesis: SumBin (a,f,{j}) <= 1

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

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: verum

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

L939:
a | {tjm2} = {[tjm2,(a . tjm2)]}
by L820, L253, L205, GRFUNC_1:28;
let i be object ; :: thesis: ( i in {tjm2} iff ( i in dom f & f . i in {j} ) )

L900: i in dom f and

L901: f . i in {j} ; :: thesis: i in {tjm2}

L902: f . i = j by L901, TARSKI:def 1;

reconsider i0 = i as Nat by L900;

L910: i0 is even

then i0 / 2 = j - 1 by L902, L910, NAT_6:4;

hence i in {tjm2} by TARSKI:def 1; :: thesis: verum

end;hereby :: thesis: ( i in dom f & f . i in {j} implies i in {tjm2} )

assume that assume L869:
i in {tjm2}
; :: thesis: ( i in dom f & f . i in {j} )

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 . i in {j}

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: verum

end;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 . i in {j}

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: verum

L900: i in dom f and

L901: f . i in {j} ; :: thesis: i in {tjm2}

L902: f . i = j by L901, TARSKI:def 1;

reconsider i0 = i as Nat by L900;

L910: i0 is even

proof

then
f . i0 = (i0 div 2) + 1
by L900, L253, L220;
assume
i0 is odd
; :: thesis: contradiction

then f . i0 = 1 by L900, L253, L220;

hence contradiction by L902, L800; :: thesis: verum

end;then f . i0 = 1 by L900, L253, L220;

hence contradiction by L902, L800; :: thesis: verum

then i0 / 2 = j - 1 by L902, L910, NAT_6:4;

hence i in {tjm2} by TARSKI:def 1; :: thesis: verum

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: verum