let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of REAL,REAL st ( for x being Real st x in A holds
f . x = 0 ) holds
integral (f,A) = 0
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real st x in A holds
f . x = 0 ) implies integral (f,A) = 0 )
assume A1: for x being Real st x in A holds
f . x = 0 ; :: thesis: integral (f,A) = 0
reconsider f = f as PartFunc of REAL,REAL ;
B1x: dom f = REAL by FUNCT_2:def 1;
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, B1x, A1
.= 0 ;
hence integral (f,A) = 0 ; :: thesis: verum