let z1 be Complex; :: thesis: (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1
((cosh_C /. z1) * (cosh_C /. z1)) - 1 = ((cosh_C /. z1) * (cosh_C /. z1)) - (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) by Th8
.= (((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z1) * (cosh_C /. z1))) - ((cosh_C /. z1) * (cosh_C /. z1)) ;
hence (sinh_C /. z1) * (sinh_C /. z1) = ((cosh_C /. z1) * (cosh_C /. z1)) - 1 ; :: thesis: verum