let z be Element of 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:24
.= (((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:24
.= ((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