let x be real number ; :: thesis: (cosh . x) ^2 = 1 + ((sinh . x) ^2 )
cosh . (2 * x) = cosh . (x + x)
.= ((cosh . x) ^2 ) + ((sinh . x) ^2 ) by SIN_COS2:20 ;
then (1 + (2 * ((sinh . x) ^2 ))) - ((sinh . x) ^2 ) = (((cosh . x) ^2 ) + ((sinh . x) ^2 )) - ((sinh . x) ^2 ) by Th69;
hence (cosh . x) ^2 = 1 + ((sinh . x) ^2 ) ; :: thesis: verum