let y, z be Real; :: thesis: ( y - z <> 0 implies ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) )
assume A1: y - z <> 0 ; :: thesis: ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z))
A2: cosh ((y / 2) - (z / 2)) <> 0 by Lm1;
((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z)) by Lm11
.= ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11
.= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76
.= ((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1 by
.= ((2 * (sinh ((y + z) / 2))) * (sinh ((y - z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) by
.= ((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2))))
.= ((cosh y) - (cosh z)) / ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) by Lm11
.= ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) by Lm11 ;
hence ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = ((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) ; :: thesis: verum