theorem :: SIN_COS7:62

for x being Real st 0 < x holds
log (number_e,x) = sinh" (((x ^2) - 1) / (2 * x))