let A be closed-interval Subset of REAL ; :: thesis: integral cos ,A = (sin . (upper_bound A)) - (sin . (lower_bound A))
A1: ( cos is_integrable_on A & cos | A is bounded ) by Lm6;
dom (sin `| REAL ) = REAL by FDIFF_1:def 8, SIN_COS:73;
then A2: dom (sin `| REAL ) = dom cos by SIN_COS:27;
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 8, SIN_COS:73;
hence (sin `| REAL ) . x = cos . x by SIN_COS:69; :: thesis: verum

end;

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