let x be real number ; :: thesis: ( sinh x <> 0 implies ((coth x) ^2 ) - ((cosech x) ^2 ) = 1 )
assume sinh x <> 0 ; :: thesis: ((coth x) ^2 ) - ((cosech x) ^2 ) = 1
then A1: (sinh x) ^2 <> 0 by SQUARE_1:74;
((coth x) ^2 ) - ((cosech x) ^2 ) = (((cosh x) ^2 ) / ((sinh x) ^2 )) - ((1 / (sinh x)) ^2 ) by XCMPLX_1:77
.= (((cosh x) ^2 ) / ((sinh x) ^2 )) - ((1 ^2 ) / ((sinh x) ^2 )) by XCMPLX_1:77
.= (((cosh x) ^2 ) - 1) / ((sinh x) ^2 ) by XCMPLX_1:121
.= (((cosh x) ^2 ) - (((cosh . x) ^2 ) - ((sinh . x) ^2 ))) / ((sinh x) ^2 ) by SIN_COS2:14
.= ((((cosh x) ^2 ) - ((cosh . x) ^2 )) + ((sinh . x) ^2 )) / ((sinh x) ^2 )
.= ((((cosh x) ^2 ) - ((cosh x) ^2 )) + ((sinh . x) ^2 )) / ((sinh x) ^2 ) by SIN_COS2:def 4
.= (0 + ((sinh x) ^2 )) / ((sinh x) ^2 ) by SIN_COS2:def 2 ;
hence ((coth x) ^2 ) - ((cosech x) ^2 ) = 1 by A1, XCMPLX_1:60; :: thesis: verum