let a, b be Real; :: thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)
A1: min (a,b) <= a by XXREAL_0:17;
A2: [.(min (a,b)),(max (a,b)).] c= REAL ;
( exp_R | REAL is continuous & a <= max (a,b) ) by XXREAL_0:25;
then A3: exp_R . (max (a,b)) = (integral (exp_R,(min (a,b)),(max (a,b)))) + (exp_R . (min (a,b))) by A1, A2, INTEGRA7:20, INTEGRA7:27, SIN_COS:47, 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 4;
then exp_R . a = (- (integral (exp_R,a,b))) + (exp_R . b) by A1, A3, A6, A7, INTEGRA5:def 4;
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 A1, 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