theorem Th23: :: BASEL_2:23

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