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

end;

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