let A be closed-interval Subset of REAL ; :: thesis: for r being Real holds integral (r (#) cos ),A = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A)))
let r be Real; :: thesis: integral (r (#) cos ),A = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A)))
A1: ( cos is_integrable_on A & cos | A is bounded ) by Lm6;
[#] REAL is open Subset of REAL ;
hence integral (r (#) cos ),A = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A))) by A1, Th27, Th68, SIN_COS:73; :: thesis: verum