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) ) )
A1: chi A,A is Function of A,REAL by FUNCT_2:131, RFUNCT_1:78;
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 bounded by INTEGRA1:19;
then A5: (chi A,A) | A is bounded_above by INTEGRA1:16;
A6: (chi A,A) | A is bounded_below by A4, INTEGRA1:14;
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