let A be 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 AA: Z = dom ((cos * ln ) / (id Z)) by RFUNCT_1:47;
Z = (dom (cos * ln )) /\ (dom ((id Z) ^ )) by VALUED_1:def 4, A1;
then A4: Z c= dom (cos * ln ) by XBOOLE_1:18;
for y being set st y in Z holds
y in dom (sin * ln )

proof

let y be set ; :: 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 A4, FUNCT_1:21, SIN_COS:27;
hence y in dom (sin * ln ) by FUNCT_1:21; :: thesis: verum

end;

then B6: Z c= dom (sin * ln ) by TARSKI:def 3;
A6: cos * ln is_differentiable_on Z by FDIFF_7:33, A4, A1;
not 0 in Z by A1;
then (id Z) ^ is_differentiable_on Z by FDIFF_5:4;
then f | Z is continuous by FDIFF_1:33, A1, A6, FDIFF_1:29;
then f | A is continuous by A1, FCONT_1:17;
then A11: ( f is_integrable_on A & f | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11;
A12: sin * ln is_differentiable_on Z by B6, A1, FDIFF_7:32;
B1: 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 B2: x in Z ; :: thesis: f . x = (cos . (ln . x)) / x
((cos * ln ) (#) ((id Z) ^ )) . x = ((cos * ln ) / (id Z)) . x by RFUNCT_1:47
.= ((cos * ln ) . x) * (((id Z) . x) " ) by RFUNCT_1:def 4, AA, B2
.= ((cos * ln ) . x) / x by FUNCT_1:35, B2
.= (cos . (ln . x)) / x by FUNCT_1:22, A4, B2 ;
hence f . x = (cos . (ln . x)) / x by A1; :: thesis: verum

end;

A13: for x being Real st x in dom ((sin * ln ) `| Z) holds
((sin * ln ) `| Z) . x = f . x

proof

let x be 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 A14: x in Z by A12, FDIFF_1:def 8;
then ((sin * ln ) `| Z) . x = (cos . (ln . x)) / x by B6, A1, FDIFF_7:32
.= f . x by A14, B1 ;
hence ((sin * ln ) `| Z) . x = f . x ; :: thesis: verum

end;

dom ((sin * ln ) `| Z) = dom f by A1, A12, FDIFF_1:def 8;
then (sin * ln ) `| Z = f by A13, PARTFUN1:34;
hence integral f,A = ((sin * ln ) . (upper_bound A)) - ((sin * ln ) . (lower_bound A)) by A11, B6, A1, FDIFF_7:32, INTEGRA5:13; :: thesis: verum