theorem :: MESFUN14:50

for a, b being Real
for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f || ['a,b'] is bounded & f is_integrable_on ['a,b'] holds
integral (f,a,b) = Integral (L-Meas,(f | [.a,b.]))