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 & A = [.1,(n + 1).] holds
integral (((id Z) ^),A) = ln . (n + 1)