let z be Complex; :: thesis: exp (z + ((2 * PI) * <i>)) = exp z
z + ((2 * PI) * <i>) = ((Re z) + ((Im z) * <i>)) + (((2 * PI) + (0 * <i>)) * <i>) by COMPLEX1:13
.= ((Re z) + 0) + (((Im z) + (2 * PI)) * <i>) ;
then exp (z + ((2 * PI) * <i>)) = ((exp_R . (Re z)) * (cos . ((Im z) + ((2 * PI) * 1)))) + (((exp_R . (Re z)) * (sin . ((Im z) + (2 * PI)))) * <i>) by Th19
.= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . ((Im z) + ((2 * PI) * 1)))) * <i>) by SIN_COS2:11
.= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . (Im z))) * <i>) by SIN_COS2:10
.= exp ((Re z) + ((Im z) * <i>)) by Th19 ;
hence exp (z + ((2 * PI) * <i>)) = exp z by COMPLEX1:13; :: thesis: verum