theorem :: INTEGRA7:28
for a, b being Real holds integral (exp_R,a,b) = (exp_R . b) - (exp_R . a)