theorem LogAdd: :: MOEBIUS3:19

for x, y being Real st 0 < x & 0 < y holds
ln . (x * y) = (ln . x) + (ln . y)