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