theorem :: MOEBIUS3:5

for n being Nat
for Z being open Subset of REAL
for A being non empty closed_interval Subset of REAL st Z = right_open_halfline 0 & 0 < n & A = [.n,(n + 1).] holds
integral (((id Z) ^),A) = ln . ((n + 1) / n)