let A be closed-interval Subset of REAL ; :: thesis: for Z being open Subset of REAL st A c= Z holds
integral ((id Z) (#) sin ),A = ((((- (id Z)) (#) cos ) + sin ) . (upper_bound A)) - ((((- (id Z)) (#) cos ) + sin ) . (lower_bound A))
let Z be open Subset of REAL ; :: thesis: ( A c= Z implies integral ((id Z) (#) sin ),A = ((((- (id Z)) (#) cos ) + sin ) . (upper_bound A)) - ((((- (id Z)) (#) cos ) + sin ) . (lower_bound A)) )
assume A1: A c= Z ; :: thesis: integral ((id Z) (#) sin ),A = ((((- (id Z)) (#) cos ) + sin ) . (upper_bound A)) - ((((- (id Z)) (#) cos ) + sin ) . (lower_bound A))
D1: dom (((- (id Z)) (#) cos ) + sin ) = Z

proof

A2: dom (- (id Z)) = dom (id Z) by VALUED_1:8;
dom (((- (id Z)) (#) cos ) + sin ) = (dom ((- (id Z)) (#) cos )) /\ REAL by SIN_COS:27, VALUED_1:def 1
.= dom ((- (id Z)) (#) cos ) by XBOOLE_1:28
.= (dom (- (id Z))) /\ REAL by SIN_COS:27, VALUED_1:def 4
.= dom (- (id Z)) by XBOOLE_1:28
.= Z by A2, RELAT_1:71 ;
hence dom (((- (id Z)) (#) cos ) + sin ) = Z ; :: thesis: verum

end;

D2: Z = dom ((id Z) (#) sin )

proof

dom ((id Z) (#) sin ) = (dom (id Z)) /\ REAL by SIN_COS:27, VALUED_1:def 4
.= dom (id Z) by XBOOLE_1:28
.= Z by RELAT_1:71 ;
hence Z = dom ((id Z) (#) sin ) ; :: thesis: verum

end;

((id Z) (#) sin ) | Z is continuous by D2, FDIFF_1:33, FDIFF_4:45;
then ((id Z) (#) sin ) | A is continuous by A1, FCONT_1:17;
then A3: ( (id Z) (#) sin is_integrable_on A & ((id Z) (#) sin ) | A is bounded ) by A1, D2, INTEGRA5:10, INTEGRA5:11;
A4: ((- (id Z)) (#) cos ) + sin is_differentiable_on Z by D1, FDIFF_4:46;
B: for x being Real st x in Z holds
((id Z) (#) sin ) . x = x * (sin . x)

proof

let x be Real; :: thesis: ( x in Z implies ((id Z) (#) sin ) . x = x * (sin . x) )
assume C: x in Z ; :: thesis: ((id Z) (#) sin ) . x = x * (sin . x)
((id Z) (#) sin ) . x = ((id Z) . x) * (sin . x) by VALUED_1:5
.= x * (sin . x) by C, FUNCT_1:35 ;
hence ((id Z) (#) sin ) . x = x * (sin . x) ; :: thesis: verum

end;

A5: for x being Real st x in dom ((((- (id Z)) (#) cos ) + sin ) `| Z) holds
((((- (id Z)) (#) cos ) + sin ) `| Z) . x = ((id Z) (#) sin ) . x

proof

let x be Real; :: thesis: ( x in dom ((((- (id Z)) (#) cos ) + sin ) `| Z) implies ((((- (id Z)) (#) cos ) + sin ) `| Z) . x = ((id Z) (#) sin ) . x )
assume x in dom ((((- (id Z)) (#) cos ) + sin ) `| Z) ; :: thesis: ((((- (id Z)) (#) cos ) + sin ) `| Z) . x = ((id Z) (#) sin ) . x
then A6: x in Z by A4, FDIFF_1:def 8;
then ((((- (id Z)) (#) cos ) + sin ) `| Z) . x = x * (sin . x) by D1, FDIFF_4:46
.= ((id Z) (#) sin ) . x by B, A6 ;
hence ((((- (id Z)) (#) cos ) + sin ) `| Z) . x = ((id Z) (#) sin ) . x ; :: thesis: verum

end;

dom ((((- (id Z)) (#) cos ) + sin ) `| Z) = dom ((id Z) (#) sin ) by D2, A4, FDIFF_1:def 8;
then (((- (id Z)) (#) cos ) + sin ) `| Z = (id Z) (#) sin by A5, PARTFUN1:34;
hence integral ((id Z) (#) sin ),A = ((((- (id Z)) (#) cos ) + sin ) . (upper_bound A)) - ((((- (id Z)) (#) cos ) + sin ) . (lower_bound A)) by A1, D1, A3, FDIFF_4:46, INTEGRA5:13; :: thesis: verum