theorem :: SIN_COS3:27

for z being Complex holds exp (z + ((2 * PI) * <i>)) = exp z