let n be Nat; :: thesis: 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)
let Z be open Subset of REAL; :: thesis: 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)
let A be non empty closed_interval Subset of REAL; :: thesis: ( Z = right_open_halfline 0 & A = [.1,(n + 1).] implies integral (((id Z) ^),A) = ln . (n + 1) )
assume Z1: ( Z = right_open_halfline 0 & A = [.1,(n + 1).] ) ; :: thesis: integral (((id Z) ^),A) = ln . (n + 1)
then N1: not 0 in Z by XXREAL_1:4;
A1: A c= Z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Z )
assume aa: x in A ; :: thesis: x in Z
then reconsider xx = x as Real ;
( 1 <= xx & xx <= n + 1 ) by aa, Z1, XXREAL_1:1;
hence x in Z by Z1, XXREAL_1:235; :: thesis: verum

end;

set f = id Z;
a3: dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def 2
.= Z \ {} by Counter0, N1
.= Z ;
B1: lower_bound A = 1 by Z1, XREAL_1:31, XXREAL_2:25;
B2: upper_bound A = n + 1 by Z1, XREAL_1:31, XXREAL_2:29;
((id Z) ^) | A is continuous by ContCut, A1, N1;
then integral (((id Z) ^),A) = (ln . (upper_bound A)) - (ln . (lower_bound A)) by A1, Z1, TAYLOR_1:18, a3, INTEGRA9:61
.= (ln . (n + 1)) - (1 - 1) by ENTROPY1:2, B1, B2
.= ln . (n + 1) ;
hence integral (((id Z) ^),A) = ln . (n + 1) ; :: thesis: verum