let A be non empty closed_interval Subset of REAL; :: thesis: integral (exp_R,A) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound A))
A1: for x being Element of REAL st x in dom (exp_R `| REAL) holds
(exp_R `| REAL) . x = exp_R . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (exp_R `| REAL) implies (exp_R `| REAL) . x = exp_R . x )
assume x in dom (exp_R `| REAL) ; :: thesis: (exp_R `| REAL) . x = exp_R . x
(exp_R `| REAL) . x = diff (exp_R,x) by FDIFF_1:def 7, SIN_COS:66;
hence (exp_R `| REAL) . x = exp_R . x by SIN_COS:65; :: thesis: verum

end;

A2: ( exp_R is_integrable_on A & exp_R | A is bounded ) by Lm13;
dom (exp_R `| REAL) = dom exp_R by FDIFF_1:def 7, SIN_COS:47, SIN_COS:66;
then exp_R `| REAL = exp_R by A1, PARTFUN1:5;
hence integral (exp_R,A) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS:66; :: thesis: verum