theorem :: INTEGRA7:28

for a, b being Real holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b)