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