theorem :: SIN_COS3:32

for n being Element of NAT holds exp ((((2 * n) + (1 / 2)) * PI) * <i>) = <i>