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