let x be real number ; :: thesis: sinh" x = tanh" (x / (sqrt ((x ^2 ) + 1)))
A1: ( (x / (sqrt ((x ^2 ) + 1))) ^2 < 1 & sqrt ((x ^2 ) + 1) > 0 & (sqrt ((x ^2 ) + 1)) + x > 0 & (x ^2 ) + 1 > 0 ) by Lm8, Th3, Th4, Th5;
set t = (sqrt ((x ^2 ) + 1)) + x;
tanh" (x / (sqrt ((x ^2 ) + 1))) = (1 / 2) * (log number_e ,(((((sqrt ((x ^2 ) + 1)) * 1) + x) / (sqrt ((x ^2 ) + 1))) / (1 - (x / (sqrt ((x ^2 ) + 1)))))) by A1, XCMPLX_1:114
.= (1 / 2) * (log number_e ,(((((sqrt ((x ^2 ) + 1)) * 1) + x) / (sqrt ((x ^2 ) + 1))) / (((1 * (sqrt ((x ^2 ) + 1))) - x) / (sqrt ((x ^2 ) + 1))))) by A1, XCMPLX_1:128
.= (1 / 2) * (log number_e ,(((sqrt ((x ^2 ) + 1)) + x) / ((sqrt ((x ^2 ) + 1)) - x))) by A1, XCMPLX_1:55
.= (1 / 2) * (log number_e ,((((sqrt ((x ^2 ) + 1)) + x) * ((sqrt ((x ^2 ) + 1)) + x)) / (((sqrt ((x ^2 ) + 1)) - x) * ((sqrt ((x ^2 ) + 1)) + x)))) by A1, XCMPLX_1:92
.= (1 / 2) * (log number_e ,((((sqrt ((x ^2 ) + 1)) + x) * ((sqrt ((x ^2 ) + 1)) + x)) / (((sqrt ((x ^2 ) + 1)) * (sqrt ((x ^2 ) + 1))) - (x ^2 ))))
.= (1 / 2) * (log number_e ,((((sqrt ((x ^2 ) + 1)) + x) * ((sqrt ((x ^2 ) + 1)) + x)) / ((sqrt (((x ^2 ) + 1) ^2 )) - (x ^2 )))) by A1, SQUARE_1:97
.= (1 / 2) * (log number_e ,((((sqrt ((x ^2 ) + 1)) + x) * ((sqrt ((x ^2 ) + 1)) + x)) / (((x ^2 ) + 1) - (x ^2 )))) by A1, SQUARE_1:89
.= (1 / 2) * (log number_e ,(((sqrt ((x ^2 ) + 1)) + x) ^2 ))
.= (1 / 2) * (log number_e ,(((sqrt ((x ^2 ) + 1)) + x) to_power 2)) by POWER:53
.= (1 / 2) * (2 * (log number_e ,((sqrt ((x ^2 ) + 1)) + x))) by A1, Lm2, POWER:63
.= log number_e ,((sqrt ((x ^2 ) + 1)) + x) ;
hence sinh" x = tanh" (x / (sqrt ((x ^2 ) + 1))) ; :: thesis: verum