let n be Nat; :: thesis: (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n = (((2 * n) + 1) choose 1) * i_FC
((2 * n) + 1) -' (2 * n) = ((2 * n) + 1) - (2 * n) by NAT_1:11, XREAL_1:233;
then A1: i_FC |^ (((2 * n) + 1) -' (2 * n)) = i_FC by BINOM:8;
(1. F_Complex) |^ (2 * n) = 1_ F_Complex by Th3;
then A2: ((1. F_Complex) |^ (2 * n)) * i_FC = i_FC ;
((2 * n) + 1) - (2 * n) = 1 ;
then A3: ((2 * n) + 1) choose (2 * n) = ((2 * n) + 1) choose 1 by NAT_1:11, NEWTON:20;
(sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n = (<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)) . (2 * n) by Def5;
hence (sieve ((<%i_FC,(1. F_Complex)%> `^ ((2 * n) + 1)),2)) . n = (((2 * n) + 1) choose 1) * i_FC by A1, A2, A3, Th13; :: thesis: verum