let y, x be real number ; :: thesis: ( y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 & not x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) implies x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) )
A1: 0 < exp_R x by SIN_COS:60;
assume A2: ( y = 1 / (((exp_R x) - (exp_R (- x))) / 2) & x <> 0 ) ; :: thesis: ( x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) or x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) )
then A3: exp_R x <> 1 by Th29;
then A4: (2 * (exp_R x)) / (((exp_R x) ^2 ) - 1) <> 0 by Lm23, SIN_COS:60;
y = (1 * 2) / (2 * (((exp_R x) - (exp_R (- x))) / 2)) by A2, XCMPLX_1:92;
then y = 2 / ((exp_R x) - (1 / (exp_R x))) by TAYLOR_1:4;
then y = 2 / ((((exp_R x) * (exp_R x)) - 1) / (exp_R x)) by A1, XCMPLX_1:128;
then y = 2 * ((exp_R x) / (((exp_R x) ^2 ) - 1)) by XCMPLX_1:80;
then A5: y = (2 * (exp_R x)) / (((exp_R x) ^2 ) - 1) ;
set t = exp_R x;
y * (((exp_R x) ^2 ) - 1) = 2 * (exp_R x) by A2, A5, Th30, XCMPLX_1:88;
then A6: ((y * ((exp_R x) ^2 )) + ((- 2) * (exp_R x))) + (- y) = 0 ;
A7: delta y,(- 2),(- y) = ((- 2) ^2 ) - ((4 * y) * (- y)) by QUIN_1:def 1
.= 4 + (4 * (y ^2 )) ;

per cases ( 0 < y or y < 0 ) by A4, A5;

suppose 0 < y ; :: thesis: ( x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) or x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) )

then A8: ( (1 - (sqrt (1 + (y ^2 )))) / y < 0 & 0 < (1 + (sqrt (1 + (y ^2 )))) / y ) by Lm17, Lm18;
A9: 0 < 1 + (y ^2 ) by Lm8;
then 0 * 4 < 4 * (1 + (y ^2 )) by XREAL_1:70;
then ( exp_R x = (2 + (sqrt (delta y,(- 2),(- y)))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta y,(- 2),(- y)))) / (2 * y) ) by A1, A3, A5, A6, A7, Lm23, QUIN_1:15;
then ( exp_R x = (2 + ((sqrt 4) * (sqrt (1 + (y ^2 ))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 + (y ^2 ))))) / (2 * y) ) by A7, A9, SQUARE_1:97;
then ( exp_R x = (2 * (1 + (sqrt (1 + (y ^2 ))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 + (y ^2 ))))) / (2 * y) ) by A9, SQUARE_1:85, SQUARE_1:97;
then ( exp_R x = (1 + (sqrt (1 + (y ^2 )))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2 ))))) / (2 * y) ) by XCMPLX_1:92;
hence ( x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) or x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) ) by A1, A8, TAYLOR_1:12, XCMPLX_1:92; :: thesis: verum

end;

suppose y < 0 ; :: thesis: ( x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) or x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) )

then A10: ( 0 < (1 - (sqrt (1 + (y ^2 )))) / y & (1 + (sqrt (1 + (y ^2 )))) / y < 0 ) by Lm24, Lm25;
A11: 0 < 1 + (y ^2 ) by Lm8;
then 0 * 4 < 4 * (1 + (y ^2 )) by XREAL_1:70;
then ( exp_R x = (2 + (sqrt (delta y,(- 2),(- y)))) / (2 * y) or exp_R x = ((- (- 2)) - (sqrt (delta y,(- 2),(- y)))) / (2 * y) ) by A1, A3, A5, A6, A7, Lm23, QUIN_1:15;
then ( exp_R x = (2 + ((sqrt 4) * (sqrt (1 + (y ^2 ))))) / (2 * y) or exp_R x = (2 - (sqrt (4 * (1 + (y ^2 ))))) / (2 * y) ) by A7, A11, SQUARE_1:97;
then ( exp_R x = (2 * (1 + (sqrt (1 + (y ^2 ))))) / (2 * y) or exp_R x = (2 - (2 * (sqrt (1 + (y ^2 ))))) / (2 * y) ) by A11, SQUARE_1:85, SQUARE_1:97;
then ( exp_R x = (1 + (sqrt (1 + (y ^2 )))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2 ))))) / (2 * y) ) by XCMPLX_1:92;
then exp_R x = (1 - (sqrt (1 + (y ^2 )))) / y by A10, SIN_COS:60, XCMPLX_1:92;
hence ( x = log number_e ,((1 + (sqrt (1 + (y ^2 )))) / y) or x = log number_e ,((1 - (sqrt (1 + (y ^2 )))) / y) ) by TAYLOR_1:12; :: thesis: verum

end;

end;