let A be non empty closed_interval Subset of REAL; :: thesis: integral ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A))
A1: [#] REAL is open Subset of REAL ;
A2: ( sin is_integrable_on A & sin | A is bounded ) by Lm19;
( cos is_integrable_on A & cos | A is bounded ) by Lm11;
hence integral ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) by A2, A1, Th26, Th27, Th29, Th66, SIN_COS:68; :: thesis: verum