let A be 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: ( cos is_integrable_on A & cos | A is bounded ) by Lm6;
A2: ( sin is_integrable_on A & sin | A is bounded ) by Lm15;
[#] REAL is open Subset of REAL ;
hence integral (sin + cos ),A = ((((- cos ) . (upper_bound A)) - ((- cos ) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) by A1, A2, Th26, Th27, Th29, Th66, SIN_COS:73; :: thesis: verum