let x be Real; :: thesis: ( x < 0 implies sinh" x = cosh2" (sqrt ((x ^2) + 1)) )
assume A1: x < 0 ; :: thesis: sinh" x = cosh2" (sqrt ((x ^2) + 1))
A2: (sqrt ((x ^2) + 1)) + x > 0 by Th5;
A3: 1 / ((sqrt ((x ^2) + 1)) + x) = ((sqrt ((x ^2) + 1)) + x) to_power (- 1) by Th1, Th5;
A4: x ^2 >= 0 by XREAL_1:63;
then cosh2" (sqrt ((x ^2) + 1)) = - (log (number_e,((sqrt ((x ^2) + 1)) + (sqrt (((x ^2) + 1) - 1))))) by SQUARE_1:def 2
.= - (log (number_e,((sqrt ((x ^2) + 1)) + (- x)))) by A1, SQUARE_1:23
.= - (log (number_e,((((sqrt ((x ^2) + 1)) - x) * ((sqrt ((x ^2) + 1)) + x)) / ((sqrt ((x ^2) + 1)) + x)))) by A2, XCMPLX_1:89
.= - (log (number_e,((((sqrt ((x ^2) + 1)) ^2) - (x ^2)) / ((sqrt ((x ^2) + 1)) + x))))
.= - (log (number_e,((((x ^2) + 1) - (x ^2)) / ((sqrt ((x ^2) + 1)) + x)))) by A4, SQUARE_1:def 2
.= - ((- 1) * (log (number_e,((sqrt ((x ^2) + 1)) + x)))) by A2, A3, Lm1, POWER:55, TAYLOR_1:11
.= log (number_e,((sqrt ((x ^2) + 1)) + x)) ;
hence sinh" x = cosh2" (sqrt ((x ^2) + 1)) ; :: thesis: verum