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