for z being Complex holds (sinh_C /. z) * (sinh_C /. z) = ((cosh_C /. (2 * z)) - 1) / 2