let x, y be Real; :: 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:55;
set t = exp_R x;
assume that
A2: y = 1 / (((exp_R x) - (exp_R (- x))) / 2) and
A3: x <> 0 ; :: thesis: ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) )
A4: delta (y,(- 2),(- y)) = ((- 2) ^2) - ((4 * y) * (- y)) by QUIN_1:def 1
.= 4 + (4 * (y ^2)) ;
y = (1 * 2) / (2 * (((exp_R x) - (exp_R (- x))) / 2)) by A2, XCMPLX_1:91;
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:127;
then A5: y = 2 * ((exp_R x) / (((exp_R x) ^2) - 1)) by XCMPLX_1:79;
then A6: y = (2 * (exp_R x)) / (((exp_R x) ^2) - 1) ;
then y * (((exp_R x) ^2) - 1) = 2 * (exp_R x) by A3, Th30, XCMPLX_1:87;
then A7: ((y * ((exp_R x) ^2)) + ((- 2) * (exp_R x))) + (- y) = 0 ;
A8: exp_R x <> 1 by A3, Th29;
then A9: (2 * (exp_R x)) / (((exp_R x) ^2) - 1) <> 0 by Lm20, SIN_COS:55;

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

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

A11: 0 < 1 + (y ^2) by Lm6;
then 0 * 4 < 4 * (1 + (y ^2)) ;
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, A8, A6, A7, A4, Lm20, 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 A4, A11, SQUARE_1:29;
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:20, SQUARE_1:29;
then A12: ( exp_R x = (1 + (sqrt (1 + (y ^2)))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2))))) / (2 * y) ) by XCMPLX_1:91;
(1 - (sqrt (1 + (y ^2)))) / y < 0 by A10, Lm15;
hence ( x = log (number_e,((1 + (sqrt (1 + (y ^2)))) / y)) or x = log (number_e,((1 - (sqrt (1 + (y ^2)))) / y)) ) by A1, A12, TAYLOR_1:12, XCMPLX_1:91; :: thesis: verum

end;

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

A14: 0 < 1 + (y ^2) by Lm6;
then 0 * 4 < 4 * (1 + (y ^2)) ;
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, A8, A6, A7, A4, Lm20, 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 A4, A14, SQUARE_1:29;
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 A14, SQUARE_1:20, SQUARE_1:29;
then A15: ( exp_R x = (1 + (sqrt (1 + (y ^2)))) / y or exp_R x = (2 * (1 - (sqrt (1 + (y ^2))))) / (2 * y) ) by XCMPLX_1:91;
(1 + (sqrt (1 + (y ^2)))) / y < 0 by A13, Lm21;
then exp_R x = (1 - (sqrt (1 + (y ^2)))) / y by A15, SIN_COS:55, XCMPLX_1:91;
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;