let A be closed-interval Subset of REAL ; :: thesis: integral (exp_R (#) exp_R ),A = (1 / 2) * (((exp_R . (upper_bound A)) ^2 ) - ((exp_R . (lower_bound A)) ^2 ))
X: A c= dom exp_R by D4;
exp_R | A is continuous ;
then A1: ( exp_R `| REAL is_integrable_on A & (exp_R `| REAL ) | A is bounded ) by Th32, X, INTEGRA5:10, INTEGRA5:11;
[#] REAL is open Subset of REAL ;
then integral (exp_R (#) exp_R ),A = (((exp_R . (upper_bound A)) * (exp_R . (upper_bound A))) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral (exp_R (#) exp_R ),A) by A1, Th32, INTEGRA5:21, SIN_COS:71
.= (((exp_R . (upper_bound A)) ^2 ) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral (exp_R (#) exp_R ),A)
.= (((exp_R . (upper_bound A)) ^2 ) - ((exp_R . (lower_bound A)) ^2 )) - (integral (exp_R (#) exp_R ),A) ;
hence integral (exp_R (#) exp_R ),A = (1 / 2) * (((exp_R . (upper_bound A)) ^2 ) - ((exp_R . (lower_bound A)) ^2 )) ; :: thesis: verum