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