let x be Real; :: thesis: ((sech x) ^2) + ((tanh x) ^2) = 1
cosh . x <> 0 by SIN_COS2:15;
then A1: (cosh . x) ^2 <> 0 by SQUARE_1:12;
((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:76
.= ((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:76
.= (1 + ((sinh . x) ^2)) / ((cosh . x) ^2) by XCMPLX_1:62
.= ((((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