let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of A,REAL st vol A = 0 holds
( f is integrable & integral f = 0 )
let f be PartFunc of A,REAL; :: 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 Lm2;
A3: lower_integral f = 0 by A1, Lm3;
A4: f is lower_integrable by A1, Lm3;
f is upper_integrable by A1, Lm2;
hence ( f is integrable & integral f = 0 ) by A2, A4, A3, INTEGRA1:def 16, INTEGRA1:def 17; :: thesis: verum