let z be Complex; :: thesis: (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2
set e1 = exp z;
set e2 = exp (- z);
(sinh_C /. z) * (sinh_C /. z) = (((exp z) - (exp (- z))) / 2) * (sinh_C /. z) by Def3
.= (((exp z) - (exp (- z))) / 2) * (((exp z) - (exp (- z))) / 2) by Def3
.= (((((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 (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2 by Lm2; :: thesis: verum