let x be real number ; :: thesis: ((sech x) ^2 ) + ((tanh x) ^2 ) = 1
cosh . x <> 0 by SIN_COS2:15;
then A1: (cosh . x) ^2 <> 0 by SQUARE_1:74;
((sech x) ^2 ) + ((tanh x) ^2 ) = ((1 / (cosh x)) ^2 ) + ((tanh . x) ^2 ) by SIN_COS2:def 6
.= ((1 / (cosh . x)) ^2 ) + ((tanh . x) ^2 ) by SIN_COS2:def 4
.= ((1 ^2 ) / ((cosh . x) ^2 )) + ((tanh . x) ^2 ) by XCMPLX_1:77
.= ((1 ^2 ) / ((cosh . x) ^2 )) + (((sinh . x) / (cosh . x)) ^2 ) by SIN_COS2:17
.= (1 / ((cosh . x) ^2 )) + (((sinh . x) ^2 ) / ((cosh . x) ^2 )) by XCMPLX_1:77
.= (1 + ((sinh . x) ^2 )) / ((cosh . x) ^2 ) by XCMPLX_1:63
.= ((((cosh . x) ^2 ) - ((sinh . x) ^2 )) + ((sinh . x) ^2 )) / ((cosh . x) ^2 ) by SIN_COS2:14
.= ((cosh . x) ^2 ) / ((cosh . x) ^2 ) ;
hence ((sech x) ^2 ) + ((tanh x) ^2 ) = 1 by A1, XCMPLX_1:60; :: thesis: verum