cosh . 1 = (number_e + (exp_R (- 1))) / 2 by IRRAT_1:def 7, SIN_COS2:def 3
.= ((number_e / 1) + (1 / number_e )) / 2 by IRRAT_1:def 7, TAYLOR_1:4
.= (((number_e * number_e ) / (1 * number_e )) + (1 / number_e )) / 2 by TAYLOR_1:11, XCMPLX_1:92
.= (((number_e ^2 ) / number_e ) + (1 / number_e )) / 2
.= (((number_e ^2 ) + 1) / number_e ) / 2 by XCMPLX_1:63
.= ((number_e ^2 ) + 1) / (2 * number_e ) by XCMPLX_1:79 ;
hence cosh . 1 = ((number_e ^2 ) + 1) / (2 * number_e ) ; :: thesis: verum