let x be real number ; :: thesis: ((cosh . x) ^2 ) - 1 = (sinh . x) ^2
(((cosh . x) ^2 ) - ((sinh . x) ^2 )) + ((sinh . x) ^2 ) = 1 + ((sinh . x) ^2 ) by SIN_COS2:14;
hence ((cosh . x) ^2 ) - 1 = (sinh . x) ^2 ; :: thesis: verum