let y, z be Real; :: thesis: ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z))
A1: ( cosh y <> 0 & cosh z <> 0 ) by Lm1;
((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = ((sinh (y + z)) / ((cosh y) * (cosh z))) / ((tanh y) - (tanh z)) by Lm11
.= ((sinh (y + z)) / ((cosh y) * (cosh z))) / ((sinh (y - z)) / ((cosh y) * (cosh z))) by Lm11
.= (sinh (y + z)) / (sinh (y - z)) by A1, XCMPLX_1:6, XCMPLX_1:55 ;
hence ((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) = (sinh (y + z)) / (sinh (y - z)) ; :: thesis: verum