let a, b be Real; :: thesis: 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.]))
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & [.a,b.] c= dom f & f || ['a,b'] is bounded & f is_integrable_on ['a,b'] implies integral (f,a,b) = Integral (L-Meas,(f | [.a,b.])) )
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f || ['a,b'] is bounded and
A4: f is_integrable_on ['a,b'] ; :: thesis: integral (f,a,b) = Integral (L-Meas,(f | [.a,b.]))
reconsider A1 = [.a,b.] as Element of L-Field by MEASUR10:5, MEASUR12:75;
A1 = ['a,b'] by A1, INTEGRA5:def 3;
then Integral (L-Meas,(f | [.a,b.])) = integral (f || ['a,b']) by A2, A3, A4, Th49;
then Integral (L-Meas,(f | [.a,b.])) = integral (f,['a,b']) by INTEGRA5:def 2;
hence integral (f,a,b) = Integral (L-Meas,(f | [.a,b.])) by A1, INTEGRA5:def 4; :: thesis: verum