for n being Nat
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