let a, b be real number ; :: thesis: (cos . a) - (cos . b) = integral sin ,a,b
A2: sin | REAL is continuous by FDIFF_1:33, SIN_COS:73;
( min a,b in REAL & max a,b in REAL ) by XREAL_0:def 1;
then A3: ( min a,b in dom ((- 1) (#) cos ) & max a,b in dom ((- 1) (#) cos ) ) by SIN_COS:27, VALUED_1:def 5;
X: REAL c= dom sin by FUNCT_2:def 1;
A4: ( min a,b <= a & a <= max a,b ) by XXREAL_0:17, XXREAL_0:25;
[.(min a,b),(max a,b).] c= REAL ;
then ((- 1) (#) cos ) . (max a,b) = (integral sin ,(min a,b),(max a,b)) + (((- 1) (#) cos ) . (min a,b)) by A2, A4, Th20, Th25, X, XXREAL_0:2;
then (- 1) * (cos . (max a,b)) = (integral sin ,(min a,b),(max a,b)) + (((- 1) (#) cos ) . (min a,b)) by A3, VALUED_1:def 5;
then (- 1) * (cos . (max a,b)) = (integral sin ,(min a,b),(max a,b)) + ((- 1) * (cos . (min a,b))) by A3, VALUED_1:def 5;
then A5: (cos . (min a,b)) - (cos . (max a,b)) = integral sin ,(min a,b),(max a,b) ;

A6: now

assume A7: min a,b = a ; :: thesis: (cos . a) - (cos . b) = integral sin ,a,b
then max a,b = b by XXREAL_0:36;
hence (cos . a) - (cos . b) = integral sin ,a,b by A5, A7; :: thesis: verum

end;

now

assume A8: min a,b = b ; :: thesis: (cos . a) - (cos . b) = integral sin ,a,b
then A9: max a,b = a by XXREAL_0:36;
( b < a implies (cos . a) - (cos . b) = integral sin ,a,b )

proof

assume A10: b < a ; :: thesis: (cos . a) - (cos . b) = integral sin ,a,b
then integral sin ,a,b = - (integral sin ,['b,a']) by INTEGRA5:def 5;
then integral sin ,a,b = - (integral sin ,b,a) by A10, INTEGRA5:def 5;
hence (cos . a) - (cos . b) = integral sin ,a,b by A5, A8, A9; :: thesis: verum

end;

hence (cos . a) - (cos . b) = integral sin ,a,b by A4, A6, A8, XXREAL_0:1; :: thesis: verum

end;

hence (cos . a) - (cos . b) = integral sin ,a,b by A6, XXREAL_0:15; :: thesis: verum