theorem LogExp: :: MOEBIUS3:16

for x being Real holds ln . (exp_R . x) = x