let A be non empty closed_interval Subset of REAL; :: thesis: integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A))
A1: dom (sin + cos) = REAL by FUNCT_2:def 1;
A2: dom (exp_R (#) (sin + cos)) = (dom exp_R) /\ (dom (sin + cos)) by VALUED_1:def 4
.= REAL /\ (dom (sin + cos)) by SIN_COS:47
.= REAL by A1 ;
A3: ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) by Lm21;
A4: ( dom (exp_R (#) sin) = REAL & [#] REAL is open Subset of REAL ) by FUNCT_2:def 1;
A5: for x being Element of REAL st x in dom ((exp_R (#) sin) `| REAL) holds
((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom ((exp_R (#) sin) `| REAL) implies ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x )
reconsider xx = x as Real ;
assume x in dom ((exp_R (#) sin) `| REAL) ; :: thesis: ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x
(exp_R (#) (sin + cos)) . x = (exp_R . x) * ((sin + cos) . x) by VALUED_1:5
.= (exp_R . x) * ((sin . xx) + (cos . xx)) by VALUED_1:1 ;
hence ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x by A4, FDIFF_7:44; :: thesis: verum

end;

exp_R (#) sin is_differentiable_on REAL by A4, FDIFF_7:44;
then dom ((exp_R (#) sin) `| REAL) = dom (exp_R (#) (sin + cos)) by A2, FDIFF_1:def 7;
then (exp_R (#) sin) `| REAL = exp_R (#) (sin + cos) by A5, PARTFUN1:5;
hence integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) by A3, A4, FDIFF_7:44, INTEGRA5:13; :: thesis: verum