theorem :: SIN_COS7:61

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