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