let y, z be Real; :: 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