let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL
for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )
let f be Function of A,REAL; :: thesis: for r being Real st rng f = {r} holds
( f is integrable & integral f = r * (vol A) )
let r be Real; :: thesis: ( rng f = {r} implies ( f is integrable & integral f = r * (vol A) ) )
A1: chi (A,A) is Function of A,REAL by FUNCT_2:68, RFUNCT_1:62;
A2: integral (chi (A,A)) = vol A by Th2;
assume rng f = {r} ; :: thesis: ( f is integrable & integral f = r * (vol A) )
then A3: f = r (#) (chi (A,A)) by Th3;
A4: rng (chi (A,A)) is real-bounded by INTEGRA1:17;
then A5: (chi (A,A)) | A is bounded_above by INTEGRA1:14;
A6: (chi (A,A)) | A is bounded_below by A4, INTEGRA1:12;
chi (A,A) is integrable by Th2;
hence ( f is integrable & integral f = r * (vol A) ) by A3, A2, A1, A5, A6, INTEGRA2:31; :: thesis: verum