let A be closed-interval Subset of REAL ; :: thesis: integral (- sin ),A = (cos . (upper_bound A)) - (cos . (lower_bound A))
A1: ( - sin is_integrable_on A & (- sin ) | A is bounded ) by Lm7;
dom (- sin ) = REAL by FUNCT_2:def 1;
then A2: dom (cos `| REAL ) = dom (- sin ) by FDIFF_1:def 8, SIN_COS:72;
for x being Element of REAL st x in dom (cos `| REAL ) holds
(cos `| REAL ) . x = (- sin ) . x

proof

let x be Element of REAL ; :: thesis: ( x in dom (cos `| REAL ) implies (cos `| REAL ) . x = (- sin ) . x )
assume x in dom (cos `| REAL ) ; :: thesis: (cos `| REAL ) . x = (- sin ) . x
(cos `| REAL ) . x = diff cos ,x by FDIFF_1:def 8, SIN_COS:72
.= - (sin . x) by SIN_COS:68 ;
hence (cos `| REAL ) . x = (- sin ) . x by VALUED_1:8; :: thesis: verum

end;

then cos `| REAL = - sin by A2, PARTFUN1:34;
hence integral (- sin ),A = (cos . (upper_bound A)) - (cos . (lower_bound A)) by A1, INTEGRA5:13, SIN_COS:72; :: thesis: verum