let y, z be Real; :: thesis: ( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) )
A1: (sinh y) * (cosh z) = (1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))))
.= (1 / 2) * ((sinh (y + z)) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) by Lm10
.= (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) by Lm10 ;
A2: (cosh y) * (sinh z) = (1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))))
.= (1 / 2) * ((sinh (y + z)) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) by Lm10
.= (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) by Lm10 ;
A3: (cosh y) * (cosh z) = (1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))))
.= (1 / 2) * ((cosh (y + z)) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) by Lm10
.= (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) by Lm10 ;
(sinh y) * (sinh z) = (1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))))
.= (1 / 2) * ((cosh (y + z)) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) by Lm10
.= (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) by Lm10 ;
hence ( (sinh y) * (sinh z) = (1 / 2) * ((cosh (y + z)) - (cosh (y - z))) & (sinh y) * (cosh z) = (1 / 2) * ((sinh (y + z)) + (sinh (y - z))) & (cosh y) * (sinh z) = (1 / 2) * ((sinh (y + z)) - (sinh (y - z))) & (cosh y) * (cosh z) = (1 / 2) * ((cosh (y + z)) + (cosh (y - z))) ) by A1, A2, A3; :: thesis: verum