let A be non empty closed_interval Subset of REAL; :: thesis: integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A))
A1: 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 7, SIN_COS:67
.= - (sin . x) by SIN_COS:63 ;
hence (cos `| REAL) . x = (- sin) . x by VALUED_1:8; :: thesis: verum

end;

A2: ( - sin is_integrable_on A & (- sin) | A is bounded ) by Lm12;
dom (- sin) = REAL by FUNCT_2:def 1;
then dom (cos `| REAL) = dom (- sin) by FDIFF_1:def 7, SIN_COS:67;
then cos `| REAL = - sin by A1, PARTFUN1:5;
hence integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS:67; :: thesis: verum