let A be non empty 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))
exp_R | A is continuous ;
then A1: exp_R `| REAL is_integrable_on A by Lm8, Th32, INTEGRA5:11;
( (exp_R `| REAL) | A is bounded & [#] REAL is open Subset of REAL ) by Lm8, Th32, INTEGRA5:10;
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:66
.= (((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