let x be Real; :: 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:22 ;
cosh x <> 0 by Lm1;
then sinh x = ((sinh x) / (cosh x)) * (cosh x) by XCMPLX_1:87
.= (tanh x) * (1 / (sqrt (1 - ((tanh x) ^2)))) by A3, Th1
.= (tanh x) / (sqrt (1 - ((tanh x) ^2))) by XCMPLX_1:99 ;
hence ( cosh x = 1 / (sqrt (1 - ((tanh x) ^2))) & sinh x = (tanh x) / (sqrt (1 - ((tanh x) ^2))) ) by A3; :: thesis: verum