let b, a be real number ; :: thesis: (exp_R . b) - (exp_R . a) = integral exp_R ,a,b
A1: exp_R | REAL is continuous by FDIFF_1:33, TAYLOR_1:16;
A2: ( min a,b <= a & a <= max a,b ) by XXREAL_0:17, XXREAL_0:25;
X: REAL c= dom exp_R by SIN_COS:51;
[.(min a,b),(max a,b).] c= REAL ;
then A3: exp_R . (max a,b) = (integral exp_R ,(min a,b),(max a,b)) + (exp_R . (min a,b)) by A1, A2, Th20, Th27, X, XXREAL_0:2;
A4: ( min a,b = a implies (exp_R . b) - (exp_R . a) = integral exp_R ,a,b )

proof

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

end;

( min a,b = b implies (exp_R . b) - (exp_R . a) = integral exp_R ,a,b )

proof

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

proof

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

end;

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

end;

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