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

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