let y, z be real number ; :: thesis: ( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2 ) - ((sin z) ^2 ))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2 ) + ((sin z) ^2 )) )
A1: (cosh (2 * y)) + (cos (2 * z)) = (1 + (2 * ((sinh y) ^2 ))) + (cos (2 * z)) by Th27
.= (1 + (2 * ((sinh y) ^2 ))) + (1 - (2 * ((sin z) ^2 ))) by SIN_COS5:7
.= 2 + (2 * (((sinh y) ^2 ) - ((sin z) ^2 ))) ;
(cosh (2 * y)) - (cos (2 * z)) = (1 + (2 * ((sinh y) ^2 ))) - (cos (2 * z)) by Th27
.= (1 + (2 * ((sinh y) ^2 ))) - (1 - (2 * ((sin z) ^2 ))) by SIN_COS5:7
.= 2 * (((sinh y) ^2 ) + ((sin z) ^2 )) ;
hence ( (cosh (2 * y)) + (cos (2 * z)) = 2 + (2 * (((sinh y) ^2 ) - ((sin z) ^2 ))) & (cosh (2 * y)) - (cos (2 * z)) = 2 * (((sinh y) ^2 ) + ((sin z) ^2 )) ) by A1; :: thesis: verum