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)))
( sin | A is bounded & [#] REAL is open Subset of REAL ) by Lm5, INTEGRA5:10;
hence integral (r (#) sin ),A = (r * ((- cos ) . (upper_bound A))) - (r * ((- cos ) . (lower_bound A))) by Lm5, Th26, Th29, Th68, INTEGRA5:11; :: thesis: verum