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 = (sin * ln ) (#) ((id Z) ^ ) holds
integral f,A = ((- (cos * ln )) . (upper_bound A)) - ((- (cos * 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 = (sin * ln ) (#) ((id Z) ^ ) holds
integral f,A = ((- (cos * ln )) . (upper_bound A)) - ((- (cos * 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 = (sin * ln ) (#) ((id Z) ^ ) implies integral f,A = ((- (cos * ln )) . (upper_bound A)) - ((- (cos * ln )) . (lower_bound A)) )
assume A1: ( A c= Z & ( for x being Real st x in Z holds
x > 0 ) & Z = dom f & f = (sin * ln ) (#) ((id Z) ^ ) ) ; :: thesis: integral f,A = ((- (cos * ln )) . (upper_bound A)) - ((- (cos * ln )) . (lower_bound A))
then AA: Z = dom ((sin * ln ) / (id Z)) by RFUNCT_1:47;
Z = (dom (sin * ln )) /\ (dom ((id Z) ^ )) by VALUED_1:def 4, A1;
then A4: Z c= dom (sin * ln ) by XBOOLE_1:18;
for y being set st y in Z holds
y in dom (cos * ln )

proof

let y be set ; :: thesis: ( y in Z implies y in dom (cos * ln ) )
assume y in Z ; :: thesis: y in dom (cos * ln )
then ( y in dom ln & ln . y in dom cos ) by A4, FUNCT_1:21, SIN_COS:27;
hence y in dom (cos * ln ) by FUNCT_1:21; :: thesis: verum

end;

then B6: Z c= dom (cos * ln ) by TARSKI:def 3;
A6: sin * ln is_differentiable_on Z by FDIFF_7:32, 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: cos * ln is_differentiable_on Z by B6, A1, FDIFF_7:33;
A13: Z c= dom (- (cos * ln )) by B6, VALUED_1:8;
then A14: (- 1) (#) (cos * ln ) is_differentiable_on Z by A12, FDIFF_1:28, X;
A15: for x being Real st x in Z holds
((- (cos * ln )) `| Z) . x = (sin . (ln . x)) / x

proof

let x be Real; :: thesis: ( x in Z implies ((- (cos * ln )) `| Z) . x = (sin . (ln . x)) / x )
assume A16: x in Z ; :: thesis: ((- (cos * ln )) `| Z) . x = (sin . (ln . x)) / x
then x > 0 by A1;
then A18: x in right_open_halfline 0 by Lm1;
A19: ln is_differentiable_in x by A16, A1, TAYLOR_1:18;
A20: cos is_differentiable_in ln . x by SIN_COS:68;
A21: cos * ln is_differentiable_in x by A12, A16, FDIFF_1:16;
((- (cos * ln )) `| Z) . x = diff (- (cos * ln )),x by A14, A16, FDIFF_1:def 8
.= (- 1) * (diff (cos * ln ),x) by A21, FDIFF_1:23, X
.= (- 1) * ((diff cos ,(ln . x)) * (diff ln ,x)) by A19, A20, FDIFF_2:13
.= (- 1) * ((- (sin . (ln . x))) * (diff ln ,x)) by SIN_COS:68
.= (- 1) * ((- (sin . (ln . x))) * (1 / x)) by A18, TAYLOR_1:18
.= (sin . (ln . x)) / x ;
hence ((- (cos * ln )) `| Z) . x = (sin . (ln . x)) / x ; :: thesis: verum

end;

B7: for x being Real st x in Z holds
f . x = (sin . (ln . x)) / x

proof

let x be Real; :: thesis: ( x in Z implies f . x = (sin . (ln . x)) / x )
assume B8: x in Z ; :: thesis: f . x = (sin . (ln . x)) / x
((sin * ln ) (#) ((id Z) ^ )) . x = ((sin * ln ) / (id Z)) . x by RFUNCT_1:47
.= ((sin * ln ) . x) * (((id Z) . x) " ) by RFUNCT_1:def 4, AA, B8
.= ((sin * ln ) . x) / x by FUNCT_1:35, B8
.= (sin . (ln . x)) / x by FUNCT_1:22, A4, B8 ;
hence f . x = (sin . (ln . x)) / x by A1; :: thesis: verum

end;

A22: for x being Real st x in dom ((- (cos * ln )) `| Z) holds
((- (cos * ln )) `| Z) . x = f . x

proof

let x be Real; :: thesis: ( x in dom ((- (cos * ln )) `| Z) implies ((- (cos * ln )) `| Z) . x = f . x )
assume x in dom ((- (cos * ln )) `| Z) ; :: thesis: ((- (cos * ln )) `| Z) . x = f . x
then A23: x in Z by A14, FDIFF_1:def 8;
then ((- (cos * ln )) `| Z) . x = (sin . (ln . x)) / x by A15
.= f . x by A23, B7 ;
hence ((- (cos * ln )) `| Z) . x = f . x ; :: thesis: verum

end;

dom ((- (cos * ln )) `| Z) = dom f by A1, A14, FDIFF_1:def 8;
then (- (cos * ln )) `| Z = f by A22, PARTFUN1:34;
hence integral f,A = ((- (cos * ln )) . (upper_bound A)) - ((- (cos * ln )) . (lower_bound A)) by A1, A11, A12, A13, FDIFF_1:28, X, INTEGRA5:13; :: thesis: verum