let n be Nat; :: thesis: ( n is odd implies ex a being non empty positive at_most_one FinSequence of REAL st

( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) ) )

assume L010: n is odd ; :: thesis: ex a being non empty positive at_most_one FinSequence of REAL st

( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) )

L020: 1 <= n by L010, NF992;

set epsilon = 1 / (n + 1);

defpred S_{1}[ 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_{1}[i,x]

L200: dom a0 = Seg n and

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

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

for i being Nat st i in dom a0 holds

a0 . i in REAL

L500: a0 is positive

a0 . i <= 1

then reconsider a0 = a0 as non empty positive at_most_one FinSequence of REAL by L500;

take a0 ; :: thesis: ( len a0 = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a0,(NextFit a0)) holds

( n = card (rng f) & n = (2 * (Opt a0)) - 1 ) ) )

L649: Seg (len a0) = Seg n by FINSEQ_1:def 3, L200;

hence len a0 = n by FINSEQ_1:6; :: thesis: for f being non empty FinSequence of NAT st f = OnlinePacking (a0,(NextFit a0)) holds

( n = card (rng f) & n = (2 * (Opt a0)) - 1 )

let f be non empty FinSequence of NAT ; :: thesis: ( f = OnlinePacking (a0,(NextFit a0)) implies ( n = card (rng f) & n = (2 * (Opt a0)) - 1 ) )

assume f = OnlinePacking (a0,(NextFit a0)) ; :: thesis: ( n = card (rng f) & n = (2 * (Opt a0)) - 1 )

hence n = card (rng f) by L010, L649, FINSEQ_1:6, L210, NF993; :: thesis: n = (2 * (Opt a0)) - 1

thus n = (2 * (Opt a0)) - 1 by L010, L649, FINSEQ_1:6, L210, NF997; :: thesis: verum

( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) ) )

assume L010: n is odd ; :: thesis: ex a being non empty positive at_most_one FinSequence of REAL st

( len a = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a,(NextFit a)) holds

( n = card (rng f) & n = (2 * (Opt a)) - 1 ) ) )

L020: 1 <= n by L010, NF992;

set epsilon = 1 / (n + 1);

defpred S

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

ex x being object st S

proof

consider a0 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 a0 = Seg n and

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

S

for i being Nat st i in dom a0 holds

a0 . i in REAL

proof

then reconsider a0 = a0 as non empty FinSequence of REAL by NF315, L010, L200;
let i be Nat; :: thesis: ( i in dom a0 implies a0 . i in REAL )

assume L309: i in dom a0 ; :: thesis: a0 . i in REAL

end;assume L309: i in dom a0 ; :: thesis: a0 . i in REAL

L500: a0 is positive

proof

for i being Nat st 1 <= i & i <= len a0 holds
1 + 1 <= n + 1
by L010, NF992, XREAL_1:6;

then ( 2 <= n or 2 = n + 1 ) by NAT_1:8;

end;then ( 2 <= n or 2 = n + 1 ) by NAT_1:8;

per cases then
( n = 1 or 2 <= n )
;

end;

suppose B000:
n = 1
; :: thesis: a0 is positive

for y being object holds

( y in {(2 * (1 / (n + 1)))} iff ex x being object st

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

for r being Real st r in rng a0 holds

0 < r

end;( y in {(2 * (1 / (n + 1)))} iff ex x being object st

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

proof

then L480:
rng a0 = {(2 * (1 / (n + 1)))}
by FUNCT_1:def 3;
let y be object ; :: thesis: ( y in {(2 * (1 / (n + 1)))} iff ex x being object st

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

L442: y = a0 . x0 ; :: thesis: y in {(2 * (1 / (n + 1)))}

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

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

hereby :: thesis: ( ex x being object st

( x in dom a0 & y = a0 . x ) implies y in {(2 * (1 / (n + 1)))} )

given x0 being object such that L440:
x0 in dom a0
and ( x in dom a0 & y = a0 . x ) implies y in {(2 * (1 / (n + 1)))} )

assume
y in {(2 * (1 / (n + 1)))}
; :: thesis: ex x being object st

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

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

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

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

L442: y = a0 . x0 ; :: thesis: y in {(2 * (1 / (n + 1)))}

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

for r being Real st r in rng a0 holds

0 < r

proof

hence
a0 is positive
by PARTFUN3:def 1; :: thesis: verum
let r be Real; :: thesis: ( r in rng a0 implies 0 < r )

assume L489: r in rng a0 ; :: thesis: 0 < r

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

end;assume L489: r in rng a0 ; :: thesis: 0 < r

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

suppose B500:
2 <= n
; :: thesis: a0 is positive

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

for r being Real st r in rng a0 holds

0 < r

end;( y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} iff ex x being object st

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

proof

then L480:
rng a0 = {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))}
by FUNCT_1:def 3;
let y be object ; :: thesis: ( y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} iff ex x being object st

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

L442: y = a0 . x0 ; :: thesis: y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))}

reconsider x0 = x0 as Nat by L440;

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

hereby :: thesis: ( ex x being object st

( x in dom a0 & y = a0 . x ) implies y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} )

given x0 being object such that L440:
x0 in dom a0
and ( x in dom a0 & y = a0 . x ) implies y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))} )

assume
y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))}
; :: thesis: ex x being object st

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

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

per cases then
( y = 2 * (1 / (n + 1)) or y = 1 - (1 / (n + 1)) )
by TARSKI:def 2;

end;

suppose L410:
y = 2 * (1 / (n + 1))
; :: thesis: ex x being object st

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

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

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

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

suppose L430:
y = 1 - (1 / (n + 1))
; :: thesis: ex x being object st

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

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

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

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

L442: y = a0 . x0 ; :: thesis: y in {(2 * (1 / (n + 1))),(1 - (1 / (n + 1)))}

reconsider x0 = x0 as Nat by L440;

for r being Real st r in rng a0 holds

0 < r

proof

hence
a0 is positive
by PARTFUN3:def 1; :: thesis: verum
let r be Real; :: thesis: ( r in rng a0 implies 0 < r )

assume r in rng a0 ; :: thesis: 0 < r

end;assume r in rng a0 ; :: thesis: 0 < r

a0 . i <= 1

proof

then
a0 is at_most_one
;
let i be Nat; :: thesis: ( 1 <= i & i <= len a0 implies a0 . i <= 1 )

assume ( 1 <= i & i <= len a0 ) ; :: thesis: a0 . i <= 1

then L510: i in Seg n by FINSEQ_3:25, L200;

end;assume ( 1 <= i & i <= len a0 ) ; :: thesis: a0 . i <= 1

then L510: i in Seg n by FINSEQ_3:25, L200;

then reconsider a0 = a0 as non empty positive at_most_one FinSequence of REAL by L500;

take a0 ; :: thesis: ( len a0 = n & ( for f being non empty FinSequence of NAT st f = OnlinePacking (a0,(NextFit a0)) holds

( n = card (rng f) & n = (2 * (Opt a0)) - 1 ) ) )

L649: Seg (len a0) = Seg n by FINSEQ_1:def 3, L200;

hence len a0 = n by FINSEQ_1:6; :: thesis: for f being non empty FinSequence of NAT st f = OnlinePacking (a0,(NextFit a0)) holds

( n = card (rng f) & n = (2 * (Opt a0)) - 1 )

let f be non empty FinSequence of NAT ; :: thesis: ( f = OnlinePacking (a0,(NextFit a0)) implies ( n = card (rng f) & n = (2 * (Opt a0)) - 1 ) )

assume f = OnlinePacking (a0,(NextFit a0)) ; :: thesis: ( n = card (rng f) & n = (2 * (Opt a0)) - 1 )

hence n = card (rng f) by L010, L649, FINSEQ_1:6, L210, NF993; :: thesis: n = (2 * (Opt a0)) - 1

thus n = (2 * (Opt a0)) - 1 by L010, L649, FINSEQ_1:6, L210, NF997; :: thesis: verum