let x be Real; :: thesis: ( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) )
A1: (cosh x) ^2 = (cosh . x) ^2 by SIN_COS2:def 4
.= (1 / 2) * ((cosh . (2 * x)) + 1) by SIN_COS2:18 ;
(sinh x) ^2 = (sinh . x) ^2 by SIN_COS2:def 2
.= (1 / 2) * ((cosh . (2 * x)) - 1) by SIN_COS2:18
.= (1 / 2) * ((cosh (2 * x)) - 1) by SIN_COS2:def 4 ;
hence ( (sinh x) ^2 = (1 / 2) * ((cosh (2 * x)) - 1) & (cosh x) ^2 = (1 / 2) * ((cosh (2 * x)) + 1) ) by A1, SIN_COS2:def 4; :: thesis: verum