let A be closed-interval Subset of REAL ; :: thesis: for f being PartFunc of A,REAL
for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )
let f be PartFunc of A,REAL ; :: thesis: for D being Element of divs A st vol A = 0 holds
( f is integrable & integral f = 0 )
let D be Element of divs A; :: thesis: ( vol A = 0 implies ( f is integrable & integral f = 0 ) )
assume vol A = 0 ; :: thesis: ( f is integrable & integral f = 0 )
then ( f is upper_integrable & upper_integral f = 0 & f is lower_integrable & lower_integral f = 0 ) by Lm1, Lm2;
hence ( f is integrable & integral f = 0 ) by INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: verum