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