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