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 = (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 A2: Z = dom ((sin * ln) / (id Z)) by RFUNCT_1:31;
Z = (dom (sin * ln)) /\ (dom ((id Z) ^)) by A1, VALUED_1:def 4;
then A3: Z c= dom (sin * ln) by XBOOLE_1:18;
for y being object st y in Z holds
y in dom (cos * ln)

proof

let y be object ; :: 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 A3, FUNCT_1:11, SIN_COS:24;
hence y in dom (cos * ln) by FUNCT_1:11; :: thesis: verum

end;

then A4: Z c= dom (cos * ln) ;
A5: sin * ln is_differentiable_on Z by A3, A1, FDIFF_7:32;
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: cos * ln is_differentiable_on Z by A4, A1, FDIFF_7:33;
A8: Z c= dom (- (cos * ln)) by A4, VALUED_1:8;
then A9: (- 1) (#) (cos * ln) is_differentiable_on Z by A7, FDIFF_1:20;
A10: 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 A11: x in Z ; :: thesis: ((- (cos * ln)) `| Z) . x = (sin . (ln . x)) / x
then x > 0 by A1;
then A12: x in right_open_halfline 0 by Lm1;
A13: ln is_differentiable_in x by A11, A1, TAYLOR_1:18;
A14: cos is_differentiable_in ln . x by SIN_COS:63;
A15: cos * ln is_differentiable_in x by A7, A11, FDIFF_1:9;
((- (cos * ln)) `| Z) . x = diff ((- (cos * ln)),x) by A9, A11, FDIFF_1:def 7
.= (- 1) * (diff ((cos * ln),x)) by A15, FDIFF_1:15
.= (- 1) * ((diff (cos,(ln . x))) * (diff (ln,x))) by A13, A14, FDIFF_2:13
.= (- 1) * ((- (sin . (ln . x))) * (diff (ln,x))) by SIN_COS:63
.= (- 1) * ((- (sin . (ln . x))) * (1 / x)) by A12, TAYLOR_1:18
.= (sin . (ln . x)) / x ;
hence ((- (cos * ln)) `| Z) . x = (sin . (ln . x)) / x ; :: thesis: verum

end;

A16: 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 A17: x in Z ; :: thesis: f . x = (sin . (ln . x)) / x
((sin * ln) (#) ((id Z) ^)) . x = ((sin * ln) / (id Z)) . x by RFUNCT_1:31
.= ((sin * ln) . x) * (((id Z) . x) ") by A2, A17, RFUNCT_1:def 1
.= ((sin * ln) . x) / x by A17, FUNCT_1:18
.= (sin . (ln . x)) / x by A3, A17, FUNCT_1:12 ;
hence f . x = (sin . (ln . x)) / x by A1; :: thesis: verum

end;

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

proof

let x be Element of 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 A19: x in Z by A9, FDIFF_1:def 7;
then ((- (cos * ln)) `| Z) . x = (sin . (ln . x)) / x by A10
.= f . x by A19, A16 ;
hence ((- (cos * ln)) `| Z) . x = f . x ; :: thesis: verum

end;

dom ((- (cos * ln)) `| Z) = dom f by A1, A9, FDIFF_1:def 7;
then (- (cos * ln)) `| Z = f by A18, PARTFUN1:5;
hence integral (f,A) = ((- (cos * ln)) . (upper_bound A)) - ((- (cos * ln)) . (lower_bound A)) by A1, A6, A7, A8, FDIFF_1:20, INTEGRA5:13; :: thesis: verum