let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln) (#) ((id Z) ^) holds
integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A))
let f be PartFunc of REAL,REAL; :: thesis: for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln) (#) ((id Z) ^) holds
integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A))
let Z be open Subset of REAL; :: thesis: ( A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln) (#) ((id Z) ^) implies integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A)) )
assume A1: ( A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (cos * ln) (#) ((id Z) ^) ) ; :: thesis: integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A))
then A2: Z = dom ((cos * ln) / (id Z)) by RFUNCT_1:31;
Z = (dom (cos * ln)) /\ (dom ((id Z) ^)) by A1, VALUED_1:def 4;
then A3: Z c= dom (cos * ln) by XBOOLE_1:18;
for y being object st y in Z holds
y in dom (sin * ln)

proof

let y be object ; :: thesis: ( y in Z implies y in dom (sin * ln) )
assume y in Z ; :: thesis: y in dom (sin * ln)
then ( y in dom ln & ln . y in dom sin ) by A3, FUNCT_1:11, SIN_COS:24;
hence y in dom (sin * ln) by FUNCT_1:11; :: thesis: verum

end;

then A4: Z c= dom (sin * ln) ;
A5: cos * ln is_differentiable_on Z by A3, A1, FDIFF_7:33;
not 0 in Z by A1;
then (id Z) ^ is_differentiable_on Z by FDIFF_5:4;
then f | Z is continuous by A1, A5, FDIFF_1:21, FDIFF_1:25;
then f | A is continuous by A1, FCONT_1:16;
then A6: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A7: sin * ln is_differentiable_on Z by A4, A1, FDIFF_7:32;
A8: for x being Real st x in Z holds
f . x = (cos . (ln . x)) / x

proof

let x be Real; :: thesis: ( x in Z implies f . x = (cos . (ln . x)) / x )
assume A9: x in Z ; :: thesis: f . x = (cos . (ln . x)) / x
((cos * ln) (#) ((id Z) ^)) . x = ((cos * ln) / (id Z)) . x by RFUNCT_1:31
.= ((cos * ln) . x) * (((id Z) . x) ") by A2, A9, RFUNCT_1:def 1
.= ((cos * ln) . x) / x by A9, FUNCT_1:18
.= (cos . (ln . x)) / x by A3, A9, FUNCT_1:12 ;
hence f . x = (cos . (ln . x)) / x by A1; :: thesis: verum

end;

A10: for x being Element of REAL st x in dom ((sin * ln) `| Z) holds
((sin * ln) `| Z) . x = f . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((sin * ln) `| Z) implies ((sin * ln) `| Z) . x = f . x )
assume x in dom ((sin * ln) `| Z) ; :: thesis: ((sin * ln) `| Z) . x = f . x
then A11: x in Z by A7, FDIFF_1:def 7;
then ((sin * ln) `| Z) . x = (cos . (ln . x)) / x by A4, A1, FDIFF_7:32
.= f . x by A11, A8 ;
hence ((sin * ln) `| Z) . x = f . x ; :: thesis: verum

end;

dom ((sin * ln) `| Z) = dom f by A1, A7, FDIFF_1:def 7;
then (sin * ln) `| Z = f by A10, PARTFUN1:5;
hence integral (f,A) = ((sin * ln) . (upper_bound A)) - ((sin * ln) . (lower_bound A)) by A6, A4, A1, FDIFF_7:32, INTEGRA5:13; :: thesis: verum