let b, a be real number ; :: thesis: (sin . b) - (sin . a) = integral cos ,a,b
A1: cos | REAL is continuous by FDIFF_1:33, SIN_COS:72;
A2: ( min a,b <= a & a <= max a,b ) by XXREAL_0:17, XXREAL_0:25;
X: REAL = dom cos by FUNCT_2:def 1;
[.(min a,b),(max a,b).] c= REAL ;
then A3: sin . (max a,b) = (integral cos ,(min a,b),(max a,b)) + (sin . (min a,b)) by A1, A2, Th20, Th23, X, XXREAL_0:2;

A4: now

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

end;

now

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

now

assume b < a ; :: thesis: (sin . b) - (sin . a) = integral cos ,a,b
then integral cos ,a,b = - (integral cos ,['b,a']) by INTEGRA5:def 5;
then sin . a = (- (integral cos ,a,b)) + (sin . b) by A2, A3, A6, A7, INTEGRA5:def 5;
hence (sin . b) - (sin . a) = integral cos ,a,b ; :: thesis: verum

end;

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

end;

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