sinh . 1 = (number_e - (exp_R (- 1))) / 2 by IRRAT_1:def 7, SIN_COS2:def 1
.= ((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:91
.= (((number_e ^2) / number_e) - (1 / number_e)) / 2
.= (((number_e ^2) - 1) / number_e) / 2 by XCMPLX_1:120
.= ((number_e ^2) - 1) / (2 * number_e) by XCMPLX_1:78 ;
hence sinh . 1 = ((number_e ^2) - 1) / (2 * number_e) ; :: thesis: verum