theorem :: SIN_COS7:60

for x being Real st 1 < x holds
log (number_e,x) = cosh1" (((x ^2) + 1) / (2 * x))