let y, z be Real; ( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) )
A1: (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) =
(2 * (sinh . ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))
by SIN_COS2:def 2
.=
(2 * (sinh . ((y / 2) - (z / 2)))) * (cosh . ((y / 2) + (z / 2)))
by SIN_COS2:def 4
.=
(sinh . y) - (sinh . z)
by SIN_COS2:26
.=
(sinh y) - (sinh . z)
by SIN_COS2:def 2
.=
(sinh y) - (sinh z)
by SIN_COS2:def 2
;
A2: (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) =
(2 * (cosh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))
by SIN_COS2:def 4
.=
(2 * (cosh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2)))
by SIN_COS2:def 4
.=
(cosh . y) + (cosh . z)
by SIN_COS2:27
.=
(cosh y) + (cosh . z)
by SIN_COS2:def 4
.=
(cosh y) + (cosh z)
by SIN_COS2:def 4
;
A3: (sinh (y - z)) / ((cosh y) * (cosh z)) =
(sinh . (y - z)) / ((cosh y) * (cosh z))
by SIN_COS2:def 2
.=
(sinh . (y - z)) / ((cosh . y) * (cosh z))
by SIN_COS2:def 4
.=
(sinh . (y - z)) / ((cosh . y) * (cosh . z))
by SIN_COS2:def 4
.=
(tanh . y) - (tanh . z)
by SIN_COS2:28
.=
(tanh y) - (tanh . z)
by SIN_COS2:def 6
.=
(tanh y) - (tanh z)
by SIN_COS2:def 6
;
A4: (sinh (y + z)) / ((cosh y) * (cosh z)) =
(sinh . (y + z)) / ((cosh y) * (cosh z))
by SIN_COS2:def 2
.=
(sinh . (y + z)) / ((cosh . y) * (cosh z))
by SIN_COS2:def 4
.=
(sinh . (y + z)) / ((cosh . y) * (cosh . z))
by SIN_COS2:def 4
.=
(tanh . y) + (tanh . z)
by SIN_COS2:28
.=
(tanh y) + (tanh . z)
by SIN_COS2:def 6
.=
(tanh y) + (tanh z)
by SIN_COS2:def 6
;
A5: (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) =
(2 * (sinh . ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2)))
by SIN_COS2:def 2
.=
(2 * (sinh . ((y / 2) - (z / 2)))) * (sinh . ((y / 2) + (z / 2)))
by SIN_COS2:def 2
.=
(cosh . y) - (cosh . z)
by SIN_COS2:27
.=
(cosh y) - (cosh . z)
by SIN_COS2:def 4
.=
(cosh y) - (cosh z)
by SIN_COS2:def 4
;
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) =
(2 * (sinh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))
by SIN_COS2:def 2
.=
(2 * (sinh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2)))
by SIN_COS2:def 4
.=
(sinh . y) + (sinh . z)
by SIN_COS2:26
.=
(sinh y) + (sinh . z)
by SIN_COS2:def 2
.=
(sinh y) + (sinh z)
by SIN_COS2:def 2
;
hence
( (sinh y) + (sinh z) = (2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (sinh y) - (sinh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) & (cosh y) + (cosh z) = (2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) & (cosh y) - (cosh z) = (2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) & (tanh y) + (tanh z) = (sinh (y + z)) / ((cosh y) * (cosh z)) & (tanh y) - (tanh z) = (sinh (y - z)) / ((cosh y) * (cosh z)) )
by A1, A2, A5, A4, A3; verum