len (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) = n + 1 by Th25;
then sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) <> 0_. F_Complex by POLYNOM4:3;
hence sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2) is non-zero by UPROOTS:def 5; :: thesis: verum