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