theorem NF994: :: BINPACK1:41

for n being Nat
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
Sum a = (((n + 1) / 2) + (1 / (n + 1))) - (1 / 2)