let n be Element of NAT ; :: thesis: for a, b being Real

for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = E ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )

let a, b be Real; :: thesis: for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = E ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )

let e be Point of (REAL-NS n); :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) )

assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) ) ; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )

reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;

reconsider e1 = e as Element of REAL n by REAL_NS1:def 4;

A2: for x being Real st x in ['a,b'] holds

f1 . x = e1 by A1;

A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;

integral (f1,a,b) = integral (f,a,b) by A3, A1, Th45;

hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) by A3, Th43, A1, Th34, REAL_NS1:3; :: thesis: verum

for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = E ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )

let a, b be Real; :: thesis: for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = E ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * E )

let e be Point of (REAL-NS n); :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) holds

( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )

let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) implies ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) )

assume A1: ( a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f . x = e ) ) ; :: thesis: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e )

reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;

reconsider e1 = e as Element of REAL n by REAL_NS1:def 4;

A2: for x being Real st x in ['a,b'] holds

f1 . x = e1 by A1;

A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;

integral (f1,a,b) = integral (f,a,b) by A3, A1, Th45;

hence ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & integral (f,a,b) = (b - a) * e ) by A3, Th43, A1, Th34, REAL_NS1:3; :: thesis: verum