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