theorem :: SIN_COS3:31

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