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