let A be non empty 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