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