let A be closed-interval Subset of REAL ; :: thesis: for r being Real holds integral (r (#) sin ),A = (r * ((- cos ) . (upper_bound A))) - (r * ((- cos ) . (lower_bound A)))
let r be Real; :: thesis: integral (r (#) sin ),A = (r * ((- cos ) . (upper_bound A))) - (r * ((- cos ) . (lower_bound A)))
X: A c= dom sin by D1;
sin | A is continuous ;
then A1: ( sin is_integrable_on A & sin | A is bounded ) by X, INTEGRA5:10, INTEGRA5:11;
[#] REAL is open Subset of REAL ;
hence integral (r (#) sin ),A = (r * ((- cos ) . (upper_bound A))) - (r * ((- cos ) . (lower_bound A))) by A1, Th26, Th29, Th68; :: thesis: verum