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: [#] 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, Th67, SIN_COS:73; :: thesis: verum