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