let z be Complex; :: thesis: for n being Element of NAT holds sin_C /. (z + ((2 * n) * PI)) = sin_C /. z
let n be Element of NAT ; :: thesis: sin_C /. (z + ((2 * n) * PI)) = sin_C /. z
sin_C /. (z + ((2 * n) * PI)) = ((exp ((<i> * z) + (<i> * ((2 * n) * PI)))) - (exp (- (<i> * (z + ((2 * n) * PI)))))) / (2 * <i>) by Def1
.= (((exp (<i> * z)) * (exp (((2 * PI) * n) * <i>))) - (exp (- (<i> * (z + ((2 * n) * PI)))))) / (2 * <i>) by SIN_COS:23
.= (((exp (<i> * z)) * 1) - (exp (- (<i> * (z + ((2 * n) * PI)))))) / (2 * <i>) by Th28
.= ((exp (<i> * z)) - (exp (((- <i>) * z) + ((- <i>) * ((2 * n) * PI))))) / (2 * <i>)
.= ((exp (<i> * z)) - ((exp ((- <i>) * z)) * (exp ((- ((2 * PI) * n)) * <i>)))) / (2 * <i>) by SIN_COS:23
.= ((exp (<i> * z)) - ((exp ((- <i>) * z)) * 1)) / (2 * <i>) by Th29
.= ((exp (<i> * z)) - (exp (- (<i> * z)))) / (2 * <i>) ;
hence sin_C /. (z + ((2 * n) * PI)) = sin_C /. z by Def1; :: thesis: verum