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