let I be non empty closed_interval Subset of REAL; :: thesis: for f being Function of I,REAL st f is constant holds
( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) )
let f be Function of I,REAL; :: thesis: ( f is constant implies ( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) ) )
assume f is constant ; :: thesis: ( f is HK-integrable & ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) )
then consider r being Real such that
A1: f = r (#) (chi (I,I)) by Th16;
reconsider g = chi (I,I) as Function of I,REAL by Th11;
A2: ( g is HK-integrable & HK-integral g = vol I ) by Th30;
hence f is HK-integrable by A1, Th35; :: thesis: ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) )
take r ; :: thesis: ( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) )
thus ( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) ) by A1, A2, Th35; :: thesis: verum