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