let y, z be Real; :: thesis: ( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) )
A1: cosh y <> 0 by Lm1;
then A2: sinh y = ((sinh y) / (cosh y)) * (cosh y) by XCMPLX_1:87
.= (tanh y) * (cosh y) by Th1 ;
A3: cosh z <> 0 by Lm1;
then A4: ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = (sinh y) / (cosh y) by XCMPLX_1:91
.= tanh y by Th1 ;
(sinh y) * (sinh z) = (((sinh y) * (sinh z)) / ((cosh y) * (cosh z))) * ((cosh y) * (cosh z)) by A1, A3, XCMPLX_1:6, XCMPLX_1:87
.= (((sinh y) / (cosh y)) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) by XCMPLX_1:76
.= ((tanh y) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) by Th1
.= ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) by Th1 ;
hence ( ((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) = tanh y & (sinh y) * (cosh z) = (tanh y) * ((cosh y) * (cosh z)) & sinh y = (tanh y) * (cosh y) & (sinh y) * (sinh z) = ((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) ) by A4, A2; :: thesis: verum