let z be Complex; :: thesis: (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2
set e1 = exp z;
set e2 = exp (- z);
(cosh_C /. z) * (cosh_C /. z) = (((exp z) + (exp (- z))) / 2) * (cosh_C /. z) by Def4
.= (((exp z) + (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2) by Def4
.= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) + (2 * ((exp z) * (exp (- z))))) / 2) / 2
.= (((((exp z) * (exp z)) + ((exp (- z)) * (exp (- z)))) + (2 * 1)) / 2) / 2 by Lm3
.= ((((exp (z + z)) + ((exp (- z)) * (exp (- z)))) + 2) / 2) / 2 by SIN_COS:23
.= ((((exp (2 * z)) + (exp ((- z) + (- z)))) + 2) / 2) / 2 by SIN_COS:23
.= ((((exp (2 * z)) + (exp (- (2 * z)))) / 2) + 1) / 2 ;
hence (cosh_C /. z) * (cosh_C /. z) = ((cosh_C /. (2 * z)) + 1) / 2 by Lm2; :: thesis: verum