let y, z, w be Real; ( 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 A3, Th1
.=
((((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 A1, A2, XCMPLX_1:6, XCMPLX_1:91
;
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; verum