theorem Th25: :: BASEL_2:25

for n being Nat holds len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1