let A be non empty closed_interval Subset of REAL; :: thesis: for e being Real
for f being PartFunc of REAL,REAL st A c= dom f & ( for x being Real st x in A holds
f . x = e ) holds
( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) )
let e be Real; :: thesis: for f being PartFunc of REAL,REAL st A c= dom f & ( for x being Real st x in A holds
f . x = e ) holds
( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) )
let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & ( for x being Real st x in A holds
f . x = e ) implies ( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) ) )
assume that
A1: A c= dom f and
A2: for x being Real st x in A holds
f . x = e ; :: thesis: ( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) )
B2: lower_bound A <= upper_bound A by SEQ_4:11;
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
hence ( f is_integrable_on A & f | A is bounded & integral (f,(lower_bound A),(upper_bound A)) = e * ((upper_bound A) - (lower_bound A)) ) by INTEGRA6:26, B2, A1, A2; :: thesis: verum