let A be 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) ) )
assume rng f = {r} ; :: thesis: ( f is integrable & integral f = r * (vol A) )
then A1: f = r (#) (chi A,A) by Th3;
A2: ( chi A,A is integrable & integral (chi A,A) = vol A ) by Th2;
A3: chi A,A is Function of A,REAL by FUNCT_2:131, RFUNCT_1:78;
rng (chi A,A) = {1} by INTEGRA1:19;
then rng (chi A,A) is bounded ;
then ( rng (chi A,A) is bounded_above & rng (chi A,A) is bounded_below ) ;
then ( (chi A,A) | A is bounded_above & (chi A,A) | A is bounded_below ) by INTEGRA1:14, INTEGRA1:16;
then (chi A,A) | A is bounded ;
hence ( f is integrable & integral f = r * (vol A) ) by A1, A2, A3, INTEGRA2:31; :: thesis: verum