let y, z be real number ; :: thesis: ((sinh y) ^2 ) - ((cosh z) ^2 ) = ((sinh (y + z)) * (sinh (y - z))) - 1
((sinh y) ^2 ) - ((cosh z) ^2 ) = ((sinh y) ^2 ) - (((cosh z) ^2 ) * 1)
.= ((sinh y) ^2 ) - (((cosh z) ^2 ) * (((cosh y) ^2 ) - ((sinh y) ^2 ))) by Lm3
.= ((sinh y) ^2 ) + ((((cosh z) ^2 ) * ((sinh y) ^2 )) - (((cosh y) ^2 ) * ((((cosh z) ^2 ) - ((sinh z) ^2 )) + ((sinh z) ^2 ))))
.= ((sinh y) ^2 ) + ((((cosh z) ^2 ) * ((sinh y) ^2 )) - (((cosh y) ^2 ) * (1 + ((sinh z) ^2 )))) by Lm3
.= ((sinh y) ^2 ) + (((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2 ))
.= ((sinh y) ^2 ) + (((sinh (y + z)) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2 )) by Lm10
.= (((sinh (y + z)) * (sinh (y - z))) - ((cosh y) ^2 )) + ((sinh y) ^2 ) by Lm10
.= ((sinh (y + z)) * (sinh (y - z))) - (((cosh y) ^2 ) - ((sinh y) ^2 ))
.= ((sinh (y + z)) * (sinh (y - z))) - 1 by Lm3 ;
hence ((sinh y) ^2 ) - ((cosh z) ^2 ) = ((sinh (y + z)) * (sinh (y - z))) - 1 ; :: thesis: verum