let a, b be Real; :: thesis: () - () = 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 ;
A4: ( min (a,b) = a implies () - () = integral (exp_R,a,b) )
proof
assume A5: min (a,b) = a ; :: thesis: () - () = integral (exp_R,a,b)
then max (a,b) = b by XXREAL_0:36;
hence (exp_R . b) - () = integral (exp_R,a,b) by A3, A5; :: thesis: verum
end;
( min (a,b) = b implies () - () = integral (exp_R,a,b) )
proof
assume A6: min (a,b) = b ; :: thesis: () - () = integral (exp_R,a,b)
then A7: max (a,b) = a by XXREAL_0:36;
( b < a implies () - () = integral (exp_R,a,b) )
proof
assume b < a ; :: thesis: () - () = 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))) + () by ;
hence (exp_R . b) - () = integral (exp_R,a,b) ; :: thesis: verum
end;
hence (exp_R . b) - () = integral (exp_R,a,b) by ; :: thesis: verum
end;
hence (exp_R . b) - () = integral (exp_R,a,b) by ; :: thesis: verum