let x be Real; :: thesis: ( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) )
A1: sinh x = 1 / (1 / (sinh x)) by XCMPLX_1:56
.= 1 / (cosech x) by SIN_COS5:def 3 ;
A2: cosh x = 1 / (1 / (cosh x)) by XCMPLX_1:56
.= 1 / (sech x) by SIN_COS5:def 2 ;
tanh x = (sinh x) / (cosh x) by Th1
.= 1 / ((cosh x) / (sinh x)) by XCMPLX_1:57
.= 1 / (coth x) by SIN_COS5:def 1 ;
hence ( sinh x = 1 / (cosech x) & cosh x = 1 / (sech x) & tanh x = 1 / (coth x) ) by A1, A2; :: thesis: verum