let x be Real; :: 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:12;
((coth x) ^2) - ((cosech x) ^2) = (((cosh x) ^2) / ((sinh x) ^2)) - ((1 / (sinh x)) ^2) by XCMPLX_1:76
.= (((cosh x) ^2) / ((sinh x) ^2)) - ((1 ^2) / ((sinh x) ^2)) by XCMPLX_1:76
.= (((cosh x) ^2) - 1) / ((sinh x) ^2) by XCMPLX_1:120
.= (((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