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:92
.= (((number_e ^2 ) / number_e ) - (1 / number_e )) / 2
.= (((number_e ^2 ) - 1) / number_e ) / 2 by XCMPLX_1:121
.= ((number_e ^2 ) - 1) / (2 * number_e ) by XCMPLX_1:79 ;
hence sinh . 1 = ((number_e ^2 ) - 1) / (2 * number_e ) ; :: thesis: verum