let z1, z2 be Complex; :: thesis: ( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) )
A1: (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) = 2 * ((sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)))
.= 2 * (((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2))) by Th59
.= ((((2 * (cosh_C /. z1)) * (cosh_C /. z1)) - 1) + 1) - (2 * ((cosh_C /. z2) * (cosh_C /. z2)))
.= ((cosh_C /. (2 * z1)) + 1) - (2 * ((cosh_C /. z2) * (cosh_C /. z2))) by Th58
.= (cosh_C /. (2 * z1)) - (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1) ;
(2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) = 2 * ((cosh_C /. (z1 + z2)) * (cosh_C /. (z1 - z2)))
.= 2 * (((sinh_C /. z1) * (sinh_C /. z1)) + ((cosh_C /. z2) * (cosh_C /. z2))) by Th60
.= 2 * ((((cosh_C /. z1) * (cosh_C /. z1)) - 1) + ((cosh_C /. z2) * (cosh_C /. z2))) by Lm5
.= (((2 * (cosh_C /. z1)) * (cosh_C /. z1)) - 1) + (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1)
.= (cosh_C /. (2 * z1)) + (((2 * (cosh_C /. z2)) * (cosh_C /. z2)) - 1) by Th58
.= (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) by Th58 ;
hence ( (cosh_C /. (2 * z1)) + (cosh_C /. (2 * z2)) = (2 * (cosh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (cosh_C /. (2 * z1)) - (cosh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (sinh_C /. (z1 - z2)) ) by A1, Th58; :: thesis: verum