let A be closed-interval Subset of REAL ; :: thesis: integral (exp_R (#) (cos - sin )),A = ((exp_R (#) cos ) . (upper_bound A)) - ((exp_R (#) cos ) . (lower_bound A))
A1: dom (exp_R (#) cos ) = REAL by FUNCT_2:def 1;
A2: dom (cos - sin ) = REAL by FUNCT_2:def 1;
A3: dom (exp_R (#) (cos - sin )) = (dom exp_R ) /\ (dom (cos - sin )) by VALUED_1:def 4
.= REAL /\ (dom (cos - sin )) by SIN_COS:51
.= REAL by A2 ;
A4: ( exp_R (#) (cos - sin ) is_integrable_on A & (exp_R (#) (cos - sin )) | A is bounded ) by Lm20;
A5: [#] REAL is open Subset of REAL ;
then A6: exp_R (#) cos is_differentiable_on REAL by A1, FDIFF_7:45;
A7: for x being Real st x in dom ((exp_R (#) cos ) `| REAL ) holds
((exp_R (#) cos ) `| REAL ) . x = (exp_R (#) (cos - sin )) . x

proof

let x be Real; :: thesis: ( x in dom ((exp_R (#) cos ) `| REAL ) implies ((exp_R (#) cos ) `| REAL ) . x = (exp_R (#) (cos - sin )) . x )
assume x in dom ((exp_R (#) cos ) `| REAL ) ; :: thesis: ((exp_R (#) cos ) `| REAL ) . x = (exp_R (#) (cos - sin )) . x
(exp_R (#) (cos - sin )) . x = (exp_R . x) * ((cos - sin ) . x) by VALUED_1:5
.= (exp_R . x) * ((cos . x) - (sin . x)) by A2, VALUED_1:13 ;
hence ((exp_R (#) cos ) `| REAL ) . x = (exp_R (#) (cos - sin )) . x by A1, A5, FDIFF_7:45; :: thesis: verum

end;

dom ((exp_R (#) cos ) `| REAL ) = dom (exp_R (#) (cos - sin )) by A3, A6, FDIFF_1:def 8;
then (exp_R (#) cos ) `| REAL = exp_R (#) (cos - sin ) by A7, PARTFUN1:34;
hence integral (exp_R (#) (cos - sin )),A = ((exp_R (#) cos ) . (upper_bound A)) - ((exp_R (#) cos ) . (lower_bound A)) by A4, A6, INTEGRA5:13; :: thesis: verum