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

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