let A be non empty closed_interval Subset of REAL; :: thesis: integral (cos,A) = (sin . (upper_bound A)) - (sin . (lower_bound A))
A1: for x being Element of REAL st x in dom (sin `| REAL) holds
(sin `| REAL) . x = cos . x

proof

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

end;

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