let A be closed-interval Subset of REAL ; :: thesis: for r being Real holds integral (r (#) exp_R ),A = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A)))
let r be Real; :: thesis: integral (r (#) exp_R ),A = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A)))
( exp_R | A is bounded & [#] REAL is open Subset of REAL ) by Lm8, INTEGRA5:10;
hence integral (r (#) exp_R ),A = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A))) by Lm8, Th32, Th68, INTEGRA5:11, SIN_COS:71; :: thesis: verum