let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st A c= dom f & ( for x being Real st x in A holds
f . x = 0 ) holds
integral (f,A) = 0
let f be PartFunc of REAL,REAL; :: thesis: ( A c= dom f & ( for x being Real st x in A holds
f . x = 0 ) implies integral (f,A) = 0 )
assume that
B1: A c= dom f and
A1: for x being Real st x in A holds
f . x = 0 ; :: thesis: integral (f,A) = 0
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4
.= ['(lower_bound A),(upper_bound A)'] by INTEGRA5:def 3, SEQ_4:11 ;
then integral (f,A) = integral (f,(lower_bound A),(upper_bound A)) by INTEGRA5:def 4, SEQ_4:11
.= 0 * ((upper_bound A) - (lower_bound A)) by Lm5, B1, A1
.= 0 ;
hence integral (f,A) = 0 ; :: thesis: verum