let I be non empty closed_interval Subset of REAL; 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; ( 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
; ( 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; ex r being Real st
( f = r (#) (chi (I,I)) & HK-integral f = r * (vol I) )
take
r
; ( 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; verum