let y, z be Real; :: thesis: ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2))
((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) - (cosh z)) by Lm11
.= ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) by Lm11
.= ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (sinh ((y - z) / 2)))
.= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2)))) by XCMPLX_1:76
.= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by SIN_COS5:def 1
.= ((2 / 2) * ((cosh ((y / 2) + (z / 2))) / (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) by XCMPLX_1:76
.= (coth ((y + z) / 2)) * (coth ((y - z) / 2)) by SIN_COS5:def 1 ;
hence ((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) = (coth ((y + z) / 2)) * (coth ((y - z) / 2)) ; :: thesis: verum