let y, z, w be Real; :: thesis: ( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) )
A1: cosh w <> 0 by Lm1;
( cosh y <> 0 & cosh z <> 0 ) by Lm1;
then A2: (cosh y) * (cosh z) <> 0 by XCMPLX_1:6;
A3: cosh ((y + z) + w) = ((cosh (y + z)) * (cosh w)) + ((sinh (y + z)) * (sinh w)) by Lm10
.= ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (cosh w)) + ((sinh (y + z)) * (sinh w)) by Lm10
.= ((((cosh y) * (cosh z)) * (cosh w)) + (((sinh y) * (sinh z)) * (cosh w))) + ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (sinh w)) by Lm10
.= ((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + ((((sinh y) * (sinh w)) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) by Lm14
.= ((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + (((((tanh w) * (tanh y)) * ((cosh w) * (cosh y))) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) by Lm14
.= ((1 + ((tanh y) * (tanh z))) * (((cosh y) * (cosh z)) * (cosh w))) + (((((tanh z) * (tanh w)) * ((cosh z) * (cosh w))) * (cosh y)) + (((tanh w) * (tanh y)) * (((cosh y) * (cosh z)) * (cosh w)))) by Lm14
.= (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) ;
A4: sinh ((y + z) + w) = ((sinh (y + z)) * (cosh w)) + ((cosh (y + z)) * (sinh w)) by Lm10
.= ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((cosh (y + z)) * (sinh w)) by Lm10
.= ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm10
.= ((((tanh y) * ((cosh y) * (cosh z))) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm14
.= ((((tanh y) * ((cosh y) * (cosh z))) + ((tanh z) * ((cosh y) * (cosh z)))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) by Lm14
.= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((cosh z) * (sinh w))) + (((sinh y) * (sinh z)) * (sinh w)))
.= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((tanh w) * ((cosh z) * (cosh w)))) + (((sinh y) * (sinh z)) * (sinh w))) by Lm14
.= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * (sinh z)) * (sinh w))) by Lm14
.= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * ((tanh z) * (cosh z))) * (sinh w))) by Lm14
.= (((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * ((tanh w) * (cosh w)))) by Lm14
.= ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) ;
then tanh ((y + z) + w) = (((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (((cosh y) * (cosh z)) * (cosh w))) / ((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (((cosh y) * (cosh z)) * (cosh w))) by
.= ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) by ;
hence ( sinh ((y + z) + w) = ((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) & cosh ((y + z) + w) = (((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) & tanh ((y + z) + w) = ((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) ) by A4, A3; :: thesis: verum