let y, z be Real; ( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) )
A1:
cosh ((y / 2) - (z / 2)) <> 0
by Lm1;
A2:
cosh ((y / 2) + (z / 2)) <> 0
by Lm1;
A3: ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) =
((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) / ((cosh y) + (cosh z))
by Lm11
.=
(2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))))
by Lm11
.=
(2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / (2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))))
.=
((cosh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))
by XCMPLX_1:91
.=
((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))))
by XCMPLX_1:76
.=
1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))))
by A2, XCMPLX_1:60
.=
tanh ((y / 2) - (z / 2))
by Th1
;
((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) =
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z))
by Lm11
.=
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))))
by Lm11
.=
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))))
by XCMPLX_1:76
.=
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1
by A1, XCMPLX_1:60
.=
(2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))))
by XCMPLX_1:76
.=
tanh ((y / 2) + (z / 2))
by Th1
;
hence
( ((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) + (z / 2)) & ((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) = tanh ((y / 2) - (z / 2)) )
by A3; verum