let a, b be Real; :: 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:24, 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:24, 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:25, FUNCT_2:def 1, SIN_COS:68;
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 :: thesis: ( min (a,b) = a implies (cos . a) - (cos . b) = integral (sin,a,b) )

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 :: thesis: ( min (a,b) = b implies (cos . a) - (cos . b) = integral (sin,a,b) )

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 4;
then integral (sin,a,b) = - (integral (sin,b,a)) by A10, INTEGRA5:def 4;
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