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 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) by Lm11
.= ((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:76
.= ((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by XCMPLX_1:91
.= 1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) by A2, XCMPLX_1:60
.= ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) by A1, Lm6, XCMPLX_1:91
.= (2 * ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2))))) / (2 * ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) by XCMPLX_1:91
.= ((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((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