let z be Complex; :: thesis: ( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 )
set e1 = exp z;
set e2 = exp (- z);
A1: ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 = (2 * ((cosh_C /. z) * (cosh_C /. z))) - 1
.= (2 * (((cosh_C /. (2 * z)) + 1) / 2)) - 1 by Th57
.= ((cosh_C /. (2 * z)) + 1) - 1 ;
(2 * (sinh_C /. z)) * (cosh_C /. z) = 2 * ((sinh_C /. z) * (cosh_C /. z))
.= 2 * ((sinh_C /. z) * (((exp z) + (exp (- z))) / 2)) by Def4
.= 2 * ((((exp z) - (exp (- z))) / 2) * (((exp z) + (exp (- z))) / 2)) by Def3
.= (((exp z) * (exp z)) - ((exp (- z)) * (exp (- z)))) / 2
.= ((exp (z + z)) - ((exp (- z)) * (exp (- z)))) / 2 by SIN_COS:23
.= ((exp (2 * z)) - (exp ((- z) + (- z)))) / 2 by SIN_COS:23
.= ((exp (2 * z)) - (exp (- (2 * z)))) / 2
.= sinh_C /. (2 * z) by Lm1 ;
hence ( sinh_C /. (2 * z) = (2 * (sinh_C /. z)) * (cosh_C /. z) & cosh_C /. (2 * z) = ((2 * (cosh_C /. z)) * (cosh_C /. z)) - 1 ) by A1; :: thesis: verum