let x be real number ; :: 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