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

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