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

A4: now :: thesis: ( min (a,b) = a implies (sin . b) - (sin . a) = integral (cos,a,b) )

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

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

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

end;

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

end;

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