let x be real number ; :: thesis: ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2 ))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2 ))) )
A1: (sech x) ^2 = (((sech x) ^2 ) + ((tanh x) ^2 )) - ((tanh x) ^2 )
.= 1 - ((tanh x) ^2 ) by SIN_COS5:38 ;
A2: sech x > 0 by Th3;
A3: cosh x = 1 / (1 / (cosh x)) by XCMPLX_1:56
.= 1 / (sech x) by SIN_COS5:def 2
.= 1 / (sqrt (1 - ((tanh x) ^2 ))) by A1, A2, SQUARE_1:89 ;
cosh x <> 0 by Lm1;
then sinh x = ((sinh x) / (cosh x)) * (cosh x) by XCMPLX_1:88
.= (tanh x) * (1 / (sqrt (1 - ((tanh x) ^2 )))) by A3, Th1
.= (tanh x) / (sqrt (1 - ((tanh x) ^2 ))) by XCMPLX_1:100 ;
hence ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2 ))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2 ))) ) by A3; :: thesis: verum