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 A1: vol A = 0 ; :: thesis: ( f is integrable & integral f = 0 )
then A2: upper_integral f = 0 by Lm1;
A3: lower_integral f = 0 by A1, Lm2;
A4: f is lower_integrable by A1, Lm2;
f is upper_integrable by A1, Lm1;
hence ( f is integrable & integral f = 0 ) by A2, A4, A3, INTEGRA1:def 17, INTEGRA1:def 18; :: thesis: verum